Loogle!

Result

Found 2233 declarations mentioning Filter.Eventually. Of these, only the first 200 are shown.

• Filter.Eventually 📋 Mathlib.Order.Filter.Defs
  {α : Type u_1} (p : α → Prop) (f : Filter α) : Prop
• Filter.eventually_true 📋 Mathlib.Order.Filter.Basic
  {α : Type u} (f : Filter α) : ∀ᶠ (x : α) in f, True
• Filter.eventually_bot 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p : α → Prop} : ∀ᶠ (x : α) in ⊥, p x
• Filter.eventually_const 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} [t : f.NeBot] {p : Prop} : (∀ᶠ (x : α) in f, p) ↔ p
• Filter.Eventually.of_forall 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p : α → Prop} {f : Filter α} (hp : ∀ (x : α), p x) : ∀ᶠ (x : α) in f, p x
• Filter.eventually_mem_principal 📋 Mathlib.Order.Filter.Basic
  {α : Type u} (s : Set α) : ∀ᶠ (x : α) in Filter.principal s, x ∈ s
• Filter.eventually_top 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p : α → Prop} : (∀ᶠ (x : α) in ⊤, p x) ↔ ∀ (x : α), p x
• Filter.eventually_false_iff_eq_bot 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} : (∀ᶠ (x : α) in f, False) ↔ f = ⊥
• Filter.Eventually.exists 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p : α → Prop} {f : Filter α} [f.NeBot] (hp : ∀ᶠ (x : α) in f, 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_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.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.eventually_or_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.eventually_or_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.forall_eventually_of_eventually_forall 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} {f : Filter α} {p : α → β → Prop} (h : ∀ᶠ (x : α) in f, ∀ (y : β), p x y) (y : β) : ∀ᶠ (x : α) in f, p x y
• 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.Eventually.and 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p q : α → Prop} {f : Filter α} : Filter.Eventually p f → Filter.Eventually q f → ∀ᶠ (x : α) in f, p x ∧ q x
• Filter.Eventually.mono 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p q : α → Prop} {f : Filter α} (hp : ∀ᶠ (x : α) in f, p x) (hq : ∀ (x : α), p x → q x) : ∀ᶠ (x : α) in f, q x
• Filter.EventuallyEq.eventually 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} (h : f =ᶠ[l] g) : ∀ᶠ (x : α) in l, f x = g x
• Filter.eventually_iff 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} {P : α → Prop} : (∀ᶠ (x : α) in f, P x) ↔ {x | P x} ∈ f
• Filter.eventually_principal 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {a : Set α} {p : α → Prop} : (∀ᶠ (x : α) in Filter.principal a, p x) ↔ ∀ x ∈ a, p x
• Filter.ext' 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f₁ f₂ : Filter α} (h : ∀ (p : α → Prop), (∀ᶠ (x : α) in f₁, p x) ↔ ∀ᶠ (x : α) in f₂, p x) : f₁ = f₂
• Filter.eventually_mem_set 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {s : Set α} {l : Filter α} : (∀ᶠ (x : α) in l, x ∈ s) ↔ s ∈ l
• Filter.Eventually.mp 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p q : α → Prop} {f : Filter α} (hp : ∀ᶠ (x : α) in f, p x) (hq : ∀ᶠ (x : α) in f, p x → q x) : ∀ᶠ (x : α) in f, q x
• 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.eventuallyEqSet_empty 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {s : Set α} {l : Filter α} : s =ᶠ[l] ∅ ↔ ∀ᶠ (x : α) in l, x ∉ s
• Filter.eventuallyEq_empty 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {s : Set α} {l : Filter α} : s =ᶠ[l] ∅ ↔ ∀ᶠ (x : α) in l, x ∉ s
• Filter.eventually_iff_all_subsets 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} {p : α → Prop} : (∀ᶠ (x : α) in f, p x) ↔ ∀ (s : Set α), ∀ᶠ (x : α) in f, x ∈ s → p 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.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.Eventually.congr 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} {p q : α → Prop} (h' : ∀ᶠ (x : α) in f, p x) (h : ∀ᶠ (x : α) in f, p x ↔ q x) : ∀ᶠ (x : α) in f, 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.eventually_congr 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} {p q : α → Prop} (h : ∀ᶠ (x : α) in f, p x ↔ q x) : (∀ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, 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.eventually_and 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p q : α → Prop} {f : Filter α} : (∀ᶠ (x : α) in f, p x ∧ q x) ↔ (∀ᶠ (x : α) in f, p x) ∧ ∀ᶠ (x : α) in f, q x
• Filter.eventually_iSup 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {ι : Sort x} {p : α → Prop} {fs : ι → Filter α} : (∀ᶠ (x : α) in ⨆ b, fs b, p x) ↔ ∀ (b : ι), ∀ᶠ (x : α) in fs b, p x
• Filter.Eventually.filter_mono 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f₁ f₂ : Filter α} (h : f₁ ≤ f₂) {p : α → Prop} (hp : ∀ᶠ (x : α) in f₂, p x) : ∀ᶠ (x : α) in f₁, p x
• Filter.EventuallySubset.eventually 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {s t : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) : ∀ᶠ (x : α) in l, x ∈ s → x ∈ t
• Filter.eventually_of_mem 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} {P : α → Prop} {U : Set α} (hU : U ∈ f) (h : ∀ x ∈ U, P x) : ∀ᶠ (x : α) in f, P x
• Filter.eventually_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.Eventually.choice 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} {r : α → β → Prop} {l : Filter α} [l.NeBot] (h : ∀ᶠ (x : α) in l, ∃ y, r x y) : ∃ f, ∀ᶠ (x : α) in l, r x (f x)
• Filter.Eventually.ne_of_gt 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f g : α → β} (h : ∀ᶠ (x : α) in l, g x < f x) : ∀ᶠ (x : α) in l, f x ≠ g x
• Filter.Eventually.ne_of_lt 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f g : α → β} (h : ∀ᶠ (x : α) in l, f x < g x) : ∀ᶠ (x : α) in l, f x ≠ g x
• Filter.Eventually.set_eq 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {s t : Set α} {l : Filter α} : (∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t) → s =ᶠ[l] t
• Filter.EventuallyEq.mem_iff 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {s t : Set α} {l : Filter α} : s =ᶠ[l] t → ∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t
• Filter.EventuallyEq.rw 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} (h : f =ᶠ[l] g) (p : α → β → Prop) (hf : ∀ᶠ (x : α) in l, p x (f x)) : ∀ᶠ (x : α) in l, p x (g x)
• Filter.EventuallyEqSet.mem_iff 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {s t : Set α} {l : Filter α} : s =ᶠ[l] t → ∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t
• Filter.eventuallyEqSet_iff 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {s t : Set α} {l : Filter α} : s =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t
• Filter.eventuallyEq_set 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {s t : Set α} {l : Filter α} : s =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t
• Filter.eventuallyEq_iff_all_subsets 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} {f g : α → β} {l : Filter α} : f =ᶠ[l] g ↔ ∀ (s : Set α), ∀ᶠ (x : α) in l, x ∈ s → f x = g x
• Filter.eventually_inf_principal 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} {p : α → Prop} {s : Set α} : (∀ᶠ (x : α) in f ⊓ Filter.principal s, p x) ↔ ∀ᶠ (x : α) in f, x ∈ s → p x
• Filter.eventually_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.Eventually.exists_mem 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p : α → Prop} {f : Filter α} (hp : ∀ᶠ (x : α) in f, p x) : ∃ v ∈ f, ∀ y ∈ v, p y
• Filter.eventually_iff_exists_mem 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {p : α → Prop} {f : Filter α} : (∀ᶠ (x : α) in f, p x) ↔ ∃ v ∈ f, ∀ y ∈ v, p y
• Filter.eventuallyLE_iff_all_subsets 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [LE β] {f g : α → β} {l : Filter α} : f ≤ᶠ[l] g ↔ ∀ (s : Set α), ∀ᶠ (x : α) in l, x ∈ s → f x ≤ g x
• Filter.inter_eventuallyEqSet_left 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {s t : Set α} {l : Filter α} : s ∩ t =ᶠ[l] s ↔ ∀ᶠ (x : α) in l, x ∈ s → x ∈ t
• Filter.inter_eventuallyEqSet_right 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {s t : Set α} {l : Filter α} : s ∩ t =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s
• Filter.inter_eventuallyEq_left 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {s t : Set α} {l : Filter α} : s ∩ t =ᶠ[l] s ↔ ∀ᶠ (x : α) in l, x ∈ s → x ∈ t
• Filter.inter_eventuallyEq_right 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {s t : Set α} {l : Filter α} : s ∩ t =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s
• Filter.Eventually.forall_mem 📋 Mathlib.Order.Filter.Basic
  {α : Type u_2} {f : Filter α} {s : Set α} {P : α → Prop} (hP : ∀ᶠ (x : α) in f, P x) (hf : Filter.principal s ≤ f) (x : α) : x ∈ s → P x
• Filter.join_le 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter (Filter α)} {l : Filter α} (h : ∀ᶠ (m : Filter α) in f, m ≤ l) : f.join ≤ l
• Filter.skolem 📋 Mathlib.Order.Filter.Basic
  {ι : Type u_2} {α : ι → Type u_3} [∀ (i : ι), Nonempty (α i)] {P : (i : ι) → α i → Prop} {F : Filter ι} : (∀ᶠ (i : ι) in F, ∃ b, P i b) ↔ ∃ b, ∀ᶠ (i : ι) in F, P i (b i)
• Filter.eventuallyEq_inf_principal_iff 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} {F : Filter α} {s : Set α} {f g : α → β} : f =ᶠ[F ⊓ Filter.principal s] g ↔ ∀ᶠ (x : α) in F, x ∈ s → f x = g x
• Filter.Eventually.ne_bot_of_gt 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [Preorder β] [OrderBot β] {l : Filter α} {f g : α → β} (h : ∀ᶠ (x : α) in l, g x < f x) : ∀ᶠ (x : α) in l, f x ≠ ⊥
• Filter.Eventually.ne_top_of_lt 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [Preorder β] [OrderTop β] {l : Filter α} {f g : α → β} (h : ∀ᶠ (x : α) in l, f x < g x) : ∀ᶠ (x : α) in l, f x ≠ ⊤
• Filter.Eventually.bot_lt_of_ne 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [PartialOrder β] [OrderBot β] {l : Filter α} {f : α → β} (h : ∀ᶠ (x : α) in l, f x ≠ ⊥) : ∀ᶠ (x : α) in l, ⊥ < f x
• Filter.Eventually.lt_top_of_ne 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [PartialOrder β] [OrderTop β] {l : Filter α} {f : α → β} (h : ∀ᶠ (x : α) in l, f x ≠ ⊤) : ∀ᶠ (x : α) in l, f x < ⊤
• Filter.Eventually.bot_lt_iff_ne_bot 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [PartialOrder β] [OrderBot β] {l : Filter α} {f : α → β} : (∀ᶠ (x : α) in l, ⊥ < f x) ↔ ∀ᶠ (x : α) in l, f x ≠ ⊥
• Filter.Eventually.lt_top_iff_ne_top 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {β : Type v} [PartialOrder β] [OrderTop β] {l : Filter α} {f : α → β} : (∀ᶠ (x : α) in l, f x < ⊤) ↔ ∀ᶠ (x : α) in l, f x ≠ ⊤
• Filter.eventually_inf 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f g : Filter α} {p : α → Prop} : (∀ᶠ (x : α) in f ⊓ g, p x) ↔ ∃ s ∈ f, ∃ t ∈ g, ∀ x ∈ s ∩ t, p x
• Filter.eventually_pure 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {a : α} {p : α → Prop} : (∀ᶠ (x : α) in pure a, p x) ↔ p a
• Filter.Eventually.comap 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {g : Filter β} {p : β → Prop} (hf : ∀ᶠ (b : β) in g, p b) (f : α → β) : ∀ᶠ (a : α) in Filter.comap f g, p (f a)
• Filter.eventually_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.canLift 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (c : β → α) (p : α → Prop) [CanLift α β c p] : CanLift (Filter α) (Filter β) (Filter.map c) fun f => ∀ᶠ (x : α) in f, p x
• Filter.eventually_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.eventually_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.eventuallyEq_bind 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : α → Filter β} {g₁ g₂ : β → γ} : g₁ =ᶠ[f.bind m] g₂ ↔ ∀ᶠ (x : α) in f, g₁ =ᶠ[m x] g₂
• Filter.eventuallyLE_bind 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE γ] {f : Filter α} {m : α → Filter β} {g₁ g₂ : β → γ} : g₁ ≤ᶠ[f.bind m] g₂ ↔ ∀ᶠ (x : α) in f, g₁ ≤ᶠ[m x] g₂
• Filter.bind_le 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} {g : α → Filter β} {l : Filter β} (h : ∀ᶠ (x : α) in f, g x ≤ l) : f.bind g ≤ l
• 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.eventually_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 : α⦄, x ∈ s i → q x
• Filter.Tendsto.basis_right 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {β : Type u_2} {ι' : Sort u_4} {la : Filter α} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β} {f : α → β} (H : Filter.Tendsto f la lb) (hlb : lb.HasBasis pb sb) (i : ι') : pb i → ∀ᶠ (x : α) in la, f x ∈ sb i
• Filter.HasBasis.tendsto_right_iff 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {β : Type u_2} {ι' : Sort u_4} {la : Filter α} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β} {f : α → β} (hlb : lb.HasBasis pb sb) : Filter.Tendsto f la lb ↔ ∀ (i : ι'), pb i → ∀ᶠ (x : α) in la, f x ∈ sb i
• Filter.eventually_prod_self_iff' 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {la : Filter α} {r : α × α → Prop} : (∀ᶠ (x : α × α) in la ×ˢ la, r x) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r (x, y)
• Filter.eventually_prod_self_iff 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {la : Filter α} {r : α → α → Prop} : (∀ᶠ (x : α × α) in la ×ˢ la, r x.1 x.2) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r x y
• Filter.eventually_ge_atTop 📋 Mathlib.Order.Filter.AtTopBot.Defs
  {α : Type u_2} [Preorder α] (a : α) : ∀ᶠ (x : α) in Filter.atTop, a ≤ x
• Filter.eventually_le_atBot 📋 Mathlib.Order.Filter.AtTopBot.Defs
  {α : Type u_2} [Preorder α] (a : α) : ∀ᶠ (x : α) in Filter.atBot, x ≤ a
• Filter.eventually_ne_atBot 📋 Mathlib.Order.Filter.AtTopBot.Defs
  {α : Type u_2} [Preorder α] [NoBotOrder α] (a : α) : ∀ᶠ (x : α) in Filter.atBot, x ≠ a
• Filter.eventually_ne_atTop 📋 Mathlib.Order.Filter.AtTopBot.Defs
  {α : Type u_2} [Preorder α] [NoTopOrder α] (a : α) : ∀ᶠ (x : α) in Filter.atTop, x ≠ a
• Filter.eventually_gt_atTop 📋 Mathlib.Order.Filter.AtTopBot.Defs
  {α : Type u_2} [Preorder α] [NoTopOrder α] (a : α) : ∀ᶠ (x : α) in Filter.atTop, a < x
• Filter.eventually_lt_atBot 📋 Mathlib.Order.Filter.AtTopBot.Defs
  {α : Type u_2} [Preorder α] [NoBotOrder α] (a : α) : ∀ᶠ (x : α) in Filter.atBot, x < a
• Antitone.piecewise_eventually_eq_iInter 📋 Mathlib.Order.Filter.AtTopBot.Defs
  {ι : Type u_1} {α : Type u_2} {β : α → Type u_4} [Preorder ι] {s : ι → Set α} [(i : ι) → DecidablePred fun x => x ∈ s i] [DecidablePred fun x => x ∈ ⋂ i, s i] (hs : Antitone s) (f g : (a : α) → β a) (a : α) : ∀ᶠ (i : ι) in Filter.atTop, (s i).piecewise f g a = (⋂ i, s i).piecewise f g a
• Monotone.piecewise_eventually_eq_iUnion 📋 Mathlib.Order.Filter.AtTopBot.Defs
  {ι : Type u_1} {α : Type u_2} {β : α → Type u_4} [Preorder ι] {s : ι → Set α} [(i : ι) → DecidablePred fun x => x ∈ s i] [DecidablePred fun x => x ∈ ⋃ i, s i] (hs : Monotone s) (f g : (a : α) → β a) (a : α) : ∀ᶠ (i : ι) in Filter.atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a
• Filter.tendsto_pure 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {f : α → β} {a : Filter α} {b : β} : Filter.Tendsto f a (pure b) ↔ ∀ᶠ (x : α) in a, f x = b
• Filter.Tendsto.eventually 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {p : β → Prop} (hf : Filter.Tendsto f l₁ l₂) (h : ∀ᶠ (y : β) in l₂, p y) : ∀ᶠ (x : α) in l₁, p (f x)
• Filter.tendsto_iff_eventually 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} : Filter.Tendsto f l₁ l₂ ↔ ∀ ⦃p : β → Prop⦄, (∀ᶠ (y : β) in l₂, p y) → ∀ᶠ (x : α) in l₁, p (f x)
• Filter.tendsto_principal 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : Filter α} {s : Set β} : Filter.Tendsto f l (Filter.principal s) ↔ ∀ᶠ (a : α) in l, f a ∈ s
• Filter.Tendsto.eventually_mem 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {s : Set β} (hf : Filter.Tendsto f l₁ l₂) (h : s ∈ l₂) : ∀ᶠ (x : α) in l₁, f x ∈ s
• Filter.tendsto_iff_forall_eventually_mem 📋 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.eventuallyEq_of_left_inv_of_right_inv 📋 Mathlib.Order.Filter.Tendsto
  {α : Type u_1} {β : Type u_2} {f : α → β} {g₁ g₂ : β → α} {fa : Filter α} {fb : Filter β} (hleft : ∀ᶠ (x : α) in fa, g₁ (f x) = x) (hright : ∀ᶠ (y : β) in fb, f (g₂ y) = y) (htendsto : Filter.Tendsto g₂ fb fa) : g₁ =ᶠ[fb] g₂
• Filter.Tendsto.eventually_ge_atTop 📋 Mathlib.Order.Filter.AtTopBot.Tendsto
  {α : Type u_3} {β : Type u_4} [Preorder β] {f : α → β} {l : Filter α} (hf : Filter.Tendsto f l Filter.atTop) (c : β) : ∀ᶠ (x : α) in l, c ≤ f x
• Filter.Tendsto.eventually_le_atBot 📋 Mathlib.Order.Filter.AtTopBot.Tendsto
  {α : Type u_3} {β : Type u_4} [Preorder β] {f : α → β} {l : Filter α} (hf : Filter.Tendsto f l Filter.atBot) (c : β) : ∀ᶠ (x : α) in l, f x ≤ c
• Filter.tendsto_atBot 📋 Mathlib.Order.Filter.AtTopBot.Tendsto
  {α : Type u_3} {β : Type u_4} [Preorder β] {m : α → β} {f : Filter α} : Filter.Tendsto m f Filter.atBot ↔ ∀ (b : β), ∀ᶠ (a : α) in f, m a ≤ b
• Filter.tendsto_atTop 📋 Mathlib.Order.Filter.AtTopBot.Tendsto
  {α : Type u_3} {β : Type u_4} [Preorder β] {m : α → β} {f : Filter α} : Filter.Tendsto m f Filter.atTop ↔ ∀ (b : β), ∀ᶠ (a : α) in f, b ≤ m a
• Filter.Tendsto.eventually_ne_atTop' 📋 Mathlib.Order.Filter.AtTopBot.Tendsto
  {α : Type u_3} {β : Type u_4} [Preorder β] [NoTopOrder β] {f : α → β} {l : Filter α} (hf : Filter.Tendsto f l Filter.atTop) (c : α) : ∀ᶠ (x : α) in l, x ≠ c
• Filter.Tendsto.eventually_ne_atBot 📋 Mathlib.Order.Filter.AtTopBot.Tendsto
  {α : Type u_3} {β : Type u_4} [Preorder β] [NoBotOrder β] {f : α → β} {l : Filter α} (hf : Filter.Tendsto f l Filter.atBot) (c : β) : ∀ᶠ (x : α) in l, f x ≠ c
• Filter.Tendsto.eventually_ne_atTop 📋 Mathlib.Order.Filter.AtTopBot.Tendsto
  {α : Type u_3} {β : Type u_4} [Preorder β] [NoTopOrder β] {f : α → β} {l : Filter α} (hf : Filter.Tendsto f l Filter.atTop) (c : β) : ∀ᶠ (x : α) in l, f x ≠ c
• Filter.Tendsto.eventually_gt_atTop 📋 Mathlib.Order.Filter.AtTopBot.Tendsto
  {α : Type u_3} {β : Type u_4} [Preorder β] [NoTopOrder β] {f : α → β} {l : Filter α} (hf : Filter.Tendsto f l Filter.atTop) (c : β) : ∀ᶠ (x : α) in l, c < f x
• Filter.Tendsto.eventually_lt_atBot 📋 Mathlib.Order.Filter.AtTopBot.Tendsto
  {α : Type u_3} {β : Type u_4} [Preorder β] [NoBotOrder β] {f : α → β} {l : Filter α} (hf : Filter.Tendsto f l Filter.atBot) (c : β) : ∀ᶠ (x : α) in l, f x < c
• Filter.extraction_of_eventually_atTop 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {P : ℕ → Prop} (h : ∀ᶠ (n : ℕ) in Filter.atTop, P n) : ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
• Filter.extraction_forall_of_eventually 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {P : ℕ → ℕ → Prop} (h : ∀ (n : ℕ), ∀ᶠ (k : ℕ) in Filter.atTop, P n k) : ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
• Filter.Eventually.exists_forall_of_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.Eventually.exists_forall_of_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.eventually_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.eventually_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.HasAntitoneBasis.eventually_subset 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {ι : Type u_1} {α : Type u_3} [Preorder ι] {l : Filter α} {s : ι → Set α} (hl : l.HasAntitoneBasis s) {t : Set α} (ht : t ∈ l) : ∀ᶠ (i : ι) in Filter.atTop, s i ⊆ t
• Filter.exists_eventually_atBot 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {β : Type u_4} {α : Type u_5} [Preorder α] [IsCodirectedOrder α] [Nonempty α] {r : α → β → Prop} : (∃ b, ∀ᶠ (a : α) in Filter.atBot, r a b) ↔ ∀ᶠ (a₀ : α) in Filter.atBot, ∃ b, ∀ a ≤ a₀, r a b
• Filter.exists_eventually_atTop 📋 Mathlib.Order.Filter.AtTopBot.Basic
  {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirectedOrder α] [Nonempty α] {r : α → β → Prop} : (∃ b, ∀ᶠ (a : α) in Filter.atTop, r a b) ↔ ∀ᶠ (a₀ : α) in Filter.atTop, ∃ b, ∀ (a : α), a₀ ≤ a → r a b
• Module.End.eventually_disjoint_ker_pow_range_pow 📋 Mathlib.RingTheory.Noetherian.Defs
  {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] (f : Module.End R M) : ∀ᶠ (n : ℕ) in Filter.atTop, Disjoint (f ^ n).ker (f ^ n).range
• LinearMap.eventually_iSup_ker_pow_eq 📋 Mathlib.RingTheory.Noetherian.Defs
  {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [IsNoetherian R M] (f : M →ₗ[R] M) : ∀ᶠ (n : ℕ) in Filter.atTop, ⨆ m, (f ^ m).ker = (f ^ n).ker
• Filter.eventually_all 📋 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.eventually_all_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.eventually_all 📋 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.eventually_subset_of_finite 📋 Mathlib.Order.Filter.Finite
  {α : Type u} {ι : Type u_1} {f : Filter ι} {s : ι → Set α} {t : Set α} (ht : t.Finite) (hs : ∀ a ∈ t, ∀ᶠ (i : ι) in f, a ∈ s i) : ∀ᶠ (i : ι) in f, t ⊆ s i
• Filter.eventually_all_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.eventually_all 📋 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.Eventually.eval_pi 📋 Mathlib.Order.Filter.Pi
  {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {p : (i : ι) → α i → Prop} {i : ι} (hf : ∀ᶠ (x : α i) in f i, p i x) : ∀ᶠ (x : (i : ι) → α i) in Filter.pi f, p i (x i)
• Filter.eventually_pi 📋 Mathlib.Order.Filter.Pi
  {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {p : (i : ι) → α i → Prop} [Finite ι] (hf : ∀ (i : ι), ∀ᶠ (x : α i) in f i, p i x) : ∀ᶠ (x : (i : ι) → α i) in Filter.pi f, ∀ (i : ι), p i (x i)
• Filter.Eventually.diag_of_prod 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {f : Filter α} {p : α × α → Prop} (h : ∀ᶠ (i : α × α) in f ×ˢ f, p i) : ∀ᶠ (i : α) in f, p (i, i)
• Filter.Eventually.prod_inl 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {la : Filter α} {p : α → Prop} (h : ∀ᶠ (x : α) in la, p x) (lb : Filter β) : ∀ᶠ (x : α × β) in la ×ˢ lb, p x.1
• Filter.Eventually.prod_inr 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {lb : Filter β} {p : β → Prop} (h : ∀ᶠ (x : β) in lb, p x) (la : Filter α) : ∀ᶠ (x : α × β) in la ×ˢ lb, p x.2
• Filter.Eventually.curry 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {p : α × β → Prop} (h : ∀ᶠ (x : α × β) in la ×ˢ lb, p x) : ∀ᶠ (x : α) in la, ∀ᶠ (y : β) in lb, p (x, y)
• Filter.Eventually.prod_mk 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {la : Filter α} {pa : α → Prop} (ha : ∀ᶠ (x : α) in la, pa x) {lb : Filter β} {pb : β → Prop} (hb : ∀ᶠ (y : β) in lb, pb y) : ∀ᶠ (p : α × β) in la ×ˢ lb, pa p.1 ∧ pb p.2
• Filter.eventually_prod_principal_iff 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {f : Filter α} {p : α × β → Prop} {s : Set β} : (∀ᶠ (x : α × β) in f ×ˢ Filter.principal s, p x) ↔ ∀ᶠ (x : α) in f, ∀ y ∈ s, p (x, y)
• Filter.Eventually.image_of_prod 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {y : α → β} {r : α → β → Prop} (hy : Filter.Tendsto y f g) (hr : ∀ᶠ (p : α × β) in f ×ˢ g, r p.1 p.2) : ∀ᶠ (x : α) in f, r x (y x)
• Filter.eventually_swap_iff 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {p : α × β → Prop} : (∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap
• Filter.eventually_prod_iff 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {p : α × β → Prop} : (∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔ ∃ pa, (∀ᶠ (x : α) in f, pa x) ∧ ∃ pb, (∀ᶠ (y : β) in g, pb y) ∧ ∀ {x : α}, pa x → ∀ {y : β}, pb y → p (x, y)
• Filter.mem_prod_iff_left 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {s : Set (α × β)} : s ∈ f ×ˢ g ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s
• Filter.mem_prod_iff_right 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {s : Set (α × β)} : s ∈ f ×ˢ g ↔ ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s
• Filter.Eventually.eventually_prod_of_eventually_swap 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} [g.NeBot] {p : α → β → Prop} {q : β → γ → Prop} {r : α → γ → Prop} (hp : ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p x y) (hq : ∀ᶠ (z : γ) in h, ∀ᶠ (y : β) in g, q y z) (hpqr : ∀ (x : α) (y : β) (z : γ), p x y → q y z → r x z) : ∀ᶠ (xz : α × γ) in f ×ˢ h, r xz.1 xz.2
• Filter.Eventually.diag_of_prod_left 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {γ : Type u_3} {f : Filter α} {g : Filter γ} {p : (α × α) × γ → Prop} : (∀ᶠ (x : (α × α) × γ) in (f ×ˢ f) ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p ((x.1, x.1), x.2)
• Filter.Eventually.diag_of_prod_right 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {γ : Type u_3} {f : Filter α} {g : Filter γ} {p : α × γ × γ → Prop} : (∀ᶠ (x : α × γ × γ) in f ×ˢ g ×ˢ g, p x) → ∀ᶠ (x : α × γ) in f ×ˢ g, p (x.1, x.2, x.2)
• Filter.Eventually.trans_prod 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Filter β} {h : Filter γ} [g.NeBot] {p : α → β → Prop} {q : β → γ → Prop} {r : α → γ → Prop} (hp : ∀ᶠ (xy : α × β) in f ×ˢ g, p xy.1 xy.2) (hq : ∀ᶠ (yz : β × γ) in g ×ˢ h, q yz.1 yz.2) (hpqr : ∀ (x : α) (y : β) (z : γ), p x y → q y z → r x z) : ∀ᶠ (xz : α × γ) in f ×ˢ h, r xz.1 xz.2
• Filter.eventually_cofinite_ne 📋 Mathlib.Order.Filter.Cofinite
  {α : Type u_2} (x : α) : ∀ᶠ (a : α) in Filter.cofinite, a ≠ x
• Nat.eventually_pos 📋 Mathlib.Order.Filter.Cofinite
  : ∀ᶠ (k : ℕ) in Filter.atTop, 0 < k
• Filter.eventually_cofinite 📋 Mathlib.Order.Filter.Cofinite
  {α : Type u_2} {p : α → Prop} : (∀ᶠ (x : α) in Filter.cofinite, p x) ↔ {x | ¬p x}.Finite
• Set.Finite.eventually_cofinite_notMem 📋 Mathlib.Order.Filter.Cofinite
  {α : Type u_2} {s : Set α} (hs : s.Finite) : ∀ᶠ (x : α) in Filter.cofinite, x ∉ s
• Finset.eventually_cofinite_notMem 📋 Mathlib.Order.Filter.Cofinite
  {α : Type u_2} (s : Finset α) : ∀ᶠ (x : α) in Filter.cofinite, x ∉ s
• Filter.le_cofinite_iff_eventually_ne 📋 Mathlib.Order.Filter.Cofinite
  {α : Type u_2} {l : Filter α} : l ≤ Filter.cofinite ↔ ∀ (x : α), ∀ᶠ (y : α) in l, y ≠ x
• Filter.map_piMap_pi 📋 Mathlib.Order.Filter.Cofinite
  {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {f : (i : ι) → α i → β i} (hf : ∀ᶠ (i : ι) in Filter.cofinite, Function.Surjective (f i)) (l : (i : ι) → Filter (α i)) : Filter.map (Pi.map f) (Filter.pi l) = Filter.pi fun i => Filter.map (f i) (l i)
• Filter.univ_pi_mem_pi 📋 Mathlib.Order.Filter.Cofinite
  {ι : Type u_1} {α : ι → Type u_4} {s : (i : ι) → Set (α i)} {l : (i : ι) → Filter (α i)} (h : ∀ (i : ι), s i ∈ l i) (hfin : ∀ᶠ (i : ι) in Filter.cofinite, s i = Set.univ) : Set.univ.pi s ∈ Filter.pi l
• Polynomial.eventually_cofinite_not_isRoot 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p ≠ 0) : ∀ᶠ (x : R) in Filter.cofinite, ¬p.IsRoot x
• Polynomial.eventually_eval_ne_zero_cofinite 📋 Mathlib.Algebra.Polynomial.Roots
  {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hp : p ≠ 0) : ∀ᶠ (x : R) in Filter.cofinite, Polynomial.eval x p ≠ 0
• 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
• Ultrafilter.em 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Ultrafilter α) (p : α → Prop) : (∀ᶠ (x : α) in ↑f, p x) ∨ ∀ᶠ (x : α) in ↑f, ¬p x
• Ultrafilter.eventually_not 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f : Ultrafilter α} {p : α → Prop} : (∀ᶠ (x : α) in ↑f, ¬p x) ↔ ¬∀ᶠ (x : α) in ↑f, p x
• Ultrafilter.eventually_imp 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f : Ultrafilter α} {p q : α → Prop} : (∀ᶠ (x : α) in ↑f, p x → q x) ↔ (∀ᶠ (x : α) in ↑f, p x) → ∀ᶠ (x : α) in ↑f, q x
• Ultrafilter.eventually_or 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f : Ultrafilter α} {p q : α → Prop} : (∀ᶠ (x : α) in ↑f, p x ∨ q x) ↔ (∀ᶠ (x : α) in ↑f, p x) ∨ ∀ᶠ (x : α) in ↑f, q x
• Filter.eventually_one 📋 Mathlib.Order.Filter.Pointwise
  {α : Type u_2} [One α] {p : α → Prop} : (∀ᶠ (x : α) in 1, p x) ↔ p 1
• Filter.eventually_zero 📋 Mathlib.Order.Filter.Pointwise
  {α : Type u_2} [Zero α] {p : α → Prop} : (∀ᶠ (x : α) in 0, p x) ↔ p 0
• Filter.eventually_inv 📋 Mathlib.Order.Filter.Pointwise
  {α : Type u_2} [Inv α] {f : Filter α} {p : α → Prop} : (∀ᶠ (x : α) in f⁻¹, p x) ↔ ∀ᶠ (x : α) in f, p x⁻¹
• Filter.eventually_neg 📋 Mathlib.Order.Filter.Pointwise
  {α : Type u_2} [Neg α] {f : Filter α} {p : α → Prop} : (∀ᶠ (x : α) in -f, p x) ↔ ∀ᶠ (x : α) in f, p (-x)
• Filter.tendsto_one 📋 Mathlib.Order.Filter.Pointwise
  {α : Type u_2} {β : Type u_3} [One α] {a : Filter β} {f : β → α} : Filter.Tendsto f a 1 ↔ ∀ᶠ (x : β) in a, f x = 1
• Filter.tendsto_zero 📋 Mathlib.Order.Filter.Pointwise
  {α : Type u_2} {β : Type u_3} [Zero α] {a : Filter β} {f : β → α} : Filter.Tendsto f a 0 ↔ ∀ᶠ (x : β) in a, f x = 0
• Filter.eventually_smul_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.eventually_vadd_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.eventually_forall_ge_atTop 📋 Mathlib.Order.Filter.AtTopBot.Finite
  {α : Type u_2} [Preorder α] {p : α → Prop} : (∀ᶠ (x : α) in Filter.atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in Filter.atTop, p x
• Filter.eventually_forall_le_atBot 📋 Mathlib.Order.Filter.AtTopBot.Finite
  {α : Type u_2} [Preorder α] {p : α → Prop} : (∀ᶠ (x : α) in Filter.atBot, ∀ y ≤ x, p y) ↔ ∀ᶠ (x : α) in Filter.atBot, p x
• Nat.eventually_pow_lt_factorial_sub 📋 Mathlib.Order.Filter.AtTopBot.Finite
  (c d : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, c ^ n < (n - d).factorial
• Filter.Tendsto.eventually_forall_ge_atTop 📋 Mathlib.Order.Filter.AtTopBot.Finite
  {α : Type u_2} {β : Type u_3} [Preorder β] {l : Filter α} {p : β → Prop} {f : α → β} (hf : Filter.Tendsto f l Filter.atTop) (h_evtl : ∀ᶠ (x : β) in Filter.atTop, p x) : ∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y
• Filter.Tendsto.eventually_forall_le_atBot 📋 Mathlib.Order.Filter.AtTopBot.Finite
  {α : Type u_2} {β : Type u_3} [Preorder β] {l : Filter α} {p : β → Prop} {f : α → β} (hf : Filter.Tendsto f l Filter.atBot) (h_evtl : ∀ᶠ (x : β) in Filter.atBot, p x) : ∀ᶠ (x : α) in l, ∀ y ≤ f x, p y
• Nat.eventually_mul_pow_lt_factorial_sub 📋 Mathlib.Order.Filter.AtTopBot.Finite
  (a c d : ℕ) : ∀ᶠ (n : ℕ) in Filter.atTop, a * c ^ n < (n - d).factorial
• Filter.Eventually.atTop_of_arithmetic 📋 Mathlib.Order.Filter.AtTopBot.Finite
  {p : ℕ → Prop} {n : ℕ} (hn : n ≠ 0) (hp : ∀ k < n, ∀ᶠ (a : ℕ) in Filter.atTop, p (n * a + k)) : ∀ᶠ (a : ℕ) in Filter.atTop, p a
• Filter.HasAntitoneBasis.subbasis_with_rel 📋 Mathlib.Order.Filter.AtTopBot.Finite
  {α : Type u_2} {f : Filter α} {s : ℕ → Set α} (hs : f.HasAntitoneBasis s) {r : ℕ → ℕ → Prop} (hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, r m n) : ∃ φ, StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)
• Filter.eventually_atBot_curry 📋 Mathlib.Order.Filter.AtTopBot.Prod
  {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {p : α × β → Prop} (hp : ∀ᶠ (x : α × β) in Filter.atBot, p x) : ∀ᶠ (k : α) in Filter.atBot, ∀ᶠ (l : β) in Filter.atBot, p (k, l)
• Filter.eventually_atTop_curry 📋 Mathlib.Order.Filter.AtTopBot.Prod
  {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {p : α × β → Prop} (hp : ∀ᶠ (x : α × β) in Filter.atTop, p x) : ∀ᶠ (k : α) in Filter.atTop, ∀ᶠ (l : β) in Filter.atTop, p (k, l)
• Filter.eventually_atBot_prod_self 📋 Mathlib.Order.Filter.AtTopBot.Prod
  {α : Type u_3} [Nonempty α] [Preorder α] [IsCodirectedOrder α] {p : α × α → Prop} : (∀ᶠ (x : α × α) in Filter.atBot, p x) ↔ ∃ a, ∀ (k l : α), k ≤ a → l ≤ a → p (k, l)
• Filter.eventually_atBot_prod_self' 📋 Mathlib.Order.Filter.AtTopBot.Prod
  {α : Type u_3} [Nonempty α] [Preorder α] [IsCodirectedOrder α] {p : α × α → Prop} : (∀ᶠ (x : α × α) in Filter.atBot, p x) ↔ ∃ a, ∀ k ≤ a, ∀ l ≤ a, p (k, l)
• Filter.eventually_atTop_prod_self 📋 Mathlib.Order.Filter.AtTopBot.Prod
  {α : Type u_3} [Nonempty α] [Preorder α] [IsDirectedOrder α] {p : α × α → Prop} : (∀ᶠ (x : α × α) in Filter.atTop, p x) ↔ ∃ a, ∀ (k l : α), a ≤ k → a ≤ l → p (k, l)
• Filter.eventually_atTop_prod_self' 📋 Mathlib.Order.Filter.AtTopBot.Prod
  {α : Type u_3} [Nonempty α] [Preorder α] [IsDirectedOrder α] {p : α × α → Prop} : (∀ᶠ (x : α × α) in Filter.atTop, p x) ↔ ∃ a, ∀ k ≥ a, ∀ l ≥ a, p (k, l)
• Filter.eventually_iff_seq_eventually 📋 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.eventually_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.Tendsto.curry 📋 Mathlib.Order.Filter.Curry
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {la : Filter α} {lb : Filter β} {lc : Filter γ} (h : ∀ᶠ (a : α) in la, Filter.Tendsto (fun b => f a b) lb lc) : Filter.Tendsto (↿f) (la.curry lb) lc
• Filter.mem_curry_iff 📋 Mathlib.Order.Filter.Curry
  {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} {s : Set (α × β)} : s ∈ l.curry m ↔ ∀ᶠ (x : α) in l, ∀ᶠ (y : β) in m, (x, y) ∈ s
• Filter.eventually_curry_prod_iff 📋 Mathlib.Order.Filter.Curry
  {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} {s : Set α} {t : Set β} [l.NeBot] [m.NeBot] : (∀ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t) ↔ s ∈ l ∧ t ∈ m
• Filter.tendsto_lift' 📋 Mathlib.Order.Filter.Lift
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {h : Set α → Set β} {m : γ → β} {l : Filter γ} : Filter.Tendsto m l (f.lift' h) ↔ ∀ s ∈ f, ∀ᶠ (a : γ) in l, m a ∈ h s
• Filter.eventually_lift'_iff 📋 Mathlib.Order.Filter.Lift
  {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β} (hh : Monotone h) {p : β → Prop} : (∀ᶠ (y : β) in f.lift' h, p y) ↔ ∃ t ∈ f, ∀ y ∈ h t, p y
• Filter.Eventually.self_of_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} (h : ∀ᶠ (y : X) in nhds x, p y) : p x
• isOpen_setOfPred_eventually_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {p : X → Prop} : IsOpen {x | ∀ᶠ (y : X) in nhds x, p y}
• isOpen_setOf_eventually_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {p : X → Prop} : IsOpen {x | ∀ᶠ (y : X) in nhds x, p y}
• tendsto_nhds_of_eventually_eq 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {l : Filter α} {f : α → X} (h : ∀ᶠ (x' : α) in l, f x' = x) : Filter.Tendsto f l (nhds x)
• interior_setOfPred_eq 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {p : X → Prop} : interior {x | p x} = {x | ∀ᶠ (y : X) in nhds x, p y}
• interior_setOf_eq 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {p : X → Prop} : interior {x | p x} = {x | ∀ᶠ (y : X) in nhds x, p y}
• Filter.Eventually.eventually_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} (h : ∀ᶠ (y : X) in nhds x, p y) : ∀ᶠ (y : X) in nhds x, ∀ᶠ (x : X) in nhds y, p x
• eventually_eventually_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} : (∀ᶠ (y : X) in nhds x, ∀ᶠ (x : X) in nhds y, p x) ↔ ∀ᶠ (x : X) in nhds x, p x

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