Loogle!

Result

Found 177 declarations mentioning Filter.liminf.

• Filter.liminf 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (u : β → α) (f : Filter β) : α
• Filter.liminf_const 📋 Mathlib.Order.LiminfLimsup
  {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} [f.NeBot] (b : β) : Filter.liminf (fun x => b) f = b
• Filter.bliminf_true 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] (f : Filter β) (u : β → α) : (Filter.bliminf u f fun x => True) = Filter.liminf u f
• Filter.liminf_comp 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] (u : β → α) (v : γ → β) (f : Filter γ) : Filter.liminf (u ∘ v) f = Filter.liminf u (Filter.map v f)
• Filter.liminf_congr 📋 Mathlib.Order.LiminfLimsup
  {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β} (h : ∀ᶠ (a : α) in f, u a = v a) : Filter.liminf u f = Filter.liminf v f
• Filter.liminf_nat_add 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} [ConditionallyCompleteLattice α] (f : ℕ → α) (k : ℕ) : Filter.liminf (fun i => f (i + k)) Filter.atTop = Filter.liminf f Filter.atTop
• Filter.liminf_top_eq_iInf 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteLattice α] (u : β → α) : Filter.liminf u ⊤ = ⨅ i, u i
• Filter.bliminf_eq_liminf 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop} : Filter.bliminf u f p = Filter.liminf u (f ⊓ Filter.principal {x | p x})
• Filter.cofinite.liminf_set_eq 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {ι : Type u_4} {s : ι → Set α} : Filter.liminf s Filter.cofinite = {x | {n | x ∉ s n}.Finite}
• Filter.iInf_le_liminf 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {u : β → α} : ⨅ n, u n ≤ Filter.liminf u f
• Filter.mem_liminf_iff_eventually_mem 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {ι : Type u_4} {s : ι → Set α} {𝓕 : Filter ι} {a : α} : a ∈ Filter.liminf 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.liminf_eq 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} : Filter.liminf u f = sSup {a | ∀ᶠ (n : β) in f, a ≤ u n}
• 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.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.liminf_top_eq_ciInf 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {u : β → α} [Nonempty β] (hu : BddBelow (Set.range u)) : Filter.liminf u ⊤ = ⨅ i, u i
• Filter.liminf_bot 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : β → α) : Filter.liminf f ⊥ = ⊤
• Filter.liminf_sdiff 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteBooleanAlgebra α] (f : Filter β) (u : β → α) [f.NeBot] (a : α) : Filter.liminf u f \ a = Filter.liminf (fun b => u b \ a) 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.liminf_eq_sSup_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.liminf f v = sSup Set.univ
• Filter.liminf_eq_iSup_iInf_of_nat' 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} [CompleteLattice α] {u : ℕ → α} : Filter.liminf u Filter.atTop = ⨆ n, ⨅ i, u (i + n)
• Filter.liminf_eq_sSup_sInf 📋 Mathlib.Order.LiminfLimsup
  {ι : Type u_6} {R : Type u_7} (F : Filter ι) [CompleteLattice R] (a : ι → R) : Filter.liminf a F = sSup ((fun I => sInf (a '' I)) '' F.sets)
• Filter.liminf_le_of_frequently_le' 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_6} {β : Type u_7} [CompleteLattice β] {f : Filter α} {u : α → β} {x : β} (h : ∃ᶠ (a : α) in f, u a ≤ x) : Filter.liminf u f ≤ x
• Filter.liminf_eq_iSup_iInf_of_nat 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} [CompleteLattice α] {u : ℕ → α} : Filter.liminf u Filter.atTop = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), u i
• Filter.bliminf_inf_not 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {p : β → Prop} {u : β → α} : (Filter.bliminf u f p ⊓ Filter.bliminf u f fun x => ¬p x) = Filter.liminf u f
• Filter.bliminf_not_inf 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {p : β → Prop} {u : β → α} : (Filter.bliminf u f fun x => ¬p x) ⊓ Filter.bliminf u f p = Filter.liminf u f
• Filter.liminf_sup_filter 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} {g : Filter β} : Filter.liminf u (f ⊔ g) = Filter.liminf u f ⊓ Filter.liminf u g
• Filter.sup_liminf 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} (a : α) : a ⊔ Filter.liminf u f = Filter.liminf (fun x => a ⊔ u x) f
• Filter.iSup_liminf_le_liminf_iSup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [CompleteLattice α] {f : Filter β} {u : ι → β → α} : ⨆ i, Filter.liminf (u i) f ≤ Filter.liminf (fun b => ⨆ i, u i b) f
• Filter.inf_liminf 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} [f.NeBot] (a : α) : a ⊓ Filter.liminf u f = Filter.liminf (fun x => a ⊓ u x) f
• Filter.le_liminf_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, a ≤ u n) : a ≤ Filter.liminf u f
• Filter.liminf_le_of_frequently_le 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {ι : Type u_4} [ConditionallyCompleteLattice α] {f : Filter ι} {u : ι → α} {a : α} (hu : ∃ᶠ (i : ι) in f, u i ≤ a) (hu_le : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u := by isBoundedDefault) : Filter.liminf u f ≤ a
• Filter.liminf_const_top 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} : Filter.liminf (fun x => ⊤) f = ⊤
• Filter.eventually_lt_of_lt_liminf 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} {f : Filter α} [ConditionallyCompleteLinearOrder β] {u : α → β} {b : β} (h : b < Filter.liminf u f) (hu : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u := by isBoundedDefault) : ∀ᶠ (a : α) in f, b < u a
• Filter.frequently_lt_of_liminf_lt 📋 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 : Filter.liminf u f < b) : ∃ᶠ (x : α) in f, u x < b
• CompleteLatticeHom.apply_liminf_iterate 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} [CompleteLattice α] (f : CompleteLatticeHom α α) (a : α) : f (Filter.liminf (fun n => (⇑f)^[n] a) Filter.atTop) = Filter.liminf (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.liminf_le_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, b ≤ u n) → b ≤ a) : Filter.liminf u f ≤ a
• Filter.HasBasis.liminf_eq_sSup_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.liminf f v = sSup (⋃ j, ⋂ i, Set.Iic (f ↑i))
• Filter.liminf_le_liminf_of_le 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_6} {β : Type u_7} [ConditionallyCompleteLattice β] {f g : Filter α} (h : g ≤ f) {u : α → β} (hf : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u := by isBoundedDefault) (hg : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) g u := by isBoundedDefault) : Filter.liminf u f ≤ Filter.liminf u g
• Filter.Tendsto.liminf_le_liminf_comp 📋 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.liminf u g ≤ Filter.liminf (u ∘ v) f
• Filter.liminf_piecewise 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteDistribLattice α] {f : Filter β} {u : β → α} {s : Set β} [DecidablePred fun x => x ∈ s] {v : β → α} : Filter.liminf (s.piecewise u v) f = (Filter.bliminf u f fun x => x ∈ s) ⊓ Filter.bliminf v f fun x => x ∉ s
• Filter.HasBasis.liminf_eq_iSup_iInf 📋 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.liminf u f = ⨆ i, ⨆ (_ : p i), ⨅ a ∈ s i, u a
• Filter.bliminf_eq_liminf_subtype 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] {f : Filter β} {u : β → α} {p : β → Prop} : Filter.bliminf u f p = Filter.liminf (u ∘ Subtype.val) (Filter.comap Subtype.val f)
• Filter.liminf_eq_iSup_iInf 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : Filter β} {u : β → α} : Filter.liminf u f = ⨆ s ∈ f, ⨅ a ∈ s, u a
• Filter.liminf_le_liminf 📋 Mathlib.Order.LiminfLimsup
  {β : Type u_2} {α : Type u_6} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β} (h : ∀ᶠ (a : α) in f, u a ≤ v a) (hu : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u := by isBoundedDefault) (hv : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v := by isBoundedDefault) : Filter.liminf u f ≤ Filter.liminf v f
• 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
• Filter.le_liminf_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.liminf u f ↔ ∀ y < x, ∀ᶠ (a : α) in f, y < u a
• Filter.liminf_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.liminf u f ≤ x ↔ ∀ y > x, ∃ᶠ (a : α) in f, u a < y
• Filter.exists_lt_of_le_liminf 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} [ConditionallyCompleteLinearOrder α] [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : ℕ → α} (hu_bdd : Filter.IsBoundedUnder GE.ge Filter.atTop u) (hu : x ≤ Filter.liminf u Filter.atTop) (hε : ε < 0) : ∃ n, x + ε < u ↑n
• Filter.le_liminf_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.liminf u f ↔ ∀ y < x, ∀ᶠ (a : α) in f, y ≤ u a
• Filter.liminf_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.liminf u f ≤ x ↔ ∀ y > x, ∃ᶠ (a : α) in f, u a ≤ y
• Filter.eventually_add_neg_lt_of_le_liminf 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLinearOrder α] [Preorder β] [AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : β → α} (hu_bdd : Filter.IsBoundedUnder GE.ge Filter.atTop u) (hu : x ≤ Filter.liminf u Filter.atTop) (hε : ε < 0) : ∀ᶠ (b : β) in Filter.atTop, x + ε < u b
• liminf_finset_inf' 📋 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.liminf (fun a => s.inf' hs fun i => F i a) f = s.inf' hs fun i => Filter.liminf (F i) f
• liminf_finset_inf 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [ConditionallyCompleteLinearOrder β] [OrderTop β] {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.liminf (fun a => s.inf fun i => F i a) f = s.inf fun i => Filter.liminf (F i) f
• liminf_min 📋 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.liminf (fun a => min (u a) (v a)) f = min (Filter.liminf u f) (Filter.liminf v f)
• Filter.HasBasis.liminf_eq_ciSup_ciInf 📋 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, BddBelow (Set.range fun i => f ↑i)) : Filter.liminf f v = ⨆ j, ⨅ i, f ↑i
• Filter.HasBasis.liminf_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.liminf f v = if ∃ j, s ↑j = ∅ then sSup Set.univ else if ∀ (j : Subtype p), ¬BddBelow (Set.range fun i => f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i
• OrderIso.liminf_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.liminf u f) = Filter.liminf (fun x => g (u x)) f
• Filter.Tendsto.liminf_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.liminf u f = a
• MapClusterPt.liminf_le 📋 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) : Filter.liminf u f ≤ x
• eventually_liminf_le 📋 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, Filter.liminf u f ≤ u b
• MapClusterPt.liminf 📋 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.liminf 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)
• isLeast_mapClusterPt_liminf 📋 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) : IsLeast {x | MapClusterPt x f u} (Filter.liminf u f)
• exists_seq_tendsto_liminf 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α] {f : Filter β} [f.NeBot] {u : β → α} [f.IsCountablyGenerated] (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.liminf u f)) ∧ Filter.Tendsto x Filter.atTop f
• liminf_eq_top 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [CompleteLinearOrder α] [TopologicalSpace α] [FirstCountableTopology α] [OrderTopology α] {f : Filter β} [CountableInterFilter f] {u : β → α} : Filter.liminf 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_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_decr : Antitone 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.liminf f F
• Monotone.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_incr : Monotone 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.liminf f F
• 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_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_incr : Monotone 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.liminf (f ∘ a) F
• Antitone.liminf_nhdsGT_eq_iSup₂ 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [CompleteLattice β] {f : α → β} [NoMaxOrder α] (hf : Antitone f) (a : α) : Filter.liminf f (nhdsWithin a (Set.Ioi a)) = ⨆ r, ⨆ (_ : r > a), f r
• Monotone.liminf_nhdsLT_eq_iSup₂ 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [CompleteLattice β] {f : α → β} [NoMinOrder α] (hf : Monotone f) (a : α) : Filter.liminf f (nhdsWithin a (Set.Iio a)) = ⨆ r, ⨆ (_ : r < a), f r
• Antitone.liminf_nhdsGT_eq_iSup₂_of_exists_gt 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [CompleteLattice β] {f : α → β} (hf : Antitone f) (a : α) (hb : ∃ b, a < b) : Filter.liminf f (nhdsWithin a (Set.Ioi a)) = ⨆ r, ⨆ (_ : r > a), f r
• Monotone.liminf_nhdsLT_eq_iSup₂_of_exists_lt 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] [CompleteLattice β] {f : α → β} (hf : Monotone f) (a : α) (hb : ∃ b, b < a) : Filter.liminf f (nhdsWithin a (Set.Iio 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_liminf 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} {f : Filter ι} {u : ι → NNReal} (hf : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u) : ↑(Filter.liminf u f) = Filter.liminf (fun i => ↑(u i)) f
• ENNReal.liminf_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.liminf (fun i => (u i).toReal) f = (Filter.liminf u f).toReal
• ENNReal.liminf_sub_const 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} (F : Filter ι) [F.NeBot] (f : ι → ENNReal) (c : ENNReal) : Filter.liminf (fun i => f i - c) F = Filter.liminf f F - c
• 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.exists_frequently_lt_of_liminf_ne_top 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} {l : Filter ι} {x : ι → ℝ} (hx : Filter.liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤) : ∃ R, ∃ᶠ (n : ι) in l, x n < R
• ENNReal.exists_frequently_lt_of_liminf_ne_top' 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} {l : Filter ι} {x : ι → ℝ} (hx : Filter.liminf (fun n => ↑(Real.nnabs (x n))) l ≠ ⊤) : ∃ R, ∃ᶠ (n : ι) in l, R < x n
• ENNReal.liminf_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.liminf (f + g) u = Filter.liminf g u
• ENNReal.liminf_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.liminf (f + g) u = Filter.liminf f u
• ENNReal.le_liminf_mul 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} {f : Filter ι} {u v : ι → ENNReal} : Filter.liminf u f * Filter.liminf v f ≤ Filter.liminf (u * v) f
• 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.exists_upcrossings_of_not_bounded_under 📋 Mathlib.Topology.Instances.ENNReal.Lemmas
  {ι : Type u_4} {l : Filter ι} {x : ι → ℝ} (hf : Filter.liminf (fun i => ↑(Real.nnabs (x i))) l ≠ ⊤) (hbdd : ¬Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun i => |x i|) : ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
• 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.tsum_eq_liminf_sum_nat 📋 Mathlib.Topology.Algebra.InfiniteSum.ENNReal
  {f : ℕ → ENNReal} : ∑' (i : ℕ), f i = Filter.liminf (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop
• LowerSemicontinuous.le_liminf 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {γ : Type u_4} [CompleteLinearOrder γ] {f : α → γ} : LowerSemicontinuous f → ∀ (x : α), f x ≤ Filter.liminf f (nhds x)
• lowerSemicontinuous_iff_le_liminf 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {γ : Type u_4} [CompleteLinearOrder γ] {f : α → γ} : LowerSemicontinuous f ↔ ∀ (x : α), f x ≤ Filter.liminf f (nhds x)
• LowerSemicontinuousAt.le_liminf 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_4} [CompleteLinearOrder γ] {f : α → γ} : LowerSemicontinuousAt f x → f x ≤ Filter.liminf f (nhds x)
• lowerSemicontinuousAt_iff_le_liminf 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {x : α} {γ : Type u_4} [CompleteLinearOrder γ] {f : α → γ} : LowerSemicontinuousAt f x ↔ f x ≤ Filter.liminf f (nhds x)
• LowerSemicontinuousWithinAt.le_liminf 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_4} [CompleteLinearOrder γ] {f : α → γ} : LowerSemicontinuousWithinAt f s x → f x ≤ Filter.liminf f (nhdsWithin x s)
• lowerSemicontinuousWithinAt_iff_le_liminf 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_4} [CompleteLinearOrder γ] {f : α → γ} : LowerSemicontinuousWithinAt f s x ↔ f x ≤ Filter.liminf f (nhdsWithin x s)
• LowerSemicontinuousOn.le_liminf 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_4} [CompleteLinearOrder γ] {f : α → γ} : LowerSemicontinuousOn f s → ∀ x ∈ s, f x ≤ Filter.liminf f (nhdsWithin x s)
• lowerSemicontinuousOn_iff_le_liminf 📋 Mathlib.Topology.Semicontinuity.Basic
  {α : Type u_1} [TopologicalSpace α] {s : Set α} {γ : Type u_4} [CompleteLinearOrder γ] {f : α → γ} : LowerSemicontinuousOn f s ↔ ∀ x ∈ s, f x ≤ Filter.liminf f (nhdsWithin x s)
• 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_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.liminf (fun x => c * u x) f = c * Filter.liminf u 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_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.liminf_add_top_of_ne_bot 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u v : α → EReal} (h : Filter.liminf u f = ⊤) (h' : Filter.liminf v f ≠ ⊥) : Filter.liminf (u + v) f = ⊤
• EReal.le_liminf_add 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u v : α → EReal} : Filter.liminf u f + Filter.liminf v f ≤ Filter.liminf (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.liminf_add_gt_of_gt 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u v : α → EReal} {a b : EReal} (ha : a < Filter.liminf u f) (hb : b < Filter.liminf v f) : a + b < Filter.liminf (u + v) f
• 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.le_liminf_mul 📋 Mathlib.Topology.Instances.EReal.Lemmas
  {α : Type u_3} {f : Filter α} {u v : α → EReal} (hu : 0 ≤ᶠ[f] u) (hv : 0 ≤ᶠ[f] v) : Filter.liminf u f * Filter.liminf v f ≤ Filter.liminf (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.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_liminf 📋 Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
  {α : Type u_1} [MeasurableSpace α] {s : ℕ → Set α} (hs : ∀ (n : ℕ), MeasurableSet (s n)) : MeasurableSet (Filter.liminf s Filter.atTop)
• MeasureTheory.liminf_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.liminf s Filter.atTop =ᵐ[μ] t
• MeasureTheory.measure_liminf_atTop_eq_zero 📋 Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
  {α : Type u_1} {F : Type u_3} [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : ℕ → Set α} (h : ∑' (i : ℕ), μ (s i) ≠ ⊤) : μ (Filter.liminf s Filter.atTop) = 0
• MeasureTheory.measure_liminf_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} [Infinite ι] {s : ι → Set α} (h : ∑' (i : ι), μ (s i) ≠ ⊤) : μ (Filter.liminf s Filter.cofinite) = 0
• MeasureTheory.Measure.QuasiMeasurePreserving.liminf_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.liminf (fun n => (Set.preimage f)^[n] s) Filter.atTop =ᵐ[μ] s
• Measurable.liminf 📋 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.liminf (fun i => f i x) Filter.atTop
• Measurable.liminf' 📋 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 : ι → δ → α} {v : Filter ι} (hf : ∀ (i : ι), Measurable (f i)) {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasCountableBasis p s) (hs : ∀ (j : ι'), (s j).Countable) : Measurable fun x => Filter.liminf (fun x_1 => f x_1 x) v
• MeasureTheory.lintegral_liminf_le 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Add
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_3} {f : ι → α → ENNReal} {u : Filter ι} [u.IsCountablyGenerated] (h_meas : ∀ (i : ι), Measurable (f i)) : ∫⁻ (a : α), Filter.liminf (fun i => f i a) u ∂μ ≤ Filter.liminf (fun i => ∫⁻ (a : α), f i a ∂μ) u
• MeasureTheory.lintegral_liminf_le' 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Add
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_3} {f : ι → α → ENNReal} {u : Filter ι} [u.IsCountablyGenerated] (h_meas : ∀ (i : ι), AEMeasurable (f i) μ) : ∫⁻ (a : α), Filter.liminf (fun i => f i a) u ∂μ ≤ Filter.liminf (fun i => ∫⁻ (a : α), f i a ∂μ) u
• NNReal.toReal_liminf 📋 Mathlib.Order.Filter.ENNReal
  {ι : Type u_1} {f : Filter ι} {u : ι → NNReal} : Filter.liminf (fun i => ↑(u i)) f = ↑(Filter.liminf u f)
• Real.liminf_of_not_isBoundedUnder 📋 Mathlib.Order.Filter.ENNReal
  {ι : Type u_1} {f : Filter ι} {u : ι → ℝ} (hf : ¬Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) : Filter.liminf u f = 0
• Real.liminf_of_not_isCoboundedUnder 📋 Mathlib.Order.Filter.ENNReal
  {ι : Type u_1} {f : Filter ι} {u : ι → ℝ} (hf : ¬Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u) : Filter.liminf u f = 0
• NNReal.liminf_of_not_isCoboundedUnder 📋 Mathlib.Order.Filter.ENNReal
  {ι : Type u_1} {f : Filter ι} {u : ι → NNReal} (hf : ¬Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u) : Filter.liminf u f = 0
• ENNReal.liminf_const_mul_of_ne_top 📋 Mathlib.Order.Filter.ENNReal
  {α : Type u_1} {f : Filter α} [f.NeBot] {u : α → ENNReal} {a : ENNReal} (ha_top : a ≠ ⊤) : Filter.liminf (fun x => a * u x) f = a * Filter.liminf u f
• ENNReal.liminf_mul_const_of_ne_top 📋 Mathlib.Order.Filter.ENNReal
  {α : Type u_1} {f : Filter α} [f.NeBot] {u : α → ENNReal} {a : ENNReal} (ha_top : a ≠ ⊤) : Filter.liminf (fun x => u x * a) f = a * Filter.liminf 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.liminf_const_mul_of_ne_zero_of_ne_top 📋 Mathlib.Order.Filter.ENNReal
  {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal} (ha₀ : a ≠ 0) (ha_top : a ≠ ⊤) : Filter.liminf (fun x => a * u x) f = a * Filter.liminf u f
• ENNReal.liminf_mul_const_of_ne_zero_of_ne_top 📋 Mathlib.Order.Filter.ENNReal
  {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal} (ha₀ : a ≠ 0) (ha_top : a ≠ ⊤) : Filter.liminf (fun x => u x * a) f = a * Filter.liminf u f
• ENNReal.essSup_liminf_le 📋 Mathlib.MeasureTheory.Function.EssSup
  {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_3} [Countable ι] [Preorder ι] (f : ι → α → ENNReal) : essSup (fun x => Filter.liminf (fun n => f n x) Filter.atTop) μ ≤ Filter.liminf (fun n => essSup (fun x => f n x) μ) Filter.atTop
• MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
  {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] {R : NNReal} {p : ENNReal} (hp : p ≠ 0) {f : ℕ → α → E} (hfmeas : ∀ (n : ℕ), Measurable (f n)) (hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R) : ∀ᵐ (x : α) ∂μ, Filter.liminf (fun n => ‖f n x‖ₑ) Filter.atTop < ⊤
• MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd 📋 Mathlib.MeasureTheory.Function.LpSeminorm.Basic
  {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E] {R : NNReal} {p : ENNReal} {f : ℕ → α → E} (hfmeas : ∀ (n : ℕ), Measurable (f n)) (hbdd : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R) : ∀ᵐ (x : α) ∂μ, Filter.liminf (fun n => ‖f n x‖ₑ ^ p.toReal) Filter.atTop < ⊤
• MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm 📋 Mathlib.MeasureTheory.Function.LpSpace.Complete
  {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [SeminormedAddGroup E] {f : ℕ → α → E} (hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) (f_lim : α → E) (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))) : MeasureTheory.eLpNorm f_lim p μ ≤ Filter.liminf (fun n => MeasureTheory.eLpNorm (f n) p μ) Filter.atTop
• MeasureTheory.Lp.eLpNorm'_lim_le_liminf_eLpNorm' 📋 Mathlib.MeasureTheory.Function.LpSpace.Complete
  {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [SeminormedAddGroup E] {f : ℕ → α → E} {p : ℝ} (hp_pos : 0 < p) (hf : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) {f_lim : α → E} (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))) : MeasureTheory.eLpNorm' f_lim p μ ≤ Filter.liminf (fun n => MeasureTheory.eLpNorm' (f n) p μ) Filter.atTop
• MeasureTheory.Lp.eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top 📋 Mathlib.MeasureTheory.Function.LpSpace.Complete
  {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [SeminormedAddGroup E] {ι : Type u_3} [Nonempty ι] [Countable ι] [LinearOrder ι] {f : ι → α → E} {f_lim : α → E} (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))) : MeasureTheory.eLpNorm f_lim ⊤ μ ≤ Filter.liminf (fun n => MeasureTheory.eLpNorm (f n) ⊤ μ) Filter.atTop
• MeasureTheory.Lp.eLpNorm_exponent_top_lim_eq_essSup_liminf 📋 Mathlib.MeasureTheory.Function.LpSpace.Complete
  {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [SeminormedAddGroup E] {ι : Type u_3} [Nonempty ι] [LinearOrder ι] {f : ι → α → E} {f_lim : α → E} (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))) : MeasureTheory.eLpNorm f_lim ⊤ μ = essSup (fun x => Filter.liminf (fun m => ‖f m x‖ₑ) Filter.atTop) μ
• MeasureTheory.Lp.eLpNorm'_lim_eq_lintegral_liminf 📋 Mathlib.MeasureTheory.Function.LpSpace.Complete
  {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [SeminormedAddGroup E] {ι : Type u_3} [Nonempty ι] [LinearOrder ι] {f : ι → α → E} {p : ℝ} {f_lim : α → E} (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))) : MeasureTheory.eLpNorm' f_lim p μ = (∫⁻ (a : α), Filter.liminf (fun x => ‖f x a‖ₑ ^ p) Filter.atTop ∂μ) ^ (1 / p)
• MeasureTheory.integrable_of_tendsto 📋 Mathlib.MeasureTheory.Function.L1Space.Integrable
  {G : ℕ → ℝ → ℝ} {f : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} (hGf : ∀ᵐ (x : ℝ) ∂μ, Filter.Tendsto (fun n => G n x) Filter.atTop (nhds (f x))) (hG : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (G n) μ) (hG' : Filter.liminf (fun n => ∫⁻ (x : ℝ), ‖G n x‖ₑ ∂μ) Filter.atTop ≠ ⊤) : MeasureTheory.Integrable f μ
• MeasureTheory.lintegral_enorm_le_liminf_of_tendsto 📋 Mathlib.MeasureTheory.Function.L1Space.Integrable
  {G : ℕ → ℝ → ℝ} {f : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} (hGf : ∀ᵐ (x : ℝ) ∂μ, Filter.Tendsto (fun n => G n x) Filter.atTop (nhds (f x))) (hG : ∀ (n : ℕ), AEMeasurable (fun x => ‖G n x‖ₑ) μ) : ∫⁻ (x : ℝ), ‖f x‖ₑ ∂μ ≤ Filter.liminf (fun n => ∫⁻ (x : ℝ), ‖G n x‖ₑ ∂μ) Filter.atTop
• FormalMultilinearSeries.radius_eq_liminf 📋 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.liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) Filter.atTop
• spectrum.spectralRadius_le_liminf_pow_nnnorm_pow_one_div 📋 Mathlib.Analysis.Normed.Algebra.Spectrum
  (𝕜 : Type u_1) {A : Type u_2} [NormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (a : A) : spectralRadius 𝕜 a ≤ Filter.liminf (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop
• MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable
  {f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b) (hf : MonotoneOn f (Set.Icc a b)) : ∃ G, (∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), Filter.Tendsto (fun n => G n x) Filter.atTop (nhds (deriv f x))) ∧ (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (G n) (MeasureTheory.volume.restrict (Set.Icc a b))) ∧ Filter.liminf (fun n => ∫⁻ (x : ℝ) in Set.Icc a b, ‖G n x‖ₑ) Filter.atTop ≤ ENNReal.ofReal (f b - f a)
• MeasureTheory.Measure.mkMetric_le_liminf_tsum 📋 Mathlib.MeasureTheory.Measure.Hausdorff
  {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {β : Type u_4} {ι : β → Type u_5} [∀ (n : β), Countable (ι n)] (s : Set X) {l : Filter β} (r : β → ENNReal) (hr : Filter.Tendsto r l (nhds 0)) (t : (n : β) → ι n → Set X) (ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), Metric.ediam (t n i) ≤ r n) (hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i) (m : ENNReal → ENNReal) : (MeasureTheory.Measure.mkMetric m) s ≤ Filter.liminf (fun n => ∑' (i : ι n), m (Metric.ediam (t n i))) l
• MeasureTheory.Measure.mkMetric_le_liminf_sum 📋 Mathlib.MeasureTheory.Measure.Hausdorff
  {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {β : Type u_4} {ι : β → Type u_5} [hι : (n : β) → Fintype (ι n)] (s : Set X) {l : Filter β} (r : β → ENNReal) (hr : Filter.Tendsto r l (nhds 0)) (t : (n : β) → ι n → Set X) (ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), Metric.ediam (t n i) ≤ r n) (hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i) (m : ENNReal → ENNReal) : (MeasureTheory.Measure.mkMetric m) s ≤ Filter.liminf (fun n => ∑ i, m (Metric.ediam (t n i))) l
• MeasureTheory.Measure.hausdorffMeasure_le_liminf_tsum 📋 Mathlib.MeasureTheory.Measure.Hausdorff
  {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {β : Type u_4} {ι : β → Type u_5} [∀ (n : β), Countable (ι n)] (d : ℝ) (s : Set X) {l : Filter β} (r : β → ENNReal) (hr : Filter.Tendsto r l (nhds 0)) (t : (n : β) → ι n → Set X) (ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), Metric.ediam (t n i) ≤ r n) (hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i) : (MeasureTheory.Measure.hausdorffMeasure d) s ≤ Filter.liminf (fun n => ∑' (i : ι n), Metric.ediam (t n i) ^ d) l
• MeasureTheory.Measure.hausdorffMeasure_le_liminf_sum 📋 Mathlib.MeasureTheory.Measure.Hausdorff
  {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {β : Type u_4} {ι : β → Type u_5} [(n : β) → Fintype (ι n)] (d : ℝ) (s : Set X) {l : Filter β} (r : β → ENNReal) (hr : Filter.Tendsto r l (nhds 0)) (t : (n : β) → ι n → Set X) (ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), Metric.ediam (t n i) ≤ r n) (hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i) : (MeasureTheory.Measure.hausdorffMeasure d) s ≤ Filter.liminf (fun n => ∑ i, Metric.ediam (t n i) ^ d) l
• 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
• le_liminf_mul 📋 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 f * Filter.liminf v f ≤ Filter.liminf (u * 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
• liminf_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) (cobdd : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) F f) (bdd_below : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) F f) : Filter.liminf (fun i => f i + c) F = Filter.liminf f F + c
• liminf_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) (cobdd : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) F f) (bdd_below : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) F f) : Filter.liminf (fun i => c + f i) F = c + Filter.liminf f F
• liminf_sub_const 📋 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] (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.liminf (fun i => f i - c) F = Filter.liminf 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_liminf_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.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 f + Filter.liminf v f ≤ Filter.liminf (u + v) 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
• BoundedContinuousFunction.tendsto_integral_of_forall_integral_le_liminf_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 → ∫ (x : X), f x ∂μ ≤ Filter.liminf (fun i => ∫ (x : X), f x ∂μs i) L) (f : BoundedContinuousFunction X ℝ) : Filter.Tendsto (fun i => ∫ (x : X), f x ∂μs i) L (nhds (∫ (x : X), f x ∂μ))
• MeasureTheory.tendsto_of_uncrossing_lt_top 📋 Mathlib.Probability.Martingale.Convergence
  {Ω : Type u_1} {f : ℕ → Ω → ℝ} {ω : Ω} (hf₁ : Filter.liminf (fun n => ↑‖f n ω‖₊) Filter.atTop < ⊤) (hf₂ : ∀ (a b : ℚ), a < b → MeasureTheory.upcrossings (↑a) (↑b) f ω < ⊤) : ∃ c, Filter.Tendsto (fun n => f n ω) Filter.atTop (nhds c)
• MeasureTheory.tendsto_of_forall_isOpen_le_liminf_nat 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ℕ → MeasureTheory.ProbabilityMeasure Ω} (h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) Filter.atTop) : Filter.Tendsto (fun i => μs i) Filter.atTop (nhds μ)
• MeasureTheory.tendsto_of_forall_isOpen_le_liminf 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2} {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} {L : Filter ι} [L.IsCountablyGenerated] (h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) L) : Filter.Tendsto (fun i => μs i) L (nhds μ)
• MeasureTheory.tendsto_of_forall_isOpen_le_liminf_nat' 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ℕ → MeasureTheory.ProbabilityMeasure Ω} (h_opens : ∀ (G : Set Ω), IsOpen G → ↑μ G ≤ Filter.liminf (fun i => ↑(μs i) G) Filter.atTop) : Filter.Tendsto (fun i => μs i) Filter.atTop (nhds μ)
• MeasureTheory.ProbabilityMeasure.le_liminf_measure_open_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 μ)) {G : Set Ω} (G_open : IsOpen G) : ↑μ G ≤ Filter.liminf (fun i => ↑(μs i) G) L
• MeasureTheory.tendsto_of_forall_isOpen_le_liminf' 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2} {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} {L : Filter ι} [L.IsCountablyGenerated] (h_opens : ∀ (G : Set Ω), IsOpen G → ↑μ G ≤ Filter.liminf (fun i => ↑(μs i) G) L) : Filter.Tendsto (fun i => μs i) 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.lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {μs : ℕ → MeasureTheory.Measure Ω} {f : Ω → ℝ} (f_cont : Continuous f) (f_nn : 0 ≤ f) (h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) Filter.atTop) : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ Filter.liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) Filter.atTop
• MeasureTheory.tendsto_measure_of_null_frontier 📋 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)] (h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) L) {E : Set Ω} (E_nullbdry : μ (frontier E) = 0) : Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))
• MeasureTheory.le_liminf_measure_open_of_forall_tendsto_measure 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [MeasurableSpace Ω] [TopologicalSpace Ω] [TopologicalSpace.PseudoMetrizableSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {μs : ι → MeasureTheory.Measure Ω} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] (h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))) (G : Set Ω) (G_open : IsOpen G) : μ G ≤ Filter.liminf (fun i => (μs i) G) L
• 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.integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure 📋 Mathlib.MeasureTheory.Measure.Portmanteau
  {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {μs : ℕ → MeasureTheory.Measure Ω} [∀ (i : ℕ), MeasureTheory.IsProbabilityMeasure (μs i)] {f : BoundedContinuousFunction Ω ℝ} (f_nn : 0 ≤ f) (h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ Filter.liminf (fun i => (μs i) G) Filter.atTop) : ∫ (x : Ω), f x ∂μ ≤ Filter.liminf (fun i => ∫ (x : Ω), f x ∂μs i) Filter.atTop

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