Loogle!

Result

Found 332 declarations mentioning Filter.Frequently. Of these, only the first 200 are shown.

• Filter.Frequently 📋 Mathlib.Order.Filter.Defs
  {α : Type u_1} (p : α → Prop) (f : Filter α) : Prop
• Filter.frequently_false 📋 Mathlib.Order.Filter.Basic
  {α : Type u} (f : Filter α) : ¬∃ᶠ (x : α) in f, False
• Filter.frequently_true_iff_neBot 📋 Mathlib.Order.Filter.Basic
  {α : Type u} (f : Filter α) : (∃ᶠ (x : α) in f, True) ↔ f.NeBot
• Filter.frequently_bot 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p : α → Prop} : ¬∃ᶠ (x : α) in ⊥, p x
• Filter.frequently_const 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} [f.NeBot] {p : Prop} : (∃ᶠ (x : α) in f, p) ↔ p
• Filter.Frequently.exists 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p : α → Prop} {f : Filter α} (hp : ∃ᶠ (x : α) in f, p x) : ∃ x, p x
• Filter.Frequently.of_forall 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop} (h : ∀ (x : α), p x) : ∃ᶠ (x : α) in f, p x
• Filter.frequently_top 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p : α → Prop} : (∃ᶠ (x : α) in ⊤, p x) ↔ ∃ x, p x
• Filter.not_eventually 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p : α → Prop} {f : Filter α} : (¬∀ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, ¬p x
• Filter.not_frequently 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p : α → Prop} {f : Filter α} : (¬∃ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, ¬p x
• Filter.Eventually.frequently 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop} (h : ∀ᶠ (x : α) in f, p x) : ∃ᶠ (x : α) in f, p x
• Filter.eventually_imp_distrib_right 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} {p : α → Prop} {q : Prop} : (∀ᶠ (x : α) in f, p x → q) ↔ (∃ᶠ (x : α) in f, p x) → q
• Filter.frequently_and_distrib_left 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} {p : Prop} {q : α → Prop} : (∃ᶠ (x : α) in f, p ∧ q x) ↔ p ∧ ∃ᶠ (x : α) in f, q x
• Filter.frequently_and_distrib_right 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} {p : α → Prop} {q : Prop} : (∃ᶠ (x : α) in f, p x ∧ q) ↔ (∃ᶠ (x : α) in f, p x) ∧ q
• Filter.frequently_imp_distrib_left 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} [f.NeBot] {p : Prop} {q : α → Prop} : (∃ᶠ (x : α) in f, p → q x) ↔ p → ∃ᶠ (x : α) in f, q x
• Filter.frequently_imp_distrib_right 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop} {q : Prop} : (∃ᶠ (x : α) in f, p x → q) ↔ (∀ᶠ (x : α) in f, p x) → q
• Filter.Frequently.mono 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p q : α → Prop} {f : Filter α} (h : ∃ᶠ (x : α) in f, p x) (hpq : ∀ (x : α), p x → q x) : ∃ᶠ (x : α) in f, q x
• Filter.frequently_or_distrib_left 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} [f.NeBot] {p : Prop} {q : α → Prop} : (∃ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∃ᶠ (x : α) in f, q x
• Filter.frequently_or_distrib_right 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop} {q : Prop} : (∃ᶠ (x : α) in f, p x ∨ q) ↔ (∃ᶠ (x : α) in f, p x) ∨ q
• Filter.frequently_iff_neBot 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {l : Filter α} {p : α → Prop} : (∃ᶠ (x : α) in l, p x) ↔ (l ⊓ Filter.principal {x | p x}).NeBot
• Filter.Frequently.mp 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p q : α → Prop} {f : Filter α} (h : ∃ᶠ (x : α) in f, p x) (hpq : ∀ᶠ (x : α) in f, p x → q x) : ∃ᶠ (x : α) in f, q x
• Filter.frequently_iff_forall_eventually_exists_and 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p : α → Prop} {f : Filter α} : (∃ᶠ (x : α) in f, p x) ↔ ∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ x, p x ∧ q x
• Filter.frequently_imp_distrib 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} {p q : α → Prop} : (∃ᶠ (x : α) in f, p x → q x) ↔ (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in f, q x
• Filter.frequently_principal 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {a : Set α} {p : α → Prop} : (∃ᶠ (x : α) in Filter.principal a, p x) ↔ ∃ x ∈ a, p x
• Filter.Eventually.and_frequently 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p q : α → Prop} {f : Filter α} (hp : ∀ᶠ (x : α) in f, p x) (hq : ∃ᶠ (x : α) in f, q x) : ∃ᶠ (x : α) in f, p x ∧ q x
• Filter.Frequently.and_eventually 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p q : α → Prop} {f : Filter α} (hp : ∃ᶠ (x : α) in f, p x) (hq : ∀ᶠ (x : α) in f, q x) : ∃ᶠ (x : α) in f, p x ∧ q x
• Filter.frequently_congr 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p q : α → Prop} {f : Filter α} (h : ∀ᶠ (x : α) in f, p x ↔ q x) : (∃ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, q x
• Filter.frequently_mem_iff_neBot 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {l : Filter α} {s : Set α} : (∃ᶠ (x : α) in l, x ∈ s) ↔ (l ⊓ Filter.principal s).NeBot
• Filter.frequently_or_distrib 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} {p q : α → Prop} : (∃ᶠ (x : α) in f, p x ∨ q x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in f, q x
• Filter.frequently_iSup 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} {p : α → Prop} {fs : β → Filter α} : (∃ᶠ (x : α) in ⨆ b, fs b, p x) ↔ ∃ b, ∃ᶠ (x : α) in fs b, p x
• Filter.Frequently.filter_mono 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p : α → Prop} {f g : Filter α} (h : ∃ᶠ (x : α) in f, p x) (hle : f ≤ g) : ∃ᶠ (x : α) in g, p x
• Filter.frequently_sup 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p : α → Prop} {f g : Filter α} : (∃ᶠ (x : α) in f ⊔ g, p x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in g, p x
• Filter.Frequently.inf_principal 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} {s : Set α} {p : α → Prop} : (∃ᶠ (x : α) in f, x ∈ s ∧ p x) → ∃ᶠ (x : α) in f ⊓ Filter.principal s, p x
• Filter.Frequently.of_inf_principal 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} {s : Set α} {p : α → Prop} : (∃ᶠ (x : α) in f ⊓ Filter.principal s, p x) → ∃ᶠ (x : α) in f, x ∈ s ∧ p x
• Filter.frequently_iff 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} {P : α → Prop} : (∃ᶠ (x : α) in f, P x) ↔ ∀ {U : Set α}, U ∈ f → ∃ x ∈ U, P x
• Filter.frequently_inf_principal 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} {s : Set α} {p : α → Prop} : (∃ᶠ (x : α) in f ⊓ Filter.principal s, p x) ↔ ∃ᶠ (x : α) in f, x ∈ s ∧ p x
• Filter.frequently_sSup 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p : α → Prop} {fs : Set (Filter α)} : (∃ᶠ (x : α) in sSup fs, p x) ↔ ∃ f ∈ fs, ∃ᶠ (x : α) in f, p x
• Filter.frequently_pure 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {a : α} {p : α → Prop} : (∃ᶠ (x : α) in pure a, p x) ↔ p a
• Filter.frequently_map 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β} {P : β → Prop} : (∃ᶠ (b : β) in Filter.map m f, P b) ↔ ∃ᶠ (a : α) in f, P (m a)
• Filter.comap_neBot_iff_frequently 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β} : (Filter.comap m f).NeBot ↔ ∃ᶠ (y : β) in f, y ∈ Set.range m
• Filter.frequently_bind 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → Filter β} {p : β → Prop} : (∃ᶠ (y : β) in f.bind m, p y) ↔ ∃ᶠ (x : α) in f, ∃ᶠ (y : β) in m x, p y
• Filter.frequently_comap 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter β} {p : α → Prop} : (∃ᶠ (a : α) in Filter.comap f l, p a) ↔ ∃ᶠ (b : β) in l, ∃ a, f a = b ∧ p a
• Filter.inf_neBot_iff_frequently_left 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {f g : Filter α} : (f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in g, p x
• Filter.inf_neBot_iff_frequently_right 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {f g : Filter α} : (f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x
• Filter.HasBasis.frequently_iff 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : l.HasBasis p s) {q : α → Prop} : (∃ᶠ (x : α) in l, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x
• Filter.Frequently.forall_exists_of_atBot 📋 Mathlib.Order.Filter.AtTopBot.Defs
  {α : Type u_2} [Preorder α] {p : α → Prop} (h : ∃ᶠ (x : α) in Filter.atBot, p x) (a : α) : ∃ b ≤ a, p b
• Filter.Frequently.forall_exists_of_atTop 📋 Mathlib.Order.Filter.AtTopBot.Defs
  {α : Type u_2} [Preorder α] {p : α → Prop} (h : ∃ᶠ (x : α) in Filter.atTop, p x) (a : α) : ∃ b, a ≤ b ∧ p b
• Filter.Tendsto.frequently 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {p : β → Prop} (hf : Filter.Tendsto f l₁ l₂) (h : ∃ᶠ (x : α) in l₁, p (f x)) : ∃ᶠ (y : β) in l₂, p y
• Filter.Tendsto.frequently_map 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {l₁ : Filter α} {l₂ : Filter β} {p : α → Prop} {q : β → Prop} (f : α → β) (c : Filter.Tendsto f l₁ l₂) (w : ∀ (x : α), p x → q (f x)) (h : ∃ᶠ (x : α) in l₁, p x) : ∃ᶠ (y : β) in l₂, q y
• Filter.not_tendsto_iff_exists_frequently_notMem 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} : ¬Filter.Tendsto f l₁ l₂ ↔ ∃ s ∈ l₂, ∃ᶠ (x : α) in l₁, f x ∉ s
• Filter.extraction_of_frequently_atTop 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {P : ℕ → Prop} (h : ∃ᶠ (n : ℕ) in Filter.atTop, P n) : ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
• Filter.extraction_forall_of_frequently 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {P : ℕ → ℕ → Prop} (h : ∀ (n : ℕ), ∃ᶠ (k : ℕ) in Filter.atTop, P n k) : ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
• Filter.frequently_atBot 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} [Preorder α] [IsCodirectedOrder α] {p : α → Prop} [Nonempty α] : (∃ᶠ (x : α) in Filter.atBot, p x) ↔ ∀ (a : α), ∃ b ≤ a, p b
• Filter.frequently_atTop 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} [Preorder α] [IsDirectedOrder α] {p : α → Prop} [Nonempty α] : (∃ᶠ (x : α) in Filter.atTop, p x) ↔ ∀ (a : α), ∃ b, a ≤ b ∧ p b
• Filter.frequently_atBot' 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} [Preorder α] [IsCodirectedOrder α] {p : α → Prop} [Nonempty α] [NoMinOrder α] : (∃ᶠ (x : α) in Filter.atBot, p x) ↔ ∀ (a : α), ∃ b, a > b ∧ p b
• Filter.frequently_atTop' 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} [Preorder α] [IsDirectedOrder α] {p : α → Prop} [Nonempty α] [NoMaxOrder α] : (∃ᶠ (x : α) in Filter.atTop, p x) ↔ ∀ (a : α), ∃ b > a, p b
• Filter.subseq_forall_of_frequently 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {ι : Type u_5} {x : ℕ → ι} {p : ι → Prop} {l : Filter ι} (h_tendsto : Filter.Tendsto x Filter.atTop l) (h : ∃ᶠ (n : ℕ) in Filter.atTop, p (x n)) : ∃ ns, Filter.Tendsto (fun n => x (ns n)) Filter.atTop l ∧ ∀ (n : ℕ), p (x (ns n))
• Filter.frequently_exists 📋 Mathlib.Order.Filter.Finite
  {α : Type u} {ι : Sort u_1} [Finite ι] {l : Filter α} {p : ι → α → Prop} : (∃ᶠ (x : α) in l, ∃ i, p i x) ↔ ∃ i, ∃ᶠ (x : α) in l, p i x
• Filter.frequently_exists_finite 📋 Mathlib.Order.Filter.Finite
  {α : Type u} {ι : Type u_1} {I : Set ι} (hI : I.Finite) {l : Filter α} {p : ι → α → Prop} : (∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x
• Set.Finite.frequently_exists 📋 Mathlib.Order.Filter.Finite
  {α : Type u} {ι : Type u_1} {I : Set ι} (hI : I.Finite) {l : Filter α} {p : ι → α → Prop} : (∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x
• Filter.frequently_exists_finset 📋 Mathlib.Order.Filter.Finite
  {α : Type u} {ι : Type u_1} (I : Finset ι) {l : Filter α} {p : ι → α → Prop} : (∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x
• Finset.frequently_exists 📋 Mathlib.Order.Filter.Finite
  {α : Type u} {ι : Type u_1} (I : Finset ι) {l : Filter α} {p : ι → α → Prop} : (∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x
• Filter.Frequently.of_curry 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {p : α × β → Prop} (h : ∃ᶠ (x : α) in la, ∃ᶠ (y : β) in lb, p (x, y)) : ∃ᶠ (xy : α × β) in la ×ˢ lb, p xy
• Filter.Frequently.uncurry 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {p : α → β → Prop} (h : ∃ᶠ (x : α) in la, ∃ᶠ (y : β) in lb, p x y) : ∃ᶠ (xy : α × β) in la ×ˢ lb, p xy.1 xy.2
• Filter.frequently_prod_and 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {p : α → Prop} {q : β → Prop} : (∃ᶠ (x : α × β) in f ×ˢ g, p x.1 ∧ q x.2) ↔ (∃ᶠ (a : α) in f, p a) ∧ ∃ᶠ (b : β) in g, q b
• Filter.frequently_cofinite_iff_infinite 📋 Mathlib.Order.Filter.Cofinite
  {α : Type u_2} {p : α → Prop} : (∃ᶠ (x : α) in Filter.cofinite, p x) ↔ {x | p x}.Infinite
• Nat.frequently_atTop_iff_infinite 📋 Mathlib.Order.Filter.Cofinite
  {p : ℕ → Prop} : (∃ᶠ (n : ℕ) in Filter.atTop, p n) ↔ {n | p n}.Infinite
• Set.Infinite.frequently_cofinite 📋 Mathlib.Order.Filter.Cofinite
  {α : Type u_2} {s : Set α} : s.Infinite → ∃ᶠ (x : α) in Filter.cofinite, x ∈ s
• Filter.frequently_cofinite_mem_iff_infinite 📋 Mathlib.Order.Filter.Cofinite
  {α : Type u_2} {s : Set α} : (∃ᶠ (x : α) in Filter.cofinite, x ∈ s) ↔ s.Infinite
• Set.infinite_iff_frequently_cofinite 📋 Mathlib.Order.Filter.Cofinite
  {α : Type u_2} {s : Set α} : s.Infinite ↔ ∃ᶠ (x : α) in Filter.cofinite, x ∈ s
• Filter.Frequently.eventually 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f : Ultrafilter α} {p : α → Prop} : (∃ᶠ (x : α) in ↑f, p x) → ∀ᶠ (x : α) in ↑f, p x
• Ultrafilter.frequently_iff_eventually 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f : Ultrafilter α} {p : α → Prop} : (∃ᶠ (x : α) in ↑f, p x) ↔ ∀ᶠ (x : α) in ↑f, p x
• Filter.frequently_one 📋 Mathlib.Order.Filter.Pointwise
  {α : Type u_2} [One α] {p : α → Prop} : (∃ᶠ (x : α) in 1, p x) ↔ p 1
• Filter.frequently_zero 📋 Mathlib.Order.Filter.Pointwise
  {α : Type u_2} [Zero α] {p : α → Prop} : (∃ᶠ (x : α) in 0, p x) ↔ p 0
• Filter.frequently_inv 📋 Mathlib.Order.Filter.Pointwise
  {α : Type u_2} [Inv α] {f : Filter α} {p : α → Prop} : (∃ᶠ (x : α) in f⁻¹, p x) ↔ ∃ᶠ (x : α) in f, p x⁻¹
• Filter.frequently_neg 📋 Mathlib.Order.Filter.Pointwise
  {α : Type u_2} [Neg α] {f : Filter α} {p : α → Prop} : (∃ᶠ (x : α) in -f, p x) ↔ ∃ᶠ (x : α) in f, p (-x)
• Filter.frequently_inv_filter 📋 Mathlib.Order.Filter.Pointwise
  {α : Type u_2} {β : Type u_3} [SMul α β] {f : Filter β} {a : α} {p : β → Prop} : (∃ᶠ (y : β) in a • f, p y) ↔ ∃ᶠ (x : β) in f, p (a • x)
• Filter.frequently_neg_filter 📋 Mathlib.Order.Filter.Pointwise
  {α : Type u_2} {β : Type u_3} [VAdd α β] {f : Filter β} {a : α} {p : β → Prop} : (∃ᶠ (y : β) in a +ᵥ f, p y) ↔ ∃ᶠ (x : β) in f, p (a +ᵥ x)
• Filter.frequently_high_scores 📋 Mathlib.Order.Filter.AtTopBot.Finite
  {β : Type u_3} [LinearOrder β] [NoMaxOrder β] {u : ℕ → β} (hu : Filter.Tendsto u Filter.atTop Filter.atTop) : ∃ᶠ (n : ℕ) in Filter.atTop, ∀ k < n, u k < u n
• Filter.frequently_low_scores 📋 Mathlib.Order.Filter.AtTopBot.Finite
  {β : Type u_3} [LinearOrder β] [NoMinOrder β] {u : ℕ → β} (hu : Filter.Tendsto u Filter.atTop Filter.atBot) : ∃ᶠ (n : ℕ) in Filter.atTop, ∀ k < n, u n < u k
• Filter.exists_seq_forall_of_frequently 📋 Mathlib.Order.Filter.AtTopBot.CountablyGenerated
  {ι : Type u_3} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated] (h : ∃ᶠ (n : ι) in l, p n) : ∃ ns, Filter.Tendsto ns Filter.atTop l ∧ ∀ (n : ℕ), p (ns n)
• Filter.frequently_iff_seq_forall 📋 Mathlib.Order.Filter.AtTopBot.CountablyGenerated
  {ι : Type u_3} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated] : (∃ᶠ (n : ι) in l, p n) ↔ ∃ ns, Filter.Tendsto ns Filter.atTop l ∧ ∀ (n : ℕ), p (ns n)
• Filter.frequently_iff_seq_frequently 📋 Mathlib.Order.Filter.AtTopBot.CountablyGenerated
  {ι : Type u_3} {l : Filter ι} {p : ι → Prop} [l.IsCountablyGenerated] : (∃ᶠ (n : ι) in l, p n) ↔ ∃ x, Filter.Tendsto x Filter.atTop l ∧ ∃ᶠ (n : ℕ) in Filter.atTop, p (x n)
• Filter.frequently_curry_iff 📋 Mathlib.Order.Filter.Curry
  {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} (p : α × β → Prop) : (∃ᶠ (x : α × β) in l.curry m, p x) ↔ ∃ᶠ (x : α) in l, ∃ᶠ (y : β) in m, p (x, y)
• Filter.frequently_curry_prod_iff 📋 Mathlib.Order.Filter.Curry
  {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} {s : Set α} {t : Set β} : (∃ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t) ↔ (∃ᶠ (x : α) in l, x ∈ s) ∧ ∃ᶠ (y : β) in m, y ∈ t
• frequently_frequently_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} : (∃ᶠ (x' : X) in nhds x, ∃ᶠ (x'' : X) in nhds x', p x'') ↔ ∃ᶠ (x : X) in nhds x, p x
• Filter.Frequently.mem_closure 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : (∃ᶠ (x : X) in nhds x, x ∈ s) → x ∈ closure s
• mem_closure_iff_frequently 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ closure s ↔ ∃ᶠ (x : X) in nhds x, x ∈ s
• Filter.Frequently.mem_of_closed 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (h : ∃ᶠ (x : X) in nhds x, x ∈ s) (hs : IsClosed s) : x ∈ s
• isClosed_iff_frequently 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsClosed s ↔ ∀ (x : X), (∃ᶠ (y : X) in nhds x, y ∈ s) → x ∈ s
• frequently_nhds_iff 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} : (∃ᶠ (y : X) in nhds x, p y) ↔ ∀ (U : Set X), x ∈ U → IsOpen U → ∃ y ∈ U, p y
• mem_closure_of_frequently_of_tendsto 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {s : Set X} {f : α → X} {b : Filter α} (h : ∃ᶠ (x : α) in b, f x ∈ s) (hf : Filter.Tendsto f b (nhds x)) : x ∈ closure s
• IsClosed.mem_of_frequently_of_tendsto 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {s : Set X} {f : α → X} {b : Filter α} (hs : IsClosed s) (h : ∃ᶠ (x : α) in b, f x ∈ s) (hf : Filter.Tendsto f b (nhds x)) : x ∈ s
• ClusterPt.frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} {p : X → Prop} (hx : ClusterPt x F) (hp : ∀ᶠ (y : X) in nhds x, p y) : ∃ᶠ (y : X) in F, p y
• ClusterPt.frequently' 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} {p : X → Prop} (hx : ClusterPt x F) (hp : ∀ᶠ (y : X) in F, p y) : ∃ᶠ (y : X) in nhds x, p y
• clusterPt_principal_iff_frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : ClusterPt x (Filter.principal s) ↔ ∃ᶠ (y : X) in nhds x, y ∈ s
• accPt_iff_frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {C : Set X} : AccPt x (Filter.principal C) ↔ ∃ᶠ (y : X) in nhds x, y ≠ x ∧ y ∈ C
• MapClusterPt.frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} (h : MapClusterPt x F u) {p : X → Prop} (hp : ∀ᶠ (y : X) in nhds x, p y) : ∃ᶠ (a : α) in F, p (u a)
• clusterPt_iff_frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : ClusterPt x F ↔ ∀ s ∈ nhds x, ∃ᶠ (y : X) in F, y ∈ s
• clusterPt_iff_frequently' 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : ClusterPt x F ↔ ∀ s ∈ F, ∃ᶠ (y : X) in nhds x, y ∈ s
• accPt_iff_frequently_nhdsNE 📋 Mathlib.Topology.ClusterPt
  {X : Type u_3} [TopologicalSpace X] {x : X} {C : Set X} : AccPt x (Filter.principal C) ↔ ∃ᶠ (y : X) in nhdsWithin x {x}ᶜ, y ∈ C
• Filter.HasBasis.clusterPt_iff_frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} {F : Filter X} (hx : (nhds x).HasBasis p s) : ClusterPt x F ↔ ∀ (i : ι), p i → ∃ᶠ (x : X) in F, x ∈ s i
• Filter.HasBasis.clusterPt_iff_frequently' 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} {F : Filter X} (hx : F.HasBasis p s) : ClusterPt x F ↔ ∀ (i : ι), p i → ∃ᶠ (x : X) in nhds x, x ∈ s i
• mapClusterPt_iff_frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} : MapClusterPt x F u ↔ ∀ s ∈ nhds x, ∃ᶠ (a : α) in F, u a ∈ s
• Filter.HasBasis.mapClusterPt_iff_frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} (hx : (nhds x).HasBasis p s) : MapClusterPt x F u ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i
• IsClosedMap.frequently_nhds_fiber 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsClosedMap f) {p : X → Prop} (y₀ : Y) (H : ∃ᶠ (y : Y) in nhds y₀, ∃ x ∈ f ⁻¹' {y}, p x) : ∃ x₀ ∈ f ⁻¹' {y₀}, ∃ᶠ (x : X) in nhds x₀, p x
• frequently_nhdsWithin_iff 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {z : α} {s : Set α} {p : α → Prop} : (∃ᶠ (x : α) in nhdsWithin z s, p x) ↔ ∃ᶠ (x : α) in nhds z, p x ∧ x ∈ s
• mem_closure_ne_iff_frequently_within 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {z : α} {s : Set α} : z ∈ closure (s \ {z}) ↔ ∃ᶠ (x : α) in nhdsWithin z {z}ᶜ, x ∈ s
• frequently_nhds_subtype_iff 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] (s : Set α) (a : ↑s) (P : α → Prop) : (∃ᶠ (x : ↑s) in nhds a, P ↑x) ↔ ∃ᶠ (x : α) in nhdsWithin (↑a) s, P x
• clusterPt_principal_subtype_iff_frequently 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} (hst : s ⊆ t) {J : Set ↑s} {a : ↑s} : ClusterPt a (Filter.principal J) ↔ ∃ᶠ (x : α) in nhdsWithin (↑a) t, ∃ (h : x ∈ s), ⟨x, h⟩ ∈ J
• IsCompact.exists_clusterPt_of_frequently 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} {l : Filter X} (hs : IsCompact s) (hl : ∃ᶠ (x : X) in l, x ∈ s) : ∃ a ∈ s, ClusterPt a l
• IsCompact.exists_mapClusterPt_of_frequently 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} {ι : Type u_1} [TopologicalSpace X] {s : Set X} {l : Filter ι} {f : ι → X} (hs : IsCompact s) (hf : ∃ᶠ (x : ι) in l, f x ∈ s) : ∃ a ∈ s, MapClusterPt a l f
• Filter.frequently_smallSets_mem 📋 Mathlib.Order.Filter.SmallSets
  {α : Type u_1} (l : Filter α) : ∃ᶠ (s : Set α) in l.smallSets, s ∈ l
• Filter.Frequently.smallSets_of_forall_mem_basis 📋 Mathlib.Order.Filter.SmallSets
  {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {P : Set α → Prop} (h₁ : ∀ (i : ι), p i → P (s i)) (h₂ : l.HasBasis p s) : ∃ᶠ (t : Set α) in l.smallSets, P t
• Filter.frequently_smallSets 📋 Mathlib.Order.Filter.SmallSets
  {α : Type u_1} {l : Filter α} {p : Set α → Prop} : (∃ᶠ (s : Set α) in l.smallSets, p s) ↔ ∀ t ∈ l, ∃ s ⊆ t, p s
• Filter.frequently_smallSets' 📋 Mathlib.Order.Filter.SmallSets
  {α : Type u_4} {l : Filter α} {p : Set α → Prop} (hp : ∀ ⦃s t : Set α⦄, s ⊆ t → p s → p t) : (∃ᶠ (s : Set α) in l.smallSets, p s) ↔ ∀ t ∈ l, p t
• Filter.HasBasis.frequently_smallSets 📋 Mathlib.Order.Filter.SmallSets
  {α : Type u_4} {ι : Sort u_5} {p : ι → Prop} {l : Filter α} {s : ι → Set α} {q : Set α → Prop} {hl : l.HasBasis p s} (hq : ∀ ⦃s t : Set α⦄, s ⊆ t → q s → q t) : (∃ᶠ (s : Set α) in l.smallSets, q s) ↔ ∀ (i : ι), p i → q (s i)
• tendsto_nhds_unique_of_frequently_eq 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {f g : Y → X} {l : Filter Y} {a b : X} (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto g l (nhds b)) (hfg : ∃ᶠ (x : Y) in l, f x = g x) : a = b
• frequently_gt_nhds 📋 Mathlib.Topology.Order.LeftRight
  {α : Type u_1} [TopologicalSpace α] [Preorder α] (a : α) [(nhdsWithin a (Set.Ioi a)).NeBot] : ∃ᶠ (x : α) in nhds a, a < x
• frequently_lt_nhds 📋 Mathlib.Topology.Order.LeftRight
  {α : Type u_1} [TopologicalSpace α] [Preorder α] (a : α) [(nhdsWithin a (Set.Iio a)).NeBot] : ∃ᶠ (x : α) in nhds a, x < a
• ge_of_tendsto_of_frequently 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIciTopology α] {f : β → α} {a b : α} {x : Filter β} (colim : Filter.Tendsto f x (nhds a)) (h : ∃ᶠ (c : β) in x, b ≤ f c) : b ≤ a
• le_of_tendsto_of_frequently 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [ClosedIicTopology α] {f : β → α} {a b : α} {x : Filter β} (lim : Filter.Tendsto f x (nhds a)) (h : ∃ᶠ (c : β) in x, f c ≤ b) : a ≤ b
• antitone_of_frequently_antitone_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {ι : Type u_1} {l : Filter ι} [Preorder β] {F : ι → β → α} {f : β → α} (hF : ∃ᶠ (i : ι) in l, Antitone (F i)) (hlim : ∀ (x : β), Filter.Tendsto (fun i => F i x) l (nhds (f x))) : Antitone f
• monotone_of_frequently_monotone_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {ι : Type u_1} {l : Filter ι} [Preorder β] {F : ι → β → α} {f : β → α} (hF : ∃ᶠ (i : ι) in l, Monotone (F i)) (hlim : ∀ (x : β), Filter.Tendsto (fun i => F i x) l (nhds (f x))) : Monotone f
• le_of_tendsto_of_tendsto_of_frequently 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {f g : β → α} {b : Filter β} {a₁ a₂ : α} (hf : Filter.Tendsto f b (nhds a₁)) (hg : Filter.Tendsto g b (nhds a₂)) (h : ∃ᶠ (x : β) in b, f x ≤ g x) : a₁ ≤ a₂
• antitoneOn_of_frequently_antitoneOn_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {ι : Type u_1} {l : Filter ι} [Preorder β] {F : ι → β → α} {f : β → α} {s : Set β} (hF : ∃ᶠ (i : ι) in l, AntitoneOn (F i) s) (hlim : ∀ x ∈ s, Filter.Tendsto (fun i => F i x) l (nhds (f x))) : AntitoneOn f s
• monotoneOn_of_frequently_monotoneOn_of_tendsto 📋 Mathlib.Topology.Order.OrderClosed
  {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder α] [t : OrderClosedTopology α] {ι : Type u_1} {l : Filter ι} [Preorder β] {F : ι → β → α} {f : β → α} {s : Set β} (hF : ∃ᶠ (i : ι) in l, MonotoneOn (F i) s) (hlim : ∀ x ∈ s, Filter.Tendsto (fun i => F i x) l (nhds (f x))) : MonotoneOn f s
• TendstoUniformly.uniformContinuous 📋 Mathlib.Topology.UniformSpace.UniformApproximation
  {α : Type u_4} {β : Type u_5} {ι : Type u_6} [UniformSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} (h : TendstoUniformly F f p) (hc : ∃ᶠ (n : ι) in p, UniformContinuous (F n)) : UniformContinuous f
• TendstoUniformly.continuous 📋 Mathlib.Topology.UniformSpace.UniformApproximation
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} (h : TendstoUniformly F f p) (hc : ∃ᶠ (n : ι) in p, Continuous (F n)) : Continuous f
• TendstoLocallyUniformly.continuous 📋 Mathlib.Topology.UniformSpace.UniformApproximation
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} (h : TendstoLocallyUniformly F f p) (hc : ∃ᶠ (n : ι) in p, Continuous (F n)) : Continuous f
• TendstoUniformlyOn.uniformContinuousOn 📋 Mathlib.Topology.UniformSpace.UniformApproximation
  {α : Type u_4} {β : Type u_5} {ι : Type u_6} [UniformSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (h : TendstoUniformlyOn F f p s) (hc : ∃ᶠ (n : ι) in p, UniformContinuousOn (F n) s) : UniformContinuousOn f s
• TendstoUniformlyOn.continuousOn 📋 Mathlib.Topology.UniformSpace.UniformApproximation
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (h : TendstoUniformlyOn F f p s) (hc : ∃ᶠ (n : ι) in p, ContinuousOn (F n) s) : ContinuousOn f s
• TendstoLocallyUniformlyOn.continuousOn 📋 Mathlib.Topology.UniformSpace.UniformApproximation
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (h : TendstoLocallyUniformlyOn F f p s) (hc : ∃ᶠ (n : ι) in p, ContinuousOn (F n) s) : ContinuousOn f s
• Mathlib.Tactic.Peel.frequently_imp 📋 Mathlib.Tactic.Peel
  {α : Type u_1} {p q : α → Prop} {f : Filter α} (hq : ∀ (x : α), p x → q x) (hp : ∃ᶠ (x : α) in f, p x) : ∃ᶠ (x : α) in f, q x
• Mathlib.Tactic.Peel.frequently_congr 📋 Mathlib.Tactic.Peel
  {α : Type u_1} {p q : α → Prop} {f : Filter α} (hq : ∀ (x : α), p x ↔ q x) : (∃ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, q x
• Metric.forall_of_forall_mem_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (p : α → Prop) (x : α) (H : ∃ᶠ (R : ℝ) in Filter.atTop, ∀ y ∈ Metric.ball x R, p y) (y : α) : p y
• Metric.forall_of_forall_mem_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (p : α → Prop) (x : α) (H : ∃ᶠ (R : ℝ) in Filter.atTop, ∀ y ∈ Metric.closedBall x R, p y) (y : α) : p y
• IsGLB.frequently_nhds_mem 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) : ∃ᶠ (x : α) in nhds a, x ∈ s
• IsLUB.frequently_nhds_mem 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : ∃ᶠ (x : α) in nhds a, x ∈ s
• IsGLB.frequently_mem 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsGLB s a) (hs : s.Nonempty) : ∃ᶠ (x : α) in nhdsWithin a (Set.Ici a), x ∈ s
• IsLUB.frequently_mem 📋 Mathlib.Topology.Order.IsLUB
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) : ∃ᶠ (x : α) in nhdsWithin a (Set.Iic a), x ∈ s
• Filter.IsCobounded.of_frequently_ge 📋 Mathlib.Order.Filter.IsBounded
  {α : Type u_1} {f : Filter α} [LinearOrder α] {l : α} (freq_ge : ∃ᶠ (x : α) in f, l ≤ x) : Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f
• Filter.IsCobounded.of_frequently_le 📋 Mathlib.Order.Filter.IsBounded
  {α : Type u_1} {f : Filter α} [LinearOrder α] {l : α} (freq_ge : ∃ᶠ (x : α) in f, x ≤ l) : Filter.IsCobounded (fun x1 x2 => x2 ≤ x1) f
• Filter.IsCobounded.frequently_ge 📋 Mathlib.Order.Filter.IsBounded
  {α : Type u_1} {f : Filter α} [LinearOrder α] [f.NeBot] (cobdd : Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f) : ∃ l, ∃ᶠ (x : α) in f, l ≤ x
• Filter.IsCobounded.frequently_le 📋 Mathlib.Order.Filter.IsBounded
  {α : Type u_1} {f : Filter α} [LinearOrder α] [f.NeBot] (cobdd : Filter.IsCobounded (fun x1 x2 => x2 ≤ x1) f) : ∃ l, ∃ᶠ (x : α) in f, x ≤ l
• Filter.IsCoboundedUnder.of_frequently_ge 📋 Mathlib.Order.Filter.IsBounded
  {α : Type u_1} {ι : Type u_4} [LinearOrder α] {f : Filter ι} {u : ι → α} {a : α} (freq_ge : ∃ᶠ (x : ι) in f, a ≤ u x) : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u
• Filter.IsCoboundedUnder.of_frequently_le 📋 Mathlib.Order.Filter.IsBounded
  {α : Type u_1} {ι : Type u_4} [LinearOrder α] {f : Filter ι} {u : ι → α} {a : α} (freq_ge : ∃ᶠ (x : ι) in f, u x ≤ a) : Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) f u
• Filter.IsCoboundedUnder.frequently_ge 📋 Mathlib.Order.Filter.IsBounded
  {α : Type u_1} {ι : Type u_4} [LinearOrder α] {f : Filter ι} [f.NeBot] {u : ι → α} (h : Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) : ∃ a, ∃ᶠ (x : ι) in f, a ≤ u x
• Filter.IsCoboundedUnder.frequently_le 📋 Mathlib.Order.Filter.IsBounded
  {α : Type u_1} {ι : Type u_4} [LinearOrder α] {f : Filter ι} [f.NeBot] {u : ι → α} (h : Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) f u) : ∃ a, ∃ᶠ (x : ι) in f, u x ≤ a
• Antitone.frequently_ge_map_of_frequently_le 📋 Mathlib.Order.Filter.IsBounded
  {R : Type u_5} {S : Type u_6} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_decr : Antitone f) {l : R} (frbdd : ∃ᶠ (x : R) in F, x ≤ l) : ∃ᶠ (y : S) in Filter.map f F, f l ≤ y
• Antitone.frequently_le_map_of_frequently_ge 📋 Mathlib.Order.Filter.IsBounded
  {R : Type u_5} {S : Type u_6} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_decr : Antitone f) {l : R} (frbdd : ∃ᶠ (x : R) in F, l ≤ x) : ∃ᶠ (y : S) in Filter.map f F, y ≤ f l
• Monotone.frequently_ge_map_of_frequently_ge 📋 Mathlib.Order.Filter.IsBounded
  {R : Type u_5} {S : Type u_6} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_incr : Monotone f) {l : R} (freq_ge : ∃ᶠ (x : R) in F, l ≤ x) : ∃ᶠ (x' : S) in Filter.map f F, f l ≤ x'
• Monotone.frequently_le_map_of_frequently_le 📋 Mathlib.Order.Filter.IsBounded
  {R : Type u_5} {S : Type u_6} {F : Filter R} [LinearOrder R] [LinearOrder S] {f : R → S} (f_incr : Monotone f) {l : R} (freq_ge : ∃ᶠ (x : R) in F, x ≤ l) : ∃ᶠ (x' : S) in Filter.map f F, x' ≤ f l
• Filter.isBoundedUnder_le_mul_of_nonneg 📋 Mathlib.Order.Filter.IsBounded
  {α : Type u_1} {ι : Type u_4} [Preorder α] [Mul α] [Zero α] [PosMulMono α] [MulPosMono α] {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.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (u * v)
• 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.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.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.frequently_lt_of_limsInf_lt 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {f : Filter α} [ConditionallyCompleteLinearOrder α] {a : α} (hf : Filter.IsCobounded (fun x1 x2 => x1 ≥ x2) f := by isBoundedDefault) (h : f.limsInf < a) : ∃ᶠ (n : α) in f, n < a
• Filter.frequently_lt_of_lt_limsSup 📋 Mathlib.Order.LiminfLimsup
  {α : Type u_1} {f : Filter α} [ConditionallyCompleteLinearOrder α] {a : α} (hf : Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f := by isBoundedDefault) (h : a < f.limsSup) : ∃ᶠ (n : α) in f, a < n
• 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.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.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
• 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
• 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_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.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.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.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
• tendsto_of_no_upcrossings 📋 Mathlib.Topology.Order.LiminfLimsup
  {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {f : Filter β} {u : β → α} {s : Set α} (hs : Dense s) (H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)) (h : Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u := by isBoundedDefault) (h' : Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u := by isBoundedDefault) : ∃ c, Filter.Tendsto u f (nhds c)
• 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.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
• IsSeqCompact.exists_tendsto_of_frequently_mem 📋 Mathlib.Topology.Sequences
  {X : Type u_1} [UniformSpace X] {s : Set X} (hs : IsSeqCompact s) {u : ℕ → X} (hu : ∃ᶠ (n : ℕ) in Filter.atTop, u n ∈ s) (huc : CauchySeq u) : ∃ x ∈ s, Filter.Tendsto u Filter.atTop (nhds x)
• IsSeqCompact.subseq_of_frequently_in 📋 Mathlib.Topology.Sequences
  {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsSeqCompact s) {x : ℕ → X} (hx : ∃ᶠ (n : ℕ) in Filter.atTop, x n ∈ s) : ∃ a ∈ s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)
• IsCompact.tendsto_subseq' 📋 Mathlib.Topology.Sequences
  {X : Type u_1} [TopologicalSpace X] [FirstCountableTopology X] {s : Set X} {x : ℕ → X} (hs : IsCompact s) (hx : ∃ᶠ (n : ℕ) in Filter.atTop, x n ∈ s) : ∃ a ∈ s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)
• semicontinuous_iff_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r : α → β → Prop} : Semicontinuous r ↔ ∀ (x : α) (y : β), (∃ᶠ (x' : α) in nhds x, ¬r x' y) → ¬r x y
• semicontinuousAt_iff_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r : α → β → Prop} {x : α} : SemicontinuousAt r x ↔ ∀ (y : β), (∃ᶠ (x' : α) in nhds x, ¬r x' y) → ¬r x y
• semicontinuousWithinAt_iff_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r : α → β → Prop} {x : α} {s : Set α} : SemicontinuousWithinAt r s x ↔ ∀ (y : β), (∃ᶠ (x' : α) in nhdsWithin x s, ¬r x' y) → ¬r x y
• semicontinuousOn_iff_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {r : α → β → Prop} {s : Set α} : SemicontinuousOn r s ↔ ∀ x ∈ s, ∀ (y : β), (∃ᶠ (x' : α) in nhdsWithin x s, ¬r x' y) → ¬r x y
• LowerHemicontinuous.frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} : LowerHemicontinuous f → ∀ (x : α) (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, f x' ⊆ t) → f x ⊆ t
• LowerHemicontinuous.of_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} : (∀ (x : α) (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, f x' ⊆ t) → f x ⊆ t) → LowerHemicontinuous f
• lowerHemicontinuous_iff_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} : LowerHemicontinuous f ↔ ∀ (x : α) (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, f x' ⊆ t) → f x ⊆ t
• LowerHemicontinuousAt.frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} : LowerHemicontinuousAt f x → ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, f x' ⊆ t) → f x ⊆ t
• LowerHemicontinuousAt.of_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} : (∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, f x' ⊆ t) → f x ⊆ t) → LowerHemicontinuousAt f x
• lowerHemicontinuousAt_iff_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} : LowerHemicontinuousAt f x ↔ ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, f x' ⊆ t) → f x ⊆ t
• UpperHemicontinuous.frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} : UpperHemicontinuous f → ∀ (x : α) (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
• UpperHemicontinuous.of_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} : (∀ (x : α) (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty) → UpperHemicontinuous f
• upperHemicontinuous_iff_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} : UpperHemicontinuous f ↔ ∀ (x : α) (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
• LowerHemicontinuousWithinAt.frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} {s : Set α} : LowerHemicontinuousWithinAt f s x → ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ t) → f x ⊆ t
• LowerHemicontinuousWithinAt.of_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} {s : Set α} : (∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ t) → f x ⊆ t) → LowerHemicontinuousWithinAt f s x
• UpperHemicontinuousAt.frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} : UpperHemicontinuousAt f x → ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
• UpperHemicontinuousAt.of_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} : (∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty) → UpperHemicontinuousAt f x
• lowerHemicontinuousWithinAt_iff_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} {s : Set α} : LowerHemicontinuousWithinAt f s x ↔ ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ t) → f x ⊆ t
• upperHemicontinuousAt_iff_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} : UpperHemicontinuousAt f x ↔ ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
• UpperHemicontinuousWithinAt.frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} {s : Set α} : UpperHemicontinuousWithinAt f s x → ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
• UpperHemicontinuousWithinAt.of_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} {s : Set α} : (∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty) → UpperHemicontinuousWithinAt f s x
• upperHemicontinuousWithinAt_iff_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {x : α} {s : Set α} : UpperHemicontinuousWithinAt f s x ↔ ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
• LowerHemicontinuousOn.frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {s : Set α} : LowerHemicontinuousOn f s → ∀ x ∈ s, ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ t) → f x ⊆ t
• LowerHemicontinuousOn.of_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {s : Set α} : (∀ x ∈ s, ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ t) → f x ⊆ t) → LowerHemicontinuousOn f s
• lowerHemicontinuousOn_iff_frequently 📋 Mathlib.Topology.Semicontinuity.Defs
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → Set β} {s : Set α} : LowerHemicontinuousOn f s ↔ ∀ x ∈ s, ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ t) → f x ⊆ t

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 ce5dd8c