Loogle!

Result

Found 205 declarations mentioning Filter.limsup. Of these, only the first 200 are shown.

• Filter.limsup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (u : β → α) (f : Filter β) : α
• Filter.limsup_const 📋 Mathlib.Order.LiminfLimsup
  {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} [f.NeBot] (b : β) : Filter.limsup (fun x => b) f = b
• Filter.blimsup_true 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (f : Filter β) (u : β → α) : (Filter.blimsup u f fun x => True) = Filter.limsup u f
• Filter.limsup_comp 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] (u : β → α) (v : γ → β) (f : Filter γ) : Filter.limsup (u ∘ v) f = Filter.limsup u (Filter.map v f)
• Filter.limsup_congr 📋 Mathlib.Order.LiminfLimsup
  {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β} (h : ∀ᶠ (a : α) in f, u a = v a) : Filter.limsup u f = Filter.limsup v f
• Filter.limsup_nat_add 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} [ConditionallyCompleteLattice α] (f : ℕ → α) (k : ℕ) : Filter.limsup (fun i => f (i + k)) Filter.atTop = Filter.limsup f Filter.atTop
• Filter.limsup_top_eq_iSup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteLattice α] (u : β → α) : Filter.limsup u ⊤ = ⨆ i, u i
• Filter.blimsup_eq_limsup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop} : Filter.blimsup u f p = Filter.limsup u (f ⊓ Filter.principal {x | p x})
• Filter.cofinite.limsup_set_eq 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {ι : Type u_4} {s : ι → Set α} : Filter.limsup s Filter.cofinite = {x | {n | x ∈ s n}.Infinite}
• Filter.limsup_le_iSup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {u : β → α} : Filter.limsup u f ≤ ⨆ n, u n
• Filter.mem_limsup_iff_frequently_mem 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {ι : Type u_4} {s : ι → Set α} {𝓕 : Filter ι} {a : α} : a ∈ Filter.limsup s 𝓕 ↔ ∃ᶠ (i : ι) in 𝓕, a ∈ s i
• Filter.liminf_compl 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) : (Filter.liminf u f)ᶜ = Filter.limsup (compl ∘ u) f
• Filter.limsup_compl 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) : (Filter.limsup u f)ᶜ = Filter.liminf (compl ∘ u) f
• Filter.limsup_eq 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} : Filter.limsup u f = sInf {a | ∀ᶠ (n : β) in f, u n ≤ a}
• Filter.limsup_sdiff 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) (a : α) : Filter.limsup u f \ a = Filter.limsup (fun b => u b \ a) f
• Filter.sdiff_liminf 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) (a : α) : a \ Filter.liminf u f = Filter.limsup (fun b => a \ u b) f
• Filter.limsup_top_eq_ciSup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {u : β → α} [Nonempty β] (hu : BddAbove (Set.range u)) : Filter.limsup u ⊤ = ⨆ i, u i
• Filter.limsup_bot 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) : Filter.limsup f ⊥ = ⊥
• Filter.sdiff_limsup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) [f.NeBot] (a : α) : a \ Filter.limsup u f = Filter.liminf (fun b => a \ u b) f
• Filter.HasBasis.limsup_eq_sInf_univ_of_empty 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [ConditionallyCompleteLattice α] {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) (i : ι') (hi : p i) (h'i : s i = ∅) : Filter.limsup f v = sInf Set.univ
• Filter.limsup_eq_iInf_iSup_of_nat' 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} [CompleteLattice α] {u : ℕ → α} : Filter.limsup u Filter.atTop = ⨅ n, ⨆ i, u (i + n)
• Filter.limsup_eq_sInf_sSup 📋 Mathlib.Order.LiminfLimsup
  {ι : Type u_6} {R : Type u_7} (F : Filter ι) [CompleteLattice R] (a : ι → R) : Filter.limsup a F = sInf ((fun I => sSup (a '' I)) '' F.sets)
• Filter.le_limsup_of_frequently_le' 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_6} {β : Type u_7} [CompleteLattice β] {f : Filter α} {u : α → β} {x : β} (h : ∃ᶠ (a : α) in f, x ≤ u a) : x ≤ Filter.limsup u f
• Filter.limsup_eq_iInf_iSup_of_nat 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} [CompleteLattice α] {u : ℕ → α} : Filter.limsup u Filter.atTop = ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), u i
• Filter.blimsup_not_sup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {p : β → Prop} {u : β → α} : (Filter.blimsup u f fun x => ¬p x) ⊔ Filter.blimsup u f p = Filter.limsup u f
• Filter.blimsup_sup_not 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {p : β → Prop} {u : β → α} : (Filter.blimsup u f p ⊔ Filter.blimsup u f fun x => ¬p x) = Filter.limsup u f
• Filter.inf_limsup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} (a : α) : a ⊓ Filter.limsup u f = Filter.limsup (fun x => a ⊓ u x) f
• Filter.limsup_sup_filter 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} {g : Filter β} : Filter.limsup u (f ⊔ g) = Filter.limsup u f ⊔ Filter.limsup u g
• Filter.limsup_iInf_le_iInf_limsup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [CompleteLattice α] {f : Filter β} {u : ι → β → α} : Filter.limsup (fun b => ⨅ i, u i b) f ≤ ⨅ i, Filter.limsup (u i) f
• Filter.sup_limsup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} [f.NeBot] (a : α) : a ⊔ Filter.limsup u f = Filter.limsup (fun x => a ⊔ u x) f
• Filter.le_limsup_of_frequently_le 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {ι : Type u_4} [ConditionallyCompleteLattice α] {f : Filter ι} {u : ι → α} {a : α} (hu : ∃ᶠ (i : ι) in f, a ≤ u i) (hu_le : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) : a ≤ Filter.limsup u f
• Filter.limsup_le_of_le 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {a : α} (hf : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h : ∀ᶠ (n : β) in f, u n ≤ a) : Filter.limsup u f ≤ a
• Filter.limsup_const_bot 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} : Filter.limsup (fun x => ⊥) f = ⊥
• Filter.eventually_lt_of_limsup_lt 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} {f : Filter α} [ConditionallyCompleteLinearOrder β] {u : α → β} {b : β} (h : Filter.limsup u f < b) (hu : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) : ∀ᶠ (a : α) in f, u a < b
• Filter.frequently_lt_of_lt_limsup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {b : β} (hu : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h : b < Filter.limsup u f) : ∃ᶠ (x : α) in f, b < u x
• CompleteLatticeHom.apply_limsup_iterate 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} [CompleteLattice α] (f : CompleteLatticeHom α α) (a : α) : f (Filter.limsup (fun n => (⇑f)^[n] a) Filter.atTop) = Filter.limsup (fun n => (⇑f)^[n] a) Filter.atTop
• Filter.liminf_le_limsup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} [f.NeBot] {u : β → α} (h : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h' : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u := by isBoundedDefault) : Filter.liminf u f ≤ Filter.limsup u f
• Filter.le_limsup_of_le 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {a : α} (hf : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h : ∀ (b : α), (∀ᶠ (n : β) in f, u n ≤ b) → a ≤ b) : a ≤ Filter.limsup u f
• Filter.HasBasis.limsup_eq_sInf_iUnion_iInter 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} [ConditionallyCompleteLattice α] {ι : Type u_6} {ι' : Type u_7} {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s) : Filter.limsup f v = sInf (⋃ j, ⋂ i, Set.Ici (f ↑i))
• Filter.limsup_le_limsup_of_le 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLattice β] {f g : Filter α} (h : f ≤ g) {u : α → β} (hf : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (hg : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) g u := by isBoundedDefault) : Filter.limsup u f ≤ Filter.limsup u g
• Filter.limsup_le_limsup 📋 Mathlib.Order.LiminfLimsup
  {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β} (h : u ≤ᶠ[f] v) (hu : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (hv : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v := by isBoundedDefault) : Filter.limsup u f ≤ Filter.limsup v f
• Filter.Tendsto.limsup_comp_le_limsup 📋 Mathlib.Order.LiminfLimsup
  {ι : Type u_6} {α : Type u_7} {β : Type u_8} [ConditionallyCompleteLattice β] {v : ι → α} {u : α → β} {f : Filter ι} {g : Filter α} (hv : Filter.Tendsto v f g) (hvf : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (Filter.map v f) u := by isBoundedDefault) (hg : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) g u := by isBoundedDefault) : Filter.limsup (u ∘ v) f ≤ Filter.limsup u g
• Filter.limsup_piecewise 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} {s : Set β} [DecidablePred fun x => x ∈ s] {v : β → α} : Filter.limsup (s.piecewise u v) f = (Filter.blimsup u f fun x => x ∈ s) ⊔ Filter.blimsup v f fun x => x ∉ s
• Filter.HasBasis.limsup_eq_iInf_iSup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [CompleteLattice α] {p : ι → Prop} {s : ι → Set β} {f : Filter β} {u : β → α} (h : f.HasBasis p s) : Filter.limsup u f = ⨅ i, ⨅ (_ : p i), ⨆ a ∈ s i, u a
• Filter.blimsup_eq_limsup_subtype 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop} : Filter.blimsup u f p = Filter.limsup (u ∘ Subtype.val) (Filter.comap Subtype.val f)
• Filter.limsup_eq_iInf_iSup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {u : β → α} : Filter.limsup u f = ⨅ s ∈ f, ⨆ a ∈ s, u a
• Filter.liminf_le_limsup_of_frequently_le 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u v : α → β} (h : ∃ᶠ (x : α) in f, u x ≤ v x) (h₁ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u := by isBoundedDefault) (h₂ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v := by isBoundedDefault) : Filter.liminf u f ≤ Filter.limsup v f
• GaloisConnection.l_limsup_le 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {f : Filter α} {v : α → β} {l : β → γ} {u : γ → β} (gc : GaloisConnection l u) (hlv : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => l (v x) := by isBoundedDefault) (hv_co : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v := by isBoundedDefault) : l (Filter.limsup v f) ≤ Filter.limsup (fun x => l (v x)) f
• Filter.le_limsup_iff 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {x : β} (h₁ : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h₂ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) : x ≤ Filter.limsup u f ↔ ∀ y < x, ∃ᶠ (a : α) in f, y < u a
• Filter.limsup_le_iff 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} {x : β} (h₁ : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h₂ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) : Filter.limsup u f ≤ x ↔ ∀ y > x, ∀ᶠ (a : α) in f, u a < y
• Filter.exists_lt_of_limsup_le 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : ℕ → α} (hu_bdd : Filter.IsBoundedUnder LE.le Filter.atTop u) (hu : Filter.limsup u Filter.atTop ≤ x) (hε : 0 < ε) : ∃ n, u ↑n < x + ε
• Filter.le_limsup_iff' 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} [DenselyOrdered β] {x : β} (h₁ : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h₂ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) : x ≤ Filter.limsup u f ↔ ∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a
• Filter.limsup_le_iff' 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β} [DenselyOrdered β] {x : β} (h₁ : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h₂ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) : Filter.limsup u f ≤ x ↔ ∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y
• Filter.eventually_lt_add_pos_of_limsup_le 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [Preorder β] [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : β → α} (hu_bdd : Filter.IsBoundedUnder LE.le Filter.atTop u) (hu : Filter.limsup u Filter.atTop ≤ x) (hε : 0 < ε) : ∀ᶠ (b : β) in Filter.atTop, u b < x + ε
• limsup_finset_sup' 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [ConditionallyCompleteLinearOrder β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty) (h₁ : ∀ i ∈ s, Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) (h₂ : ∀ i ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) : Filter.limsup (fun a => s.sup' hs fun i => F i a) f = s.sup' hs fun i => Filter.limsup (F i) f
• limsup_finset_sup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [ConditionallyCompleteLinearOrder β] [OrderBot β] {f : Filter α} {F : ι → α → β} {s : Finset ι} (h₁ : ∀ i ∈ s, Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) (h₂ : ∀ i ∈ s, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i) := by exact fun _ _ ↦ by isBoundedDefault) : Filter.limsup (fun a => s.sup fun i => F i a) f = s.sup fun i => Filter.limsup (F i) f
• limsup_max 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder β] {f : Filter α} {u v : α → β} (h₁ : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h₂ : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v := by isBoundedDefault) (h₃ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h₄ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v := by isBoundedDefault) : Filter.limsup (fun a => max (u a) (v a)) f = max (Filter.limsup u f) (Filter.limsup v f)
• Filter.HasBasis.limsup_eq_ciInf_ciSup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [ConditionallyCompleteLinearOrder α] {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s) {f : ι → α} (hs : ∀ (j : Subtype p), (s ↑j).Nonempty) (H : ∃ j, BddAbove (Set.range fun i => f ↑i)) : Filter.limsup f v = ⨅ j, ⨆ i, f ↑i
• Filter.HasBasis.limsup_eq_ite 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [ConditionallyCompleteLinearOrder α] {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)] (hv : v.HasBasis p s) (f : ι → α) : Filter.limsup f v = if ∃ j, s ↑j = ∅ then sInf Set.univ else if ∀ (j : Subtype p), ¬BddAbove (Set.range fun i => f ↑i) then sInf ∅ else ⨅ j, ⨆ i, f ↑i
• OrderIso.limsup_apply 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} {γ : Type u_6} [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {f : Filter α} {u : α → β} (g : β ≃o γ) (hu : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (hu_co : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (hgu : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x) := by isBoundedDefault) (hgu_co : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => g (u x) := by isBoundedDefault) : g (Filter.limsup u f) = Filter.limsup (fun x => g (u x)) f
• Filter.Tendsto.limsup_eq 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter β} {u : β → α} {a : α} [f.NeBot] (h : Filter.Tendsto u f (nhds a)) : Filter.limsup u f = a
• MapClusterPt.le_limsup 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {u : β → α} {f : Filter β} {x : α} (hx : MapClusterPt x f u) (hb : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) : x ≤ Filter.limsup u f
• eventually_le_limsup 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α] {f : Filter β} [CountableInterFilter f] {u : β → α} (hf : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) : ∀ᶠ (b : β) in f, u b ≤ Filter.limsup u f
• MapClusterPt.limsup 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {u : β → α} {f : Filter β} [f.NeBot] (hc : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (hb : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) : MapClusterPt (Filter.limsup u f) f u
• tendsto_of_liminf_eq_limsup 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter β} {u : β → α} {a : α} (hinf : Filter.liminf u f = a) (hsup : Filter.limsup u f = a) (h : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h' : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u := by isBoundedDefault) : Filter.Tendsto u f (nhds a)
• isGreatest_mapClusterPt_limsup 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {u : β → α} {f : Filter β} [f.NeBot] (hc : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (hb : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) : IsGreatest {x | MapClusterPt x f u} (Filter.limsup u f)
• exists_seq_tendsto_limsup 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α] {f : Filter β} [f.NeBot] [f.IsCountablyGenerated] {u : β → α} (hc : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (hb : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) : ∃ x, Filter.Tendsto (u ∘ x) Filter.atTop (nhds (Filter.limsup u f)) ∧ Filter.Tendsto x Filter.atTop f
• limsup_eq_bot 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [CompleteLinearOrder α] [TopologicalSpace α] [FirstCountableTopology α] [OrderTopology α] {f : Filter β} [CountableInterFilter f] {u : β → α} : Filter.limsup u f = ⊥ ↔ u =ᶠ[f] ⊥
• tendsto_of_le_liminf_of_limsup_le 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {f : Filter β} {u : β → α} {a : α} (hinf : a ≤ Filter.liminf u f) (hsup : Filter.limsup u f ≤ a) (h : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h' : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u := by isBoundedDefault) : Filter.Tendsto u f (nhds a)
• Antitone.map_limsInf_of_continuousAt 📋 Mathlib.Topology.Order.LiminfLimsup
  {R : Type u_4} {S : Type u_5} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {F : Filter R} [F.NeBot] {f : R → S} (f_decr : Antitone f) (f_cont : ContinuousAt f F.limsInf) (cobdd : Filter.IsCobounded (fun x1 x2 => x1 ≥ x2) F := by isBoundedDefault) (bdd_below : Filter.IsBounded (fun x1 x2 => x1 ≥ x2) F := by isBoundedDefault) : f F.limsInf = Filter.limsup f F
• Monotone.map_limsSup_of_continuousAt 📋 Mathlib.Topology.Order.LiminfLimsup
  {R : Type u_4} {S : Type u_5} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {F : Filter R} [F.NeBot] {f : R → S} (f_incr : Monotone f) (f_cont : ContinuousAt f F.limsSup) (bdd_above : Filter.IsBounded (fun x1 x2 => x1 ≤ x2) F := by isBoundedDefault) (cobdd : Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) F := by isBoundedDefault) : f F.limsSup = Filter.limsup f F
• tendsto_iSup_of_tendsto_limsup 📋 Mathlib.Topology.Order.LiminfLimsup
  {ι : Type u_1} {α : Type u_7} {β : Type u_8} [ConditionallyCompleteLattice α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {u : ι → α → β} {c : β} (h_all : ∀ (i : ι), Filter.Tendsto (u i) Filter.atTop (nhds c)) (h_limsup : Filter.Tendsto (fun r => Filter.limsup (fun i => u i r) Filter.cofinite) Filter.atTop (nhds c)) (h_anti : ∀ (i : ι), Antitone (u i)) : Filter.Tendsto (fun r => ⨆ i, u i r) Filter.atTop (nhds c)
• Nat.tendsto_iSup_of_tendsto_limsup 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_7} {β : Type u_8} [ConditionallyCompleteLattice α] [CompleteLinearOrder β] [TopologicalSpace β] [OrderTopology β] {u : ℕ → α → β} {c : β} (h_all : ∀ (n : ℕ), Filter.Tendsto (u n) Filter.atTop (nhds c)) (h_limsup : Filter.Tendsto (fun r => Filter.limsup (fun n => u n r) Filter.atTop) Filter.atTop (nhds c)) (h_anti : ∀ (n : ℕ), Antitone (u n)) : Filter.Tendsto (fun r => ⨆ n, u n r) Filter.atTop (nhds c)
• Antitone.map_liminf_of_continuousAt 📋 Mathlib.Topology.Order.LiminfLimsup
  {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {f : R → S} (f_decr : Antitone f) (a : ι → R) (f_cont : ContinuousAt f (Filter.liminf a F)) (cobdd : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) F a := by isBoundedDefault) (bdd_below : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) F a := by isBoundedDefault) : f (Filter.liminf a F) = Filter.limsup (f ∘ a) F
• Antitone.map_limsup_of_continuousAt 📋 Mathlib.Topology.Order.LiminfLimsup
  {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {f : R → S} (f_decr : Antitone f) (a : ι → R) (f_cont : ContinuousAt f (Filter.limsup a F)) (bdd_above : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) F a := by isBoundedDefault) (cobdd : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F a := by isBoundedDefault) : f (Filter.limsup a F) = Filter.liminf (f ∘ a) F
• Monotone.map_limsup_of_continuousAt 📋 Mathlib.Topology.Order.LiminfLimsup
  {ι : Type u_1} {R : Type u_4} {S : Type u_5} {F : Filter ι} [F.NeBot] [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] [ConditionallyCompleteLinearOrder S] [TopologicalSpace S] [OrderTopology S] {f : R → S} (f_incr : Monotone f) (a : ι → R) (f_cont : ContinuousAt f (Filter.limsup a F)) (bdd_above : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) F a := by isBoundedDefault) (cobdd : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F a := by isBoundedDefault) : f (Filter.limsup a F) = Filter.limsup (f ∘ a) F
• Antitone.limsup_nhdsLT_eq_iInf₂ 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [CompleteLattice β] {f : α → β} [NoMinOrder α] (hf : Antitone f) (a : α) : Filter.limsup f (nhdsWithin a (Set.Iio a)) = ⨅ r, ⨅ (_ : r < a), f r
• Monotone.limsup_nhdsGT_eq_iInf₂ 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [CompleteLattice β] {f : α → β} [NoMaxOrder α] (hf : Monotone f) (a : α) : Filter.limsup f (nhdsWithin a (Set.Ioi a)) = ⨅ r, ⨅ (_ : r > a), f r
• Antitone.limsup_nhdsLT_eq_iInf₂_of_exists_lt 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [CompleteLattice β] {f : α → β} (hf : Antitone f) (a : α) (hb : ∃ b, b < a) : Filter.limsup f (nhdsWithin a (Set.Iio a)) = ⨅ r, ⨅ (_ : r < a), f r
• Monotone.limsup_nhdsGT_eq_iInf₂_of_exists_gt 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [CompleteLattice β] {f : α → β} (hf : Monotone f) (a : α) (hb : ∃ b, a < b) : Filter.limsup f (nhdsWithin a (Set.Ioi a)) = ⨅ r, ⨅ (_ : r > a), f r
• ENNReal.inv_liminf 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} {x : ι → ENNReal} {l : Filter ι} : (Filter.liminf x l)⁻¹ = Filter.limsup (fun i => (x i)⁻¹) l
• ENNReal.inv_limsup 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} {x : ι → ENNReal} {l : Filter ι} : (Filter.limsup x l)⁻¹ = Filter.liminf (fun i => (x i)⁻¹) l
• ENNReal.ofNNReal_limsup 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} {f : Filter ι} {u : ι → NNReal} (hf : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) : ↑(Filter.limsup u f) = Filter.limsup (fun i => ↑(u i)) f
• ENNReal.limsup_sub_const 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} (F : Filter ι) (f : ι → ENNReal) (c : ENNReal) : Filter.limsup (fun i => f i - c) F = Filter.limsup f F - c
• ENNReal.limsup_toReal_eq 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} {f : Filter ι} {u : ι → ENNReal} [f.NeBot] {b : ENNReal} (b_ne_top : b ≠ ⊤) (le_b : ∀ᶠ (i : ι) in f, u i ≤ b) : Filter.limsup (fun i => (u i).toReal) f = (Filter.limsup u f).toReal
• ENNReal.limsup_const_sub 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} (F : Filter ι) (f : ι → ENNReal) {c : ENNReal} (c_ne_top : c ≠ ⊤) : Filter.limsup (fun i => c - f i) F = c - Filter.liminf f F
• ENNReal.liminf_const_sub 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} (F : Filter ι) [F.NeBot] (f : ι → ENNReal) {c : ENNReal} (c_ne_top : c ≠ ⊤) : Filter.liminf (fun i => c - f i) F = c - Filter.limsup f F
• ENNReal.limsup_add_of_left_tendsto_zero 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} {u : Filter ι} {f : ι → ENNReal} (hf : Filter.Tendsto f u (nhds 0)) (g : ι → ENNReal) : Filter.limsup (f + g) u = Filter.limsup g u
• ENNReal.limsup_add_of_right_tendsto_zero 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} {u : Filter ι} {g : ι → ENNReal} (hg : Filter.Tendsto g u (nhds 0)) (f : ι → ENNReal) : Filter.limsup (f + g) u = Filter.limsup f u
• ENNReal.le_limsup_mul 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} {f : Filter ι} {u v : ι → ENNReal} : Filter.limsup u f * Filter.liminf v f ≤ Filter.limsup (u * v) f
• ENNReal.liminf_mul_le 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} {f : Filter ι} {u v : ι → ENNReal} (h : Filter.limsup u f ≠ 0 ∨ Filter.liminf v f ≠ ⊤) (h' : Filter.limsup u f ≠ ⊤ ∨ Filter.liminf v f ≠ 0) : Filter.liminf (u * v) f ≤ Filter.limsup u f * Filter.liminf v f
• ENNReal.limsup_mul_le' 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} {f : Filter ι} {u v : ι → ENNReal} (h : Filter.limsup u f ≠ 0 ∨ Filter.limsup v f ≠ ⊤) (h' : Filter.limsup u f ≠ ⊤ ∨ Filter.limsup v f ≠ 0) : Filter.limsup (u * v) f ≤ Filter.limsup u f * Filter.limsup v f
• ENNReal.tsum_eq_limsup_sum_nat 📋 Mathlib.Topology.Algebra.InfiniteSum.ENNReal
  {f : ℕ → ENNReal} : ∑' (i : ℕ), f i = Filter.limsup (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop
• UpperSemicontinuous.limsup_le 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {γ : Type u_4} [CompleteLinearOrder γ] {f : α → γ} : UpperSemicontinuous f → ∀ (x : α), Filter.limsup f (nhds x) ≤ f x
• upperSemicontinuous_iff_limsup_le 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {γ : Type u_4} [CompleteLinearOrder γ] {f : α → γ} : UpperSemicontinuous f ↔ ∀ (x : α), Filter.limsup f (nhds x) ≤ f x
• UpperSemicontinuousAt.limsup_le 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_4} [CompleteLinearOrder γ] {f : α → γ} : UpperSemicontinuousAt f x → Filter.limsup f (nhds x) ≤ f x
• upperSemicontinuousAt_iff_limsup_le 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_4} [CompleteLinearOrder γ] {f : α → γ} : UpperSemicontinuousAt f x ↔ Filter.limsup f (nhds x) ≤ f x
• UpperSemicontinuousWithinAt.limsup_le 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_4} [CompleteLinearOrder γ] {f : α → γ} : UpperSemicontinuousWithinAt f s x → Filter.limsup f (nhdsWithin x s) ≤ f x
• upperSemicontinuousWithinAt_iff_limsup_le 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_4} [CompleteLinearOrder γ] {f : α → γ} : UpperSemicontinuousWithinAt f s x ↔ Filter.limsup f (nhdsWithin x s) ≤ f x
• UpperSemicontinuousOn.limsup_le 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_4} [CompleteLinearOrder γ] {f : α → γ} : UpperSemicontinuousOn f s → ∀ x ∈ s, Filter.limsup f (nhdsWithin x s) ≤ f x
• upperSemicontinuousOn_iff_limsup_le 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_4} [CompleteLinearOrder γ] {f : α → γ} : UpperSemicontinuousOn f s ↔ ∀ x ∈ s, Filter.limsup f (nhdsWithin x s) ≤ f x
• EReal.liminf_neg 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {v : α → EReal} : Filter.liminf (-v) f = -Filter.limsup v f
• EReal.limsup_neg 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {v : α → EReal} : Filter.limsup (-v) f = -Filter.liminf v f
• EReal.liminf_const_mul_of_nonpos_of_ne_bot 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u : α → EReal} [f.NeBot] {c : EReal} (h₁ : c ≤ 0) (h₂ : c ≠ ⊥) : Filter.liminf (fun x => c * u x) f = c * Filter.limsup u f
• EReal.limsup_const_mul_of_nonneg_of_ne_top 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u : α → EReal} [f.NeBot] {c : EReal} (h₁ : 0 ≤ c) (h₂ : c ≠ ⊤) : Filter.limsup (fun x => c * u x) f = c * Filter.limsup u f
• EReal.limsup_const_mul_of_nonpos_of_ne_bot 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u : α → EReal} [f.NeBot] {c : EReal} (h₁ : c ≤ 0) (h₂ : c ≠ ⊥) : Filter.limsup (fun x => c * u x) f = c * Filter.liminf u f
• EReal.limsup_add_bot_of_ne_top 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u v : α → EReal} (h : Filter.limsup u f = ⊥) (h' : Filter.limsup v f ≠ ⊤) : Filter.limsup (u + v) f = ⊥
• EReal.le_limsup_add 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u v : α → EReal} : Filter.limsup u f + Filter.liminf v f ≤ Filter.limsup (u + v) f
• EReal.limsup_add_le_of_le 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u v : α → EReal} {a b : EReal} (ha : Filter.limsup u f < a) (hb : Filter.limsup v f ≤ b) : Filter.limsup (u + v) f ≤ a + b
• EReal.le_limsup_mul 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u v : α → EReal} (hu : ∃ᶠ (x : α) in f, 0 ≤ u x) (hv : 0 ≤ᶠ[f] v) : Filter.limsup u f * Filter.liminf v f ≤ Filter.limsup (u * v) f
• EReal.liminf_add_le 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u v : α → EReal} (h : Filter.limsup u f ≠ ⊥ ∨ Filter.liminf v f ≠ ⊤) (h' : Filter.limsup u f ≠ ⊤ ∨ Filter.liminf v f ≠ ⊥) : Filter.liminf (u + v) f ≤ Filter.limsup u f + Filter.liminf v f
• EReal.limsup_add_le 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u v : α → EReal} (h : Filter.limsup u f ≠ ⊥ ∨ Filter.limsup v f ≠ ⊤) (h' : Filter.limsup u f ≠ ⊤ ∨ Filter.limsup v f ≠ ⊥) : Filter.limsup (u + v) f ≤ Filter.limsup u f + Filter.limsup v f
• EReal.limsup_mul_le 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u v : α → EReal} (hu : ∃ᶠ (x : α) in f, 0 ≤ u x) (hv : 0 ≤ᶠ[f] v) (h₁ : Filter.limsup u f ≠ 0 ∨ Filter.limsup v f ≠ ⊤) (h₂ : Filter.limsup u f ≠ ⊤ ∨ Filter.limsup v f ≠ 0) : Filter.limsup (u * v) f ≤ Filter.limsup u f * Filter.limsup v f
• EReal.liminf_mul_le 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u v : α → EReal} [f.NeBot] (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v) (h₁ : Filter.limsup u f ≠ 0 ∨ Filter.liminf v f ≠ ⊤) (h₂ : Filter.limsup u f ≠ ⊤ ∨ Filter.liminf v f ≠ 0) : Filter.liminf (u * v) f ≤ Filter.limsup u f * Filter.liminf v f
• MeasurableSet.measurableSet_limsup 📋 Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
  {α : Type u_1} [MeasurableSpace α] {s : ℕ → Set α} (hs : ∀ (n : ℕ), MeasurableSet (s n)) : MeasurableSet (Filter.limsup s Filter.atTop)
• MeasureTheory.limsup_ae_eq_of_forall_ae_eq 📋 Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
  {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} (s : ℕ → Set α) {t : Set α} (h : ∀ (n : ℕ), s n =ᵐ[μ] t) : Filter.limsup s Filter.atTop =ᵐ[μ] t
• MeasureTheory.measure_limsup_atTop_eq_zero 📋 Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
  {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : ℕ → Set α} (hs : ∑' (i : ℕ), μ (s i) ≠ ⊤) : μ (Filter.limsup s Filter.atTop) = 0
• MeasureTheory.measure_limsup_cofinite_eq_zero 📋 Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
  {α : Type u_1} {ι : Type u_2} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] [Countable ι] {μ : F} {s : ι → Set α} (hs : ∑' (i : ι), μ (s i) ≠ ⊤) : μ (Filter.limsup s Filter.cofinite) = 0
• MeasureTheory.Measure.QuasiMeasurePreserving.limsup_preimage_iterate_ae_eq 📋 Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
  {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → α} (hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ) (hs : f ⁻¹' s =ᵐ[μ] s) : Filter.limsup (fun n => (Set.preimage f)^[n] s) Filter.atTop =ᵐ[μ] s
• Measurable.limsup 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : MeasurableSpace δ} [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {f : ℕ → δ → α} (hf : ∀ (i : ℕ), Measurable (f i)) : Measurable fun x => Filter.limsup (fun i => f i x) Filter.atTop
• Measurable.limsup' 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} {δ : Type u_4} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] {mδ : MeasurableSpace δ} [ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α] {ι : Type u_5} {ι' : Type u_6} {f : ι → δ → α} {u : Filter ι} (hf : ∀ (i : ι), Measurable (f i)) {p : ι' → Prop} {s : ι' → Set ι} (hu : u.HasCountableBasis p s) (hs : ∀ (i : ι'), (s i).Countable) : Measurable fun x => Filter.limsup (fun i => f i x) u
• MeasureTheory.limsup_lintegral_le 📋 Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (g : α → ENNReal) (hf_meas : ∀ (n : ℕ), Measurable (f n)) (h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g) (h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤) : Filter.limsup (fun n => ∫⁻ (a : α), f n a ∂μ) Filter.atTop ≤ ∫⁻ (a : α), Filter.limsup (fun n => f n a) Filter.atTop ∂μ
• ENNReal.eventually_le_limsup 📋 Mathlib.Order.Filter.ENNReal
  {α : Type u_1} {f : Filter α} [CountableInterFilter f] (u : α → ENNReal) : ∀ᶠ (y : α) in f, u y ≤ Filter.limsup u f
• NNReal.toReal_limsup 📋 Mathlib.Order.Filter.ENNReal
  {ι : Type u_1} {f : Filter ι} {u : ι → NNReal} : Filter.limsup (fun i => ↑(u i)) f = ↑(Filter.limsup u f)
• Real.limsup_of_not_isBoundedUnder 📋 Mathlib.Order.Filter.ENNReal
  {ι : Type u_1} {f : Filter ι} {u : ι → ℝ} (hf : ¬Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) : Filter.limsup u f = 0
• Real.limsup_of_not_isCoboundedUnder 📋 Mathlib.Order.Filter.ENNReal
  {ι : Type u_1} {f : Filter ι} {u : ι → ℝ} (hf : ¬Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) : Filter.limsup u f = 0
• NNReal.limsup_of_not_isBoundedUnder 📋 Mathlib.Order.Filter.ENNReal
  {ι : Type u_1} {f : Filter ι} {u : ι → NNReal} (hf : ¬Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) : Filter.limsup u f = 0
• ENNReal.ofReal_limsup_toReal 📋 Mathlib.Order.Filter.ENNReal
  {α : Type u_1} {f : Filter α} [f.NeBot] {u : α → ENNReal} {C : NNReal} (hf : ∀ᶠ (a : α) in f, u a ≤ ↑C) : ENNReal.ofReal (Filter.limsup (fun a => (u a).toReal) f) = Filter.limsup u f
• ENNReal.limsup_eq_zero_iff 📋 Mathlib.Order.Filter.ENNReal
  {α : Type u_1} {f : Filter α} [CountableInterFilter f] {u : α → ENNReal} : Filter.limsup u f = 0 ↔ u =ᶠ[f] 0
• ENNReal.ofReal_limsup 📋 Mathlib.Order.Filter.ENNReal
  {α : Type u_1} {f : Filter α} {u : α → ℝ} (h₁ : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h₂ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) : ENNReal.ofReal (Filter.limsup u f) = Filter.limsup (fun a => ENNReal.ofReal (u a)) f
• ENNReal.toReal_limsup 📋 Mathlib.Order.Filter.ENNReal
  {α : Type u_1} {f : Filter α} {u : α → ENNReal} (h₁ : ∀ᶠ (a : α) in f, u a ≠ ⊤) (h₂ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => (u a).toReal := by isBoundedDefault) : (Filter.limsup u f).toReal = Filter.limsup (fun a => (u a).toReal) f
• ENNReal.limsup_const_mul 📋 Mathlib.Order.Filter.ENNReal
  {α : Type u_1} {f : Filter α} [CountableInterFilter f] {u : α → ENNReal} {a : ENNReal} : Filter.limsup (fun x => a * u x) f = a * Filter.limsup u f
• ENNReal.limsup_mul_const 📋 Mathlib.Order.Filter.ENNReal
  {α : Type u_1} {f : Filter α} [CountableInterFilter f] {u : α → ENNReal} {a : ENNReal} : Filter.limsup (fun x => u x * a) f = a * Filter.limsup u f
• ENNReal.limsup_const_mul_of_ne_top 📋 Mathlib.Order.Filter.ENNReal
  {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal} (ha_top : a ≠ ⊤) : Filter.limsup (fun x => a * u x) f = a * Filter.limsup u f
• ENNReal.limsup_mul_const_of_ne_top 📋 Mathlib.Order.Filter.ENNReal
  {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal} (ha_top : a ≠ ⊤) : Filter.limsup (fun x => u x * a) f = a * Filter.limsup u f
• ENNReal.limsup_liminf_le_liminf_limsup 📋 Mathlib.Order.Filter.ENNReal
  {α : Type u_1} {β : Type u_2} [Countable β] {f : Filter α} [CountableInterFilter f] {g : Filter β} (u : α → β → ENNReal) : Filter.limsup (fun a => Filter.liminf (fun b => u a b) g) f ≤ Filter.liminf (fun b => Filter.limsup (fun a => u a b) f) g
• ENNReal.limsup_add_le 📋 Mathlib.Order.Filter.ENNReal
  {α : Type u_1} {f : Filter α} [CountableInterFilter f] (u v : α → ENNReal) : Filter.limsup (u + v) f ≤ Filter.limsup u f + Filter.limsup v f
• ENNReal.limsup_mul_le 📋 Mathlib.Order.Filter.ENNReal
  {α : Type u_1} {f : Filter α} [CountableInterFilter f] (u v : α → ENNReal) : Filter.limsup (u * v) f ≤ Filter.limsup u f * Filter.limsup v f
• Set.limsup_eq_tendsto_sum_indicator_atTop 📋 Mathlib.Algebra.Order.Archimedean.IndicatorCard
  {α : Type u_1} {R : Type u_2} [AddCommMonoid R] [PartialOrder R] [IsOrderedAddMonoid R] [AddLeftStrictMono R] [Archimedean R] {r : R} (h : 0 < r) (s : ℕ → Set α) : Filter.limsup s Filter.atTop = {ω | Filter.Tendsto (fun n => ∑ k ∈ Finset.range n, (s k).indicator (fun x => r) ω) Filter.atTop Filter.atTop}
• FormalMultilinearSeries.radius_inv_eq_limsup 📋 Mathlib.Analysis.Analytic.RadiusLiminf
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) : p.radius⁻¹ = Filter.limsup (fun n => ↑(‖p n‖₊ ^ (1 / ↑n))) Filter.atTop
• spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius 📋 Mathlib.Analysis.Normed.Algebra.GelfandFormula
  {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] (a : A) : Filter.limsup (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop ≤ spectralRadius ℂ a
• iSup_limsup_dimH 📋 Mathlib.Topology.MetricSpace.HausdorffDimension
  {X : Type u_2} [EMetricSpace X] [SecondCountableTopology X] (s : Set X) : ⨆ x, Filter.limsup dimH (nhdsWithin x s).smallSets = dimH s
• bsupr_limsup_dimH 📋 Mathlib.Topology.MetricSpace.HausdorffDimension
  {X : Type u_2} [EMetricSpace X] [SecondCountableTopology X] (s : Set X) : ⨆ x ∈ s, Filter.limsup dimH (nhdsWithin x s).smallSets = dimH s
• le_limsup_mul 📋 Mathlib.Topology.Algebra.Order.LiminfLimsup
  {ι : Type u_1} {f : Filter ι} {u v : ι → ℝ} (h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x) (h₂ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v) (h₄ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) : Filter.limsup u f * Filter.liminf v f ≤ Filter.limsup (u * v) f
• limsup_mul_le 📋 Mathlib.Topology.Algebra.Order.LiminfLimsup
  {ι : Type u_1} {f : Filter ι} {u v : ι → ℝ} (h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x) (h₂ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v) (h₄ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) : Filter.limsup (u * v) f ≤ Filter.limsup u f * Filter.limsup v f
• liminf_mul_le 📋 Mathlib.Topology.Algebra.Order.LiminfLimsup
  {ι : Type u_1} {f : Filter ι} {u v : ι → ℝ} [f.NeBot] (h₁ : 0 ≤ᶠ[f] u) (h₂ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) (h₃ : 0 ≤ᶠ[f] v) (h₄ : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v) : Filter.liminf (u * v) f ≤ Filter.limsup u f * Filter.liminf v f
• limsup_add_const 📋 Mathlib.Topology.Algebra.Order.LiminfLimsup
  {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [F.NeBot] [Add R] [ContinuousAdd R] [AddRightMono R] (f : ι → R) (c : R) (bdd_above : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) F f) (cobdd : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f) : Filter.limsup (fun i => f i + c) F = Filter.limsup f F + c
• limsup_const_add 📋 Mathlib.Topology.Algebra.Order.LiminfLimsup
  {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [F.NeBot] [Add R] [ContinuousAdd R] [AddLeftMono R] (f : ι → R) (c : R) (bdd_above : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) F f) (cobdd : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f) : Filter.limsup (fun i => c + f i) F = c + Filter.limsup f F
• limsup_sub_const 📋 Mathlib.Topology.Algebra.Order.LiminfLimsup
  {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] (f : ι → R) (c : R) (bdd_above : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) F f) (cobdd : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f) : Filter.limsup (fun i => f i - c) F = Filter.limsup f F - c
• limsup_const_sub 📋 Mathlib.Topology.Algebra.Order.LiminfLimsup
  {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] [AddLeftMono R] (f : ι → R) (c : R) (cobdd : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) F f) (bdd_below : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) F f) : Filter.limsup (fun i => c - f i) F = c - Filter.liminf f F
• liminf_const_sub 📋 Mathlib.Topology.Algebra.Order.LiminfLimsup
  {ι : Type u_1} {R : Type u_4} [ConditionallyCompleteLinearOrder R] [TopologicalSpace R] [OrderTopology R] (F : Filter ι) [F.NeBot] [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R] [AddLeftMono R] (f : ι → R) (c : R) (bdd_above : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) F f) (cobdd : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f) : Filter.liminf (fun i => c - f i) F = c - Filter.limsup f F
• le_limsup_add 📋 Mathlib.Topology.Algebra.Order.LiminfLimsup
  {ι : Type u_1} {α : Type u_2} [AddCommGroup α] [ConditionallyCompleteLinearOrder α] [DenselyOrdered α] [AddLeftMono α] {f : Filter ι} [f.NeBot] {u v : ι → α} (h₁ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h₂ : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h₃ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v := by isBoundedDefault) (h₄ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v := by isBoundedDefault) : Filter.limsup u f + Filter.liminf v f ≤ Filter.limsup (u + v) f
• liminf_add_le 📋 Mathlib.Topology.Algebra.Order.LiminfLimsup
  {ι : Type u_1} {α : Type u_2} [AddCommGroup α] [ConditionallyCompleteLinearOrder α] [DenselyOrdered α] [AddLeftMono α] {f : Filter ι} [f.NeBot] {u v : ι → α} (h₁ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u := by isBoundedDefault) (h₂ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h₃ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v := by isBoundedDefault) (h₄ : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v := by isBoundedDefault) : Filter.liminf (u + v) f ≤ Filter.limsup u f + Filter.liminf v f
• limsup_add_le 📋 Mathlib.Topology.Algebra.Order.LiminfLimsup
  {ι : Type u_1} {α : Type u_2} [AddCommGroup α] [ConditionallyCompleteLinearOrder α] [DenselyOrdered α] [AddLeftMono α] {f : Filter ι} [f.NeBot] {u v : ι → α} (h₁ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u := by isBoundedDefault) (h₂ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h₃ : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v := by isBoundedDefault) (h₄ : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v := by isBoundedDefault) : Filter.limsup (u + v) f ≤ Filter.limsup u f + Filter.limsup v f
• BoundedContinuousFunction.tendsto_integral_of_forall_limsup_integral_le_integral 📋 Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
  {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {μs : ι → MeasureTheory.Measure X} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] (h : ∀ (f : BoundedContinuousFunction X ℝ), 0 ≤ f → Filter.limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ) (f : BoundedContinuousFunction X ℝ) : Filter.Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (nhds (∫ (x : X), f x ∂μ))
• MeasureTheory.limsup_trim 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Trim
  {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f : α → ENNReal} (hf : Measurable f) : Filter.limsup f (MeasureTheory.ae (μ.trim hm)) = Filter.limsup f (MeasureTheory.ae μ)
• MeasureTheory.tendsto_of_forall_isClosed_limsup_real_le' 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} {L : Filter ι} [L.IsCountablyGenerated] (h : ∀ (F : Set Ω), IsClosed F → Filter.limsup (fun i => (↑(μs i)).real F) L ≤ (↑μ).real F) : Filter.Tendsto μs L (nhds μ)
• MeasureTheory.tendsto_of_forall_isClosed_limsup_le_nat 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} {mΩ : MeasurableSpace Ω} [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ℕ → MeasureTheory.ProbabilityMeasure Ω} (h : ∀ (F : Set Ω), IsClosed F → Filter.limsup (fun i => (μs i) F) Filter.atTop ≤ μ F) : Filter.Tendsto μs Filter.atTop (nhds μ)
• MeasureTheory.tendsto_of_forall_isClosed_limsup_le 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} {L : Filter ι} [L.IsCountablyGenerated] (h : ∀ (F : Set Ω), IsClosed F → Filter.limsup (fun i => (μs i) F) L ≤ μ F) : Filter.Tendsto μs L (nhds μ)
• MeasureTheory.tendsto_of_forall_isClosed_limsup_le' 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} {L : Filter ι} [L.IsCountablyGenerated] (h : ∀ (F : Set Ω), IsClosed F → Filter.limsup (fun i => ↑(μs i) F) L ≤ ↑μ F) : Filter.Tendsto μs L (nhds μ)
• MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [MeasurableSpace Ω] [TopologicalSpace Ω] [HasOuterApproxClosed Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω} {μs : ι → MeasureTheory.FiniteMeasure Ω} (μs_lim : Filter.Tendsto μs L (nhds μ)) {F : Set Ω} (F_closed : IsClosed F) : Filter.limsup (fun i => ↑(μs i) F) L ≤ ↑μ F
• MeasureTheory.ProbabilityMeasure.limsup_measure_closed_le_of_tendsto 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω] {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} (μs_lim : Filter.Tendsto μs L (nhds μ)) {F : Set Ω} (F_closed : IsClosed F) : Filter.limsup (fun i => ↑(μs i) F) L ≤ ↑μ F
• MeasureTheory.tendsto_of_forall_isCompact_of_isTightMeasureSet 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} {L : Filter ι} [L.IsCountablyGenerated] (h₁ : MeasureTheory.IsTightMeasureSet (Set.range (MeasureTheory.ProbabilityMeasure.toMeasure ∘ μs))) (h₂ : ∀ (F : Set Ω), IsCompact F → Filter.limsup (fun x => (μs x) F) L ≤ μ F) : Filter.Tendsto μs L (nhds μ)
• MeasureTheory.le_measure_compl_liminf_of_limsup_measure_le 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] {E : Set Ω} (E_mble : MeasurableSet E) (h : Filter.limsup (fun i => (μs i) E) L ≤ μ E) : μ Eᶜ ≤ Filter.liminf (fun i => (μs i) Eᶜ) L
• MeasureTheory.le_measure_liminf_of_limsup_measure_compl_le 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] {E : Set Ω} (E_mble : MeasurableSet E) (h : Filter.limsup (fun i => (μs i) Eᶜ) L ≤ μ Eᶜ) : μ E ≤ Filter.liminf (fun i => (μs i) E) L
• MeasureTheory.limsup_measure_compl_le_of_le_liminf_measure 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] {E : Set Ω} (E_mble : MeasurableSet E) (h : μ E ≤ Filter.liminf (fun i => (μs i) E) L) : Filter.limsup (fun i => (μs i) Eᶜ) L ≤ μ Eᶜ
• MeasureTheory.limsup_measure_le_of_le_liminf_measure_compl 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] {E : Set Ω} (E_mble : MeasurableSet E) (h : μ Eᶜ ≤ Filter.liminf (fun i => (μs i) Eᶜ) L) : Filter.limsup (fun i => (μs i) E) L ≤ μ E
• MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] : (∀ (F : Set Ω), IsClosed F → Filter.limsup (fun i => (μs i) F) L ≤ μ F) ↔ ∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) L
• MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measure 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [MeasurableSpace Ω] [TopologicalSpace Ω] [TopologicalSpace.PseudoMetrizableSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {μs : ι → MeasureTheory.Measure Ω} (h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))) (F : Set Ω) (F_closed : IsClosed F) : Filter.limsup (fun i => (μs i) F) L ≤ μ F
• MeasureTheory.tendsto_measure_of_le_liminf_measure_of_limsup_measure_le 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} {E₀ E E₁ : Set Ω} (E₀_subset : E₀ ⊆ E) (subset_E₁ : E ⊆ E₁) (nulldiff : μ (E₁ \ E₀) = 0) (h_E₀ : μ E₀ ≤ Filter.liminf (fun i => (μs i) E₀) L) (h_E₁ : Filter.limsup (fun i => (μs i) E₁) L ≤ μ E₁) : Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))
• MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_measure_norm_gt 📋 Mathlib.MeasureTheory.Measure.TightNormed
  {E : Type u_1} {mE : MeasurableSpace E} [NormedAddCommGroup E] [BorelSpace E] [ProperSpace E] {μ : ℕ → MeasureTheory.Measure E} [∀ (i : ℕ), MeasureTheory.IsFiniteMeasure (μ i)] (h : Filter.Tendsto (fun r => Filter.limsup (fun n => (μ n) {x | r < ‖x‖}) Filter.atTop) Filter.atTop (nhds 0)) : MeasureTheory.IsTightMeasureSet (Set.range μ)
• MeasureTheory.isTightMeasureSet_range_iff_tendsto_limsup_measure_norm_gt 📋 Mathlib.MeasureTheory.Measure.TightNormed
  {E : Type u_1} {mE : MeasurableSpace E} [NormedAddCommGroup E] [BorelSpace E] [ProperSpace E] {μ : ℕ → MeasureTheory.Measure E} [∀ (i : ℕ), MeasureTheory.IsFiniteMeasure (μ i)] : MeasureTheory.IsTightMeasureSet (Set.range μ) ↔ Filter.Tendsto (fun r => Filter.limsup (fun n => (μ n) {x | r < ‖x‖}) Filter.atTop) Filter.atTop (nhds 0)
• MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_inner 📋 Mathlib.MeasureTheory.Measure.TightNormed
  {E : Type u_1} {mE : MeasurableSpace E} [NormedAddCommGroup E] (𝕜 : Type u_2) [RCLike 𝕜] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [BorelSpace E] {μ : ℕ → MeasureTheory.Measure E} [∀ (i : ℕ), MeasureTheory.IsFiniteMeasure (μ i)] (h : ∀ (y : E), Filter.Tendsto (fun r => Filter.limsup (fun n => (μ n) {x | r < ‖inner 𝕜 y x‖}) Filter.atTop) Filter.atTop (nhds 0)) : MeasureTheory.IsTightMeasureSet (Set.range μ)
• MeasureTheory.isTightMeasureSet_range_iff_tendsto_limsup_inner 📋 Mathlib.MeasureTheory.Measure.TightNormed
  {E : Type u_1} {mE : MeasurableSpace E} [NormedAddCommGroup E] (𝕜 : Type u_2) [RCLike 𝕜] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [BorelSpace E] {μ : ℕ → MeasureTheory.Measure E} [∀ (i : ℕ), MeasureTheory.IsFiniteMeasure (μ i)] : MeasureTheory.IsTightMeasureSet (Set.range μ) ↔ ∀ (y : E), Filter.Tendsto (fun r => Filter.limsup (fun n => (μ n) {x | r < ‖inner 𝕜 y x‖}) Filter.atTop) Filter.atTop (nhds 0)
• MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_inner_of_norm_eq_one 📋 Mathlib.MeasureTheory.Measure.TightNormed
  {E : Type u_1} {mE : MeasurableSpace E} [NormedAddCommGroup E] (𝕜 : Type u_2) [RCLike 𝕜] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [BorelSpace E] {μ : ℕ → MeasureTheory.Measure E} [∀ (i : ℕ), MeasureTheory.IsFiniteMeasure (μ i)] (h : ∀ (y : E), ‖y‖ = 1 → Filter.Tendsto (fun r => Filter.limsup (fun n => (μ n) {x | r < ‖inner 𝕜 y x‖}) Filter.atTop) Filter.atTop (nhds 0)) : MeasureTheory.IsTightMeasureSet (Set.range μ)
• MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_measureReal_inner_of_norm_eq_one 📋 Mathlib.MeasureTheory.Measure.TightNormed
  {E : Type u_1} {mE : MeasurableSpace E} [NormedAddCommGroup E] (𝕜 : Type u_2) [RCLike 𝕜] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [BorelSpace E] {μ : ℕ → MeasureTheory.Measure E} [∀ (i : ℕ), MeasureTheory.IsFiniteMeasure (μ i)] (h : ∀ (y : E), ‖y‖ = 1 → Filter.Tendsto (fun r => Filter.limsup (fun n => (μ n).real {x | r < ‖inner 𝕜 y x‖}) Filter.atTop) Filter.atTop (nhds 0)) (C : NNReal) (hμ : ∀ᶠ (n : ℕ) in Filter.atTop, (μ n) Set.univ ≤ ↑C) : MeasureTheory.IsTightMeasureSet (Set.range μ)
• MeasureTheory.ae_mem_limsup_atTop_iff 📋 Mathlib.Probability.Martingale.BorelCantelli
  {Ω : Type u_2} {m0 : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration ℕ m0} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] {s : ℕ → Set Ω} (hs : ∀ (n : ℕ), MeasurableSet (s n)) : ∀ᵐ (ω : Ω) ∂μ, ω ∈ Filter.limsup s Filter.atTop ↔ Filter.Tendsto (fun n => ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑ℱ k] ω) Filter.atTop Filter.atTop
• ProbabilityTheory.measure_limsup_eq_one 📋 Mathlib.Probability.BorelCantelli
  {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ℕ → Set Ω} (hsm : ∀ (n : ℕ), MeasurableSet (s n)) (hs : ProbabilityTheory.iIndepSet s μ) (hs' : ∑' (n : ℕ), μ (s n) = ⊤) : μ (Filter.limsup s Filter.atTop) = 1
• ProbabilityTheory.indep_limsup_atBot_self 📋 Mathlib.Probability.Independence.ZeroOne
  {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.iIndep s μ) : ProbabilityTheory.Indep (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) μ
• ProbabilityTheory.indep_limsup_atTop_self 📋 Mathlib.Probability.Independence.ZeroOne
  {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.iIndep s μ) : ProbabilityTheory.Indep (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) μ
• ProbabilityTheory.Kernel.indep_limsup_atBot_self 📋 Mathlib.Probability.Independence.ZeroOne
  {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} [SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.Kernel.iIndep s κ μα) : ProbabilityTheory.Kernel.Indep (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) κ μα
• ProbabilityTheory.Kernel.indep_limsup_atTop_self 📋 Mathlib.Probability.Independence.ZeroOne
  {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} [SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.Kernel.iIndep s κ μα) : ProbabilityTheory.Kernel.Indep (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) κ μα
• ProbabilityTheory.condIndep_limsup_atBot_self 📋 Mathlib.Probability.Independence.ZeroOne
  {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] [StandardBorelSpace Ω] (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.iCondIndep m hm s μ) : ProbabilityTheory.CondIndep m (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) hm μ
• ProbabilityTheory.condIndep_limsup_atTop_self 📋 Mathlib.Probability.Independence.ZeroOne
  {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] [StandardBorelSpace Ω] (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.iCondIndep m hm s μ) : ProbabilityTheory.CondIndep m (Filter.limsup s Filter.atTop) (Filter.limsup s Filter.atTop) hm μ
• ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atBot 📋 Mathlib.Probability.Independence.ZeroOne
  {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.iIndep s μ) {t : Set Ω} (ht_tail : MeasurableSet t) : μ t = 0 ∨ μ t = 1
• ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop 📋 Mathlib.Probability.Independence.ZeroOne
  {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.iIndep s μ) {t : Set Ω} (ht_tail : MeasurableSet t) : μ t = 0 ∨ μ t = 1
• ProbabilityTheory.indep_limsup_self 📋 Mathlib.Probability.Independence.ZeroOne
  {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.iIndep s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun x1 x2 => x1 ⊆ x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a) : ProbabilityTheory.Indep (Filter.limsup s f) (Filter.limsup s f) μ
• ProbabilityTheory.indep_biSup_limsup 📋 Mathlib.Probability.Independence.ZeroOne
  {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {p : Set ι → Prop} {f : Filter ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.iIndep s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) {t : Set ι} (ht : p t) : ProbabilityTheory.Indep (⨆ n ∈ t, s n) (Filter.limsup s f) μ
• ProbabilityTheory.indep_iSup_limsup 📋 Mathlib.Probability.Independence.ZeroOne
  {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.iIndep s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun x1 x2 => x1 ⊆ x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a) : ProbabilityTheory.Indep (⨆ n, s n) (Filter.limsup s f) μ
• ProbabilityTheory.Kernel.indep_limsup_self 📋 Mathlib.Probability.Independence.ZeroOne
  {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.Kernel.iIndep s κ μα) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun x1 x2 => x1 ⊆ x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a) : ProbabilityTheory.Kernel.Indep (Filter.limsup s f) (Filter.limsup s f) κ μα
• ProbabilityTheory.condIndep_limsup_self 📋 Mathlib.Probability.Independence.ZeroOne
  {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} [StandardBorelSpace Ω] (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.iCondIndep m hm s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun x1 x2 => x1 ⊆ x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a) : ProbabilityTheory.CondIndep m (Filter.limsup s f) (Filter.limsup s f) hm μ
• ProbabilityTheory.Kernel.indep_biSup_limsup 📋 Mathlib.Probability.Independence.ZeroOne
  {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} {p : Set ι → Prop} {f : Filter ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.Kernel.iIndep s κ μα) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) {t : Set ι} (ht : p t) : ProbabilityTheory.Kernel.Indep (⨆ n ∈ t, s n) (Filter.limsup s f) κ μα
• ProbabilityTheory.Kernel.indep_iSup_limsup 📋 Mathlib.Probability.Independence.ZeroOne
  {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.Kernel.iIndep s κ μα) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun x1 x2 => x1 ⊆ x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a) : ProbabilityTheory.Kernel.Indep (⨆ n, s n) (Filter.limsup s f) κ μα
• ProbabilityTheory.condIndep_biSup_limsup 📋 Mathlib.Probability.Independence.ZeroOne
  {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {p : Set ι → Prop} {f : Filter ι} [StandardBorelSpace Ω] (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.iCondIndep m hm s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) {t : Set ι} (ht : p t) : ProbabilityTheory.CondIndep m (⨆ n ∈ t, s n) (Filter.limsup s f) hm μ
• ProbabilityTheory.condIndep_iSup_limsup 📋 Mathlib.Probability.Independence.ZeroOne
  {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} [StandardBorelSpace Ω] (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.iCondIndep m hm s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun x1 x2 => x1 ⊆ x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a) : ProbabilityTheory.CondIndep m (⨆ n, s n) (Filter.limsup s f) hm μ
• ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup 📋 Mathlib.Probability.Independence.ZeroOne
  {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.iIndep s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun x1 x2 => x1 ⊆ x2) ns) (hnsp : ∀ (a : β), p (ns a)) (hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a) {t : Set Ω} (ht_tail : MeasurableSet t) : μ t = 0 ∨ μ t = 1
• ProbabilityTheory.indep_iSup_directed_limsup 📋 Mathlib.Probability.Independence.ZeroOne
  {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_4} {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι} (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.iIndep s μ) (hf : ∀ (t : Set ι), p t → tᶜ ∈ f) (hns : Directed (fun x1 x2 => x1 ⊆ x2) ns) (hnsp : ∀ (a : β), p (ns a)) : ProbabilityTheory.Indep (⨆ a, ⨆ n ∈ ns a, s n) (Filter.limsup s f) μ
• ProbabilityTheory.Kernel.measure_zero_or_one_of_measurableSet_limsup_atBot 📋 Mathlib.Probability.Independence.ZeroOne
  {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} [SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.Kernel.iIndep s κ μα) {t : Set Ω} (ht_tail : MeasurableSet t) : ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1
• ProbabilityTheory.Kernel.measure_zero_or_one_of_measurableSet_limsup_atTop 📋 Mathlib.Probability.Independence.ZeroOne
  {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω} {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} [SemilatticeSup ι] [NoMaxOrder ι] [Nonempty ι] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.Kernel.iIndep s κ μα) {t : Set Ω} (ht_tail : MeasurableSet t) : ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1
• ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atBot 📋 Mathlib.Probability.Independence.ZeroOne
  {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] [StandardBorelSpace Ω] (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] (h_le : ∀ (n : ι), s n ≤ m0) (h_indep : ProbabilityTheory.iCondIndep m hm s μ) {t : Set Ω} (ht_tail : MeasurableSet t) : ∀ᵐ (ω : Ω) ∂μ, μ[t.indicator fun ω => 1 | m] ω = 0 ∨ μ[t.indicator fun ω => 1 | m] ω = 1

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59