Loogle!

Result

Found 218 declarations mentioning Ultrafilter. Of these, only the first 200 are shown.

• Ultrafilter 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  (α : Type u_2) : Type u_2
• Ultrafilter.functor 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  : Functor Ultrafilter
• Ultrafilter.instBind 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  : Bind Ultrafilter
• Ultrafilter.instPure 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  : Pure Ultrafilter
• Ultrafilter.monad 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  : Monad Ultrafilter
• Ultrafilter.lawfulMonad 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  : LawfulMonad Ultrafilter
• Ultrafilter.toFilter 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u_2} (self : Ultrafilter α) : Filter α
• Ultrafilter.instCoeTCFilter 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} : CoeTC (Ultrafilter α) (Filter α)
• Ultrafilter.instInhabited 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} [Inhabited α] : Inhabited (Ultrafilter α)
• Ultrafilter.instMembershipSet 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} : Membership (Set α) (Ultrafilter α)
• Ultrafilter.instNonempty 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} [Nonempty α] : Nonempty (Ultrafilter α)
• Ultrafilter.coe_injective 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} : Function.Injective Ultrafilter.toFilter
• Ultrafilter.map 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {β : Type v} (m : α → β) (f : Ultrafilter α) : Ultrafilter β
• Ultrafilter.neBot 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Ultrafilter α) : (↑f).NeBot
• Ultrafilter.neBot' 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u_2} (self : Ultrafilter α) : (↑self).NeBot
• Ultrafilter.of 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Filter α) [f.NeBot] : Ultrafilter α
• Ultrafilter.bind 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {β : Type v} (f : Ultrafilter α) (m : α → Ultrafilter β) : Ultrafilter β
• Ultrafilter.pure_injective 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} : Function.Injective pure
• Ultrafilter.map_id 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Ultrafilter α) : Ultrafilter.map id f = f
• Ultrafilter.map_id' 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Ultrafilter α) : Ultrafilter.map (fun x => x) f = f
• Ultrafilter.of_coe 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Ultrafilter α) : Ultrafilter.of ↑f = f
• Ultrafilter.coe_pure 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (a : α) : ↑(pure a) = pure a
• Ultrafilter.empty_notMem 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f : Ultrafilter α} : ∅ ∉ f
• Ultrafilter.nonempty_of_mem 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f : Ultrafilter α} {s : Set α} (hs : s ∈ f) : s.Nonempty
• Ultrafilter.coe_inj 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f g : Ultrafilter α} : ↑f = ↑g ↔ f = g
• 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.coe_map 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {β : Type v} (m : α → β) (f : Ultrafilter α) : ↑(Ultrafilter.map m f) = Filter.map m ↑f
• Ultrafilter.em 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Ultrafilter α) (p : α → Prop) : (∀ᶠ (x : α) in ↑f, p x) ∨ ∀ᶠ (x : α) in ↑f, ¬p x
• Ultrafilter.map_pure 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {β : Type v} (m : α → β) (a : α) : Ultrafilter.map m (pure a) = pure (m a)
• Ultrafilter.ne_empty_of_mem 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f : Ultrafilter α} {s : Set α} (hs : s ∈ f) : s ≠ ∅
• Ultrafilter.ofComapInfPrincipal 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {β : Type v} {m : α → β} {s : Set α} {g : Ultrafilter β} (h : m '' s ∈ g) : Ultrafilter α
• Ultrafilter.comap 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {β : Type v} {m : α → β} (u : Ultrafilter β) (inj : Function.Injective m) (large : Set.range m ∈ u) : Ultrafilter α
• Ultrafilter.eventually_not 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f : Ultrafilter α} {p : α → Prop} : (∀ᶠ (x : α) in ↑f, ¬p x) ↔ ¬∀ᶠ (x : α) in ↑f, p x
• Filter.exists_ultrafilter_le 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Filter α) [h : f.NeBot] : ∃ u, ↑u ≤ f
• Ultrafilter.exists_le 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Filter α) [h : f.NeBot] : ∃ u, ↑u ≤ f
• Ultrafilter.mem_coe 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f : Ultrafilter α} {s : Set α} : s ∈ ↑f ↔ s ∈ f
• Ultrafilter.mem_pure 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {a : α} {s : Set α} : s ∈ pure a ↔ a ∈ s
• Filter.exists_ultrafilter_iff 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f : Filter α} : (∃ u, ↑u ≤ f) ↔ f.NeBot
• Ultrafilter.eq_of_le 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f g : Ultrafilter α} (h : ↑f ≤ ↑g) : f = g
• Ultrafilter.coe_le_coe 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f g : Ultrafilter α} : ↑f ≤ ↑g ↔ f = g
• Ultrafilter.mem_or_compl_mem 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Ultrafilter α) (s : Set α) : s ∈ f ∨ sᶜ ∈ f
• Ultrafilter.compl_mem_iff_notMem 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f : Ultrafilter α} {s : Set α} : sᶜ ∈ f ↔ s ∉ f
• Ultrafilter.compl_notMem_iff 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f : Ultrafilter α} {s : Set α} : sᶜ ∉ f ↔ s ∈ f
• Ultrafilter.isAtom 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Ultrafilter α) : IsAtom ↑f
• Ultrafilter.ofAtom 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Filter α) (hf : IsAtom f) : Ultrafilter α
• Ultrafilter.ext 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} ⦃f g : Ultrafilter α⦄ (h : ∀ (s : Set α), s ∈ f ↔ s ∈ g) : f = g
• Ultrafilter.le_of_inf_neBot 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Ultrafilter α) {g : Filter α} (hg : (↑f ⊓ g).NeBot) : ↑f ≤ g
• Ultrafilter.le_of_inf_neBot' 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Ultrafilter α) {g : Filter α} (hg : (g ⊓ ↑f).NeBot) : ↑f ≤ g
• Ultrafilter.map_map 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {β : Type v} {γ : Type u_1} (f : Ultrafilter α) (m : α → β) (n : β → γ) : Ultrafilter.map n (Ultrafilter.map m f) = Ultrafilter.map (n ∘ m) f
• Ultrafilter.ext_iff 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f g : Ultrafilter α} : f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
• Ultrafilter.inf_neBot_iff 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f : Ultrafilter α} {g : Filter α} : (↑f ⊓ g).NeBot ↔ ↑f ≤ g
• Ultrafilter.ofComplNotMemIff 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Filter α) (h : ∀ (s : Set α), sᶜ ∉ f ↔ s ∈ f) : Ultrafilter α
• Ultrafilter.unique 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Ultrafilter α) {g : Filter α} (h : g ≤ ↑f) (hne : g.NeBot := by infer_instance) : g = ↑f
• 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.mem_map 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {β : Type v} {m : α → β} {f : Ultrafilter α} {s : Set β} : s ∈ Ultrafilter.map m f ↔ m ⁻¹' s ∈ f
• 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
• Ultrafilter.ofComapInfPrincipal_eq_of_map 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {β : Type v} {m : α → β} {s : Set α} {g : Ultrafilter β} (h : m '' s ∈ g) : Ultrafilter.map m (Ultrafilter.ofComapInfPrincipal h) = g
• Ultrafilter.ofComapInfPrincipal_mem 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {β : Type v} {m : α → β} {s : Set α} {g : Ultrafilter β} (h : m '' s ∈ g) : s ∈ Ultrafilter.ofComapInfPrincipal h
• Ultrafilter.comap_inf_principal_neBot_of_image_mem 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {β : Type v} {m : α → β} {s : Set α} {g : Ultrafilter β} (h : m '' s ∈ g) : (Filter.comap m ↑g ⊓ Filter.principal s).NeBot
• Ultrafilter.le_of_le 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u_2} (self : Ultrafilter α) (g : Filter α) : g.NeBot → g ≤ ↑self → ↑self ≤ g
• Ultrafilter.mk 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u_2} (toFilter : Filter α) (neBot' : toFilter.NeBot) (le_of_le : ∀ (g : Filter α), g.NeBot → g ≤ toFilter → toFilter ≤ g) : Ultrafilter α
• Ultrafilter.comap_id 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Ultrafilter α) (h₀ : Function.Injective id := ⋯) (h₁ : Set.range id ∈ f := ⋯) : f.comap h₀ h₁ = f
• Filter.mem_iff_ultrafilter 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f : Filter α} {s : Set α} : s ∈ f ↔ ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
• Ultrafilter.coe_comap 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {β : Type v} {m : α → β} (u : Ultrafilter β) (inj : Function.Injective m) (large : Set.range m ∈ u) : ↑(u.comap inj large) = Filter.comap m ↑u
• Ultrafilter.union_mem_iff 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f : Ultrafilter α} {s t : Set α} : s ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f
• Ultrafilter.diff_mem_iff 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {s t : Set α} (f : Ultrafilter α) : s \ t ∈ f ↔ s ∈ f ∧ t ∉ f
• Ultrafilter.sdiff_mem_iff 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {s t : Set α} (f : Ultrafilter α) : s \ t ∈ f ↔ s ∈ f ∧ t ∉ f
• Ultrafilter.comap_pure 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {β : Type v} {m : α → β} (a : α) (inj : Function.Injective m) (large : Set.range m ∈ pure (m a)) : (pure (m a)).comap inj large = pure a
• Ultrafilter.disjoint_iff_not_le 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f : Ultrafilter α} {g : Filter α} : Disjoint (↑f) g ↔ ¬↑f ≤ g
• Filter.le_iff_ultrafilter 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {f₁ f₂ : Filter α} : f₁ ≤ f₂ ↔ ∀ (g : Ultrafilter α), ↑g ≤ f₁ → ↑g ≤ f₂
• Ultrafilter.mem_comap 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {β : Type v} {m : α → β} (u : Ultrafilter β) (inj : Function.Injective m) (large : Set.range m ∈ u) {s : Set α} : s ∈ u.comap inj large ↔ m '' s ∈ u
• Filter.iSup_ultrafilter_le_eq 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} (f : Filter α) : ⨆ g, ⨆ (_ : ↑g ≤ f), ↑g = f
• Ultrafilter.le_sup_iff 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {u : Ultrafilter α} {f g : Filter α} : ↑u ≤ f ⊔ g ↔ ↑u ≤ f ∨ ↑u ≤ g
• Filter.forall_neBot_le_iff 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {g : Filter α} {p : Filter α → Prop} (hp : Monotone p) : (∀ (f : Filter α), f.NeBot → f ≤ g → p f) ↔ ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
• Ultrafilter.comap_comap 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {β : Type v} {γ : Type u_1} (f : Ultrafilter γ) {m : α → β} {n : β → γ} (inj₀ : Function.Injective n) (large₀ : Set.range n ∈ f) (inj₁ : Function.Injective m) (large₁ : Set.range m ∈ f.comap inj₀ large₀) (inj₂ : Function.Injective (n ∘ m) := ⋯) (large₂ : Set.range (n ∘ m) ∈ f := ⋯) : (f.comap inj₀ large₀).comap inj₁ large₁ = f.comap inj₂ large₂
• Filter.hyperfilter 📋 Mathlib.Order.Filter.Ultrafilter.Basic
  (α : Type u) [Infinite α] : Ultrafilter α
• Ultrafilter.eq_pure_of_finite 📋 Mathlib.Order.Filter.Ultrafilter.Basic
  {α : Type u} [Finite α] (f : Ultrafilter α) : ∃ a, f = pure a
• Filter.notMem_hyperfilter_of_finite 📋 Mathlib.Order.Filter.Ultrafilter.Basic
  {α : Type u} [Infinite α] {s : Set α} (hf : s.Finite) : s ∉ Filter.hyperfilter α
• Set.Finite.notMem_hyperfilter 📋 Mathlib.Order.Filter.Ultrafilter.Basic
  {α : Type u} [Infinite α] {s : Set α} (hf : s.Finite) : s ∉ Filter.hyperfilter α
• Filter.compl_mem_hyperfilter_of_finite 📋 Mathlib.Order.Filter.Ultrafilter.Basic
  {α : Type u} [Infinite α] {s : Set α} (hf : s.Finite) : sᶜ ∈ Filter.hyperfilter α
• Filter.mem_hyperfilter_of_finite_compl 📋 Mathlib.Order.Filter.Ultrafilter.Basic
  {α : Type u} [Infinite α] {s : Set α} (hf : sᶜ.Finite) : s ∈ Filter.hyperfilter α
• Set.Finite.compl_mem_hyperfilter 📋 Mathlib.Order.Filter.Ultrafilter.Basic
  {α : Type u} [Infinite α] {s : Set α} (hf : s.Finite) : sᶜ ∈ Filter.hyperfilter α
• Ultrafilter.le_cofinite_or_eq_pure 📋 Mathlib.Order.Filter.Ultrafilter.Basic
  {α : Type u} (f : Ultrafilter α) : ↑f ≤ Filter.cofinite ∨ ∃ a, f = pure a
• Ultrafilter.eventually_exists_iff 📋 Mathlib.Order.Filter.Ultrafilter.Basic
  {α : Type u} {β : Type v} {f : Ultrafilter α} [Finite β] {P : β → α → Prop} : (∀ᶠ (i : α) in ↑f, ∃ a, P a i) ↔ ∃ a, ∀ᶠ (i : α) in ↑f, P a i
• Ultrafilter.eq_pure_of_finite_mem 📋 Mathlib.Order.Filter.Ultrafilter.Basic
  {α : Type u} {f : Ultrafilter α} {s : Set α} (h : s.Finite) (h' : s ∈ f) : ∃ x ∈ s, f = pure x
• Filter.tendsto_iff_ultrafilter 📋 Mathlib.Order.Filter.Ultrafilter.Basic
  {α : Type u} {β : Type v} (f : α → β) (l₁ : Filter α) (l₂ : Filter β) : Filter.Tendsto f l₁ l₂ ↔ ∀ (g : Ultrafilter α), ↑g ≤ l₁ → Filter.Tendsto f (↑g) l₂
• Ultrafilter.finite_sUnion_mem_iff 📋 Mathlib.Order.Filter.Ultrafilter.Basic
  {α : Type u} {f : Ultrafilter α} {s : Set (Set α)} (hs : s.Finite) : ⋃₀ s ∈ f ↔ ∃ t ∈ s, t ∈ f
• Ultrafilter.eventually_exists_mem_iff 📋 Mathlib.Order.Filter.Ultrafilter.Basic
  {α : Type u} {β : Type v} {f : Ultrafilter α} {is : Set β} {P : β → α → Prop} (his : is.Finite) : (∀ᶠ (i : α) in ↑f, ∃ a ∈ is, P a i) ↔ ∃ a ∈ is, ∀ᶠ (i : α) in ↑f, P a i
• Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty 📋 Mathlib.Order.Filter.Ultrafilter.Basic
  {α : Type u} (S : Set (Set α)) (cond : ∀ (T : Finset (Set α)), ↑T ⊆ S → (⋂₀ ↑T).Nonempty) : ∃ F, S ⊆ (↑F).sets
• Ultrafilter.finite_biUnion_mem_iff 📋 Mathlib.Order.Filter.Ultrafilter.Basic
  {α : Type u} {β : Type v} {f : Ultrafilter α} {is : Set β} {s : β → Set α} (his : is.Finite) : ⋃ i ∈ is, s i ∈ f ↔ ∃ i ∈ is, s i ∈ f
• Ultrafilter.clusterPt_iff 📋 Mathlib.Topology.Ultrafilter
  {X : Type u} {x : X} [TopologicalSpace X] {f : Ultrafilter X} : ClusterPt x ↑f ↔ ↑f ≤ nhds x
• continuous_iff_ultrafilter 📋 Mathlib.Topology.Ultrafilter
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : Continuous f ↔ ∀ (x : X) (g : Ultrafilter X), ↑g ≤ nhds x → Filter.Tendsto f (↑g) (nhds (f x))
• isClosed_iff_ultrafilter 📋 Mathlib.Topology.Ultrafilter
  {X : Type u} {s : Set X} [TopologicalSpace X] : IsClosed s ↔ ∀ (x : X) (u : Ultrafilter X), ↑u ≤ nhds x → s ∈ u → x ∈ s
• isOpen_iff_ultrafilter 📋 Mathlib.Topology.Ultrafilter
  {X : Type u} {s : Set X} [TopologicalSpace X] : IsOpen s ↔ ∀ x ∈ s, ∀ (l : Ultrafilter X), ↑l ≤ nhds x → s ∈ l
• continuousAt_iff_ultrafilter 📋 Mathlib.Topology.Ultrafilter
  {X : Type u} {Y : Type v} {x : X} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : ContinuousAt f x ↔ ∀ (g : Ultrafilter X), ↑g ≤ nhds x → Filter.Tendsto f (↑g) (nhds (f x))
• mapClusterPt_iff_ultrafilter 📋 Mathlib.Topology.Ultrafilter
  {X : Type u} {α : Type u_1} {x : X} [TopologicalSpace X] {F : Filter α} {u : α → X} : MapClusterPt x F u ↔ ∃ U, ↑U ≤ F ∧ Filter.Tendsto u (↑U) (nhds x)
• clusterPt_iff_ultrafilter 📋 Mathlib.Topology.Ultrafilter
  {X : Type u} {x : X} [TopologicalSpace X] {f : Filter X} : ClusterPt x f ↔ ∃ u, ↑u ≤ f ∧ ↑u ≤ nhds x
• mem_closure_iff_ultrafilter 📋 Mathlib.Topology.Ultrafilter
  {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] : x ∈ closure s ↔ ∃ u, s ∈ u ∧ ↑u ≤ nhds x
• Ultrafilter.lim 📋 Mathlib.Topology.Defs.Ultrafilter
  {X : Type u_1} [TopologicalSpace X] (F : Ultrafilter X) : X
• Ultrafilter.le_nhds_lim 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] [CompactSpace X] (F : Ultrafilter X) : ↑F ≤ nhds F.lim
• IsCompact.ultrafilter_le_nhds' 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsCompact s → ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ nhds x
• isCompact_iff_ultrafilter_le_nhds' 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsCompact s ↔ ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ nhds x
• IsCompact.ultrafilter_le_nhds 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsCompact s → ∀ (f : Ultrafilter X), ↑f ≤ Filter.principal s → ∃ x ∈ s, ↑f ≤ nhds x
• isCompact_iff_ultrafilter_le_nhds 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsCompact s ↔ ∀ (f : Ultrafilter X), ↑f ≤ Filter.principal s → ∃ x ∈ s, ↑f ≤ nhds x
• Ultrafilter.lim_eq_iff_le_nhds 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] {x : X} {F : Ultrafilter X} : F.lim = x ↔ ↑F ≤ nhds x
• isOpen_iff_ultrafilter' 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] (U : Set X) : IsOpen U ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
• t2_iff_ultrafilter 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] : T2Space X ↔ ∀ {x y : X} (f : Ultrafilter X), ↑f ≤ nhds x → ↑f ≤ nhds y → x = y
• Ultrafilter.cauchy_of_totallyBounded' 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] (f : Ultrafilter α) (hf : (↑f).TotallyBounded) : Cauchy ↑f
• Filter.totallyBounded_iff_ultrafilter 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {g : Filter α} : g.TotallyBounded ↔ ∀ (f : Ultrafilter α), ↑f ≤ g → Cauchy ↑f
• Ultrafilter.cauchy_of_totallyBounded 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (f : Ultrafilter α) (hs : TotallyBounded s) (h : ↑f ≤ Filter.principal s) : Cauchy ↑f
• totallyBounded_iff_ultrafilter 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : TotallyBounded s ↔ ∀ (f : Ultrafilter α), ↑f ≤ Filter.principal s → Cauchy ↑f
• completeSpace_iff_ultrafilter 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] : CompleteSpace α ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ∃ x, ↑l ≤ nhds x
• isComplete_iff_ultrafilter' 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → s ∈ l → ∃ x ∈ s, ↑l ≤ nhds x
• isComplete_iff_ultrafilter 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ Filter.principal s → ∃ x ∈ s, ↑l ≤ nhds x
• IsProperMap.ultrafilter_le_nhds_of_tendsto 📋 Mathlib.Topology.Maps.Proper.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (h : IsProperMap f) ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄ (hy : Filter.Tendsto f (↑𝒰) (nhds y)) : ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x
• isProperMap_iff_ultrafilter_of_t2 📋 Mathlib.Topology.Maps.Proper.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [T2Space Y] : IsProperMap f ↔ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Filter.Tendsto f (↑𝒰) (nhds y) → ∃ x, ↑𝒰 ≤ nhds x
• isProperMap_iff_ultrafilter 📋 Mathlib.Topology.Maps.Proper.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} : IsProperMap f ↔ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Filter.Tendsto f (↑𝒰) (nhds y) → ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x
• properSMul_iff_continuousSMul_ultrafilter_tendsto_t2 📋 Mathlib.Topology.Algebra.ProperAction.Basic
  {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace G] [TopologicalSpace X] [T2Space X] : ProperSMul G X ↔ ContinuousSMul G X ∧ ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X), Filter.Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (nhds (x₁, x₂)) → ∃ g, Filter.Tendsto Prod.fst (↑𝒰) (nhds g)
• properSMul_iff_continuousSMul_ultrafilter_tendsto 📋 Mathlib.Topology.Algebra.ProperAction.Basic
  {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace G] [TopologicalSpace X] : ProperSMul G X ↔ ContinuousSMul G X ∧ ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X), Filter.Tendsto (fun gx => (gx.1 • gx.2, gx.2)) (↑𝒰) (nhds (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Filter.Tendsto Prod.fst (↑𝒰) (nhds g)
• properVAdd_iff_continuousVAdd_ultrafilter_tendsto 📋 Mathlib.Topology.Algebra.ProperAction.Basic
  {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] [TopologicalSpace G] [TopologicalSpace X] : ProperVAdd G X ↔ ContinuousVAdd G X ∧ ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X), Filter.Tendsto (fun gx => (gx.1 +ᵥ gx.2, gx.2)) (↑𝒰) (nhds (x₁, x₂)) → ∃ g, g +ᵥ x₂ = x₁ ∧ Filter.Tendsto Prod.fst (↑𝒰) (nhds g)
• Ultrafilter.topologicalSpace 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} : TopologicalSpace (Ultrafilter α)
• ultrafilterBasis 📋 Mathlib.Topology.Compactification.StoneCech
  (α : Type u) : Set (Set (Ultrafilter α))
• instTotallyDisconnectedSpaceUltrafilter 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} : TotallyDisconnectedSpace (Ultrafilter α)
• ultrafilter_compact 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} : CompactSpace (Ultrafilter α)
• Ultrafilter.t2Space 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} : T2Space (Ultrafilter α)
• ultrafilterBasis_is_basis 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} : TopologicalSpace.IsTopologicalBasis (ultrafilterBasis α)
• Ultrafilter.extend 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} {γ : Type u_1} [TopologicalSpace γ] (f : α → γ) : Ultrafilter α → γ
• denseRange_pure 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} : DenseRange pure
• Ultrafilter.tendsto_pure_self 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} (b : Ultrafilter α) : Filter.Tendsto pure (↑b) (nhds b)
• ultrafilter_isClosed_basic 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} (s : Set α) : IsClosed {u | s ∈ u}
• ultrafilter_isOpen_basic 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} (s : Set α) : IsOpen {u | s ∈ u}
• continuous_ultrafilter_extend 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} {γ : Type u_1} [TopologicalSpace γ] [T2Space γ] [CompactSpace γ] (f : α → γ) : Continuous (Ultrafilter.extend f)
• ultrafilter_extend_pure 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} {γ : Type u_1} [TopologicalSpace γ] [T2Space γ] (f : α → γ) (a : α) : Ultrafilter.extend f (pure a) = f a
• ultrafilter_extend_extends 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} {γ : Type u_1} [TopologicalSpace γ] [T2Space γ] (f : α → γ) : Ultrafilter.extend f ∘ pure = f
• ultrafilter_comap_pure_nhds 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} (b : Ultrafilter α) : Filter.comap pure (nhds b) ≤ ↑b
• ultrafilter_converges_iff 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} {u : Ultrafilter (Ultrafilter α)} {x : Ultrafilter α} : ↑u ≤ nhds x ↔ x = joinM u
• ultrafilter_extend_eq_iff 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} {γ : Type u_1} [TopologicalSpace γ] [T2Space γ] [CompactSpace γ] {f : α → γ} {b : Ultrafilter α} {c : γ} : Ultrafilter.extend f b = c ↔ ↑(Ultrafilter.map f b) ≤ nhds c
• isDenseEmbedding_pure 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} : IsDenseEmbedding pure
• isDenseInducing_pure 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} : IsDenseInducing pure
• induced_topology_pure 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} : TopologicalSpace.induced pure Ultrafilter.topologicalSpace = ⊥
• preStoneCechCompat 📋 Mathlib.Topology.Compactification.StoneCech
  {α : Type u} [TopologicalSpace α] {β : Type v} [TopologicalSpace β] [T2Space β] [CompactSpace β] {g : α → β} (hg : Continuous g) {F G : Ultrafilter α} {x : α} (hF : ↑F ≤ nhds x) (hG : ↑G ≤ nhds x) : Ultrafilter.extend g F = Ultrafilter.extend g G
• OnePoint.ultrafilter_le_nhds_infty 📋 Mathlib.Topology.Compactification.OnePoint.Basic
  {X : Type u_1} [TopologicalSpace X] {f : Ultrafilter (OnePoint X)} : ↑f ≤ nhds OnePoint.infty ↔ ∀ (s : Set X), IsClosed s → IsCompact s → OnePoint.some '' s ∉ f
• Filter.Germ.instDivisionRing 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [DivisionRing β] : DivisionRing ((↑φ).Germ β)
• Filter.Germ.instDivisionSemiring 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [DivisionSemiring β] : DivisionSemiring ((↑φ).Germ β)
• Filter.Germ.instField 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [Field β] : Field ((↑φ).Germ β)
• Filter.Germ.instGroupWithZero 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [GroupWithZero β] : GroupWithZero ((↑φ).Germ β)
• Filter.Germ.instLinearOrder 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrder β] : LinearOrder ((↑φ).Germ β)
• Filter.Germ.instSemifield 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [Semifield β] : Semifield ((↑φ).Germ β)
• Filter.Germ.instIsStrictOrderedRing 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [Semiring β] [PartialOrder β] [IsStrictOrderedRing β] : IsStrictOrderedRing ((↑φ).Germ β)
• Filter.Germ.const_lt 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [Preorder β] {x y : β} : x < y → ↑x < ↑y
• Filter.Germ.total 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [LE β] [Std.Total fun x1 x2 => x1 ≤ x2] : Std.Total fun x1 x2 => x1 ≤ x2
• Filter.Germ.const_lt_iff 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [Preorder β] {x y : β} : ↑x < ↑y ↔ x < y
• Filter.Germ.coe_lt 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [Preorder β] {f g : α → β} : ↑f < ↑g ↔ ∀ᶠ (x : α) in ↑φ, f x < g x
• Filter.Germ.abs_def 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [AddCommGroup β] [LinearOrder β] (x : (↑φ).Germ β) : |x| = Filter.Germ.map abs x
• Filter.Germ.const_abs 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [AddCommGroup β] [LinearOrder β] (x : β) : ↑|x| = |↑x|
• Filter.Germ.const_max 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrder β] (x y : β) : ↑(max x y) = max ↑x ↑y
• Filter.Germ.const_min 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrder β] (x y : β) : ↑(min x y) = min ↑x ↑y
• Filter.Germ.max_def 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrder β] (x y : (↑φ).Germ β) : max x y = Filter.Germ.map₂ max x y
• Filter.Germ.min_def 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [K : LinearOrder β] (x y : (↑φ).Germ β) : min x y = Filter.Germ.map₂ min x y
• Filter.Germ.lt_def 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [Preorder β] : (fun x1 x2 => x1 < x2) = Filter.Germ.LiftRel fun x1 x2 => x1 < x2
• Filter.Germ.coe_pos 📋 Mathlib.Order.Filter.FilterProduct
  {α : Type u} {β : Type v} {φ : Ultrafilter α} [Preorder β] [Zero β] {f : α → β} : 0 < ↑f ↔ ∀ᶠ (x : α) in ↑φ, 0 < f x
• Ultrafilter.add 📋 Mathlib.Combinatorics.Hindman
  {M : Type u_1} [Add M] : Add (Ultrafilter M)
• Ultrafilter.addSemigroup 📋 Mathlib.Combinatorics.Hindman
  {M : Type u_1} [AddSemigroup M] : AddSemigroup (Ultrafilter M)
• Ultrafilter.mul 📋 Mathlib.Combinatorics.Hindman
  {M : Type u_1} [Mul M] : Mul (Ultrafilter M)
• Ultrafilter.semigroup 📋 Mathlib.Combinatorics.Hindman
  {M : Type u_1} [Semigroup M] : Semigroup (Ultrafilter M)
• Ultrafilter.continuous_add_left 📋 Mathlib.Combinatorics.Hindman
  {M : Type u_1} [Add M] (V : Ultrafilter M) : Continuous fun x => x + V
• Ultrafilter.continuous_mul_left 📋 Mathlib.Combinatorics.Hindman
  {M : Type u_1} [Mul M] (V : Ultrafilter M) : Continuous fun x => x * V
• Hindman.exists_idempotent_ultrafilter_le_FP 📋 Mathlib.Combinatorics.Hindman
  {M : Type u_1} [Semigroup M] (a : Stream' M) : ∃ U, U * U = U ∧ ∀ᶠ (m : M) in ↑U, Hindman.FP a m
• Hindman.exists_idempotent_ultrafilter_le_FS 📋 Mathlib.Combinatorics.Hindman
  {M : Type u_1} [AddSemigroup M] (a : Stream' M) : ∃ U, U + U = U ∧ ∀ᶠ (m : M) in ↑U, Hindman.FS a m
• Ultrafilter.eventually_add 📋 Mathlib.Combinatorics.Hindman
  {M : Type u_1} [Add M] (U V : Ultrafilter M) (p : M → Prop) : (∀ᶠ (m : M) in ↑(U + V), p m) ↔ ∀ᶠ (m : M) in ↑U, ∀ᶠ (m' : M) in ↑V, p (m + m')
• Ultrafilter.eventually_mul 📋 Mathlib.Combinatorics.Hindman
  {M : Type u_1} [Mul M] (U V : Ultrafilter M) (p : M → Prop) : (∀ᶠ (m : M) in ↑(U * V), p m) ↔ ∀ᶠ (m : M) in ↑U, ∀ᶠ (m' : M) in ↑V, p (m * m')
• Hindman.exists_FP_of_large 📋 Mathlib.Combinatorics.Hindman
  {M : Type u_1} [Semigroup M] (U : Ultrafilter M) (U_idem : U * U = U) (s₀ : Set M) (sU : s₀ ∈ U) : ∃ a, ∀ (m : M), Hindman.FP a m → m ∈ s₀
• Hindman.exists_FS_of_large 📋 Mathlib.Combinatorics.Hindman
  {M : Type u_1} [AddSemigroup M] (U : Ultrafilter M) (U_idem : U + U = U) (s₀ : Set M) (sU : s₀ ∈ U) : ∃ a, ∀ (m : M), Hindman.FS a m → m ∈ s₀
• CompHaus.projective_ultrafilter 📋 Mathlib.Topology.Category.CompHaus.Projective
  (X : Type u_1) : CategoryTheory.Projective (CompHaus.of (Ultrafilter X))
• FirstOrder.Language.Ultraproduct.Product.instNonempty 📋 Mathlib.ModelTheory.Ultraproducts
  {α : Type u_1} {M : α → Type u_2} {u : Ultrafilter α} [∀ (a : α), Nonempty (M a)] : Nonempty ((↑u).Product M)
• FirstOrder.Language.Ultraproduct.structure 📋 Mathlib.ModelTheory.Ultraproducts
  {α : Type u_1} {M : α → Type u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → L.Structure (M a)] : L.Structure ((↑u).Product M)
• FirstOrder.Language.Ultraproduct.setoidPrestructure 📋 Mathlib.ModelTheory.Ultraproducts
  {α : Type u_1} (M : α → Type u_2) (u : Ultrafilter α) {L : FirstOrder.Language} [(a : α) → L.Structure (M a)] : L.Prestructure ((↑u).productSetoid M)
• FirstOrder.Language.Ultraproduct.sentence_realize 📋 Mathlib.ModelTheory.Ultraproducts
  {α : Type u_1} {M : α → Type u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → L.Structure (M a)] [∀ (a : α), Nonempty (M a)] (φ : L.Sentence) : (↑u).Product M ⊨ φ ↔ ∀ᶠ (a : α) in ↑u, M a ⊨ φ
• FirstOrder.Language.Ultraproduct.realize_formula_cast 📋 Mathlib.ModelTheory.Ultraproducts
  {α : Type u_1} {M : α → Type u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → L.Structure (M a)] [∀ (a : α), Nonempty (M a)] {β : Type u_3} (φ : L.Formula β) (x : β → (a : α) → M a) : (φ.Realize fun i => Quotient.mk' (x i)) ↔ ∀ᶠ (a : α) in ↑u, φ.Realize fun i => x i a
• FirstOrder.Language.Ultraproduct.term_realize_cast 📋 Mathlib.ModelTheory.Ultraproducts
  {α : Type u_1} {M : α → Type u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → L.Structure (M a)] {β : Type u_3} (x : β → (a : α) → M a) (t : L.Term β) : FirstOrder.Language.Term.realize (fun i => Quotient.mk' (x i)) t = Quotient.mk' fun a => FirstOrder.Language.Term.realize (fun i => x i a) t
• FirstOrder.Language.Ultraproduct.funMap_cast 📋 Mathlib.ModelTheory.Ultraproducts
  {α : Type u_1} {M : α → Type u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → L.Structure (M a)] {n : ℕ} (f : L.Functions n) (x : Fin n → (a : α) → M a) : (FirstOrder.Language.Structure.funMap f fun i => Quotient.mk' (x i)) = Quotient.mk' fun a => FirstOrder.Language.Structure.funMap f fun i => x i a
• FirstOrder.Language.Ultraproduct.boundedFormula_realize_cast 📋 Mathlib.ModelTheory.Ultraproducts
  {α : Type u_1} {M : α → Type u_2} {u : Ultrafilter α} {L : FirstOrder.Language} [(a : α) → L.Structure (M a)] [∀ (a : α), Nonempty (M a)] {β : Type u_3} {n : ℕ} (φ : L.BoundedFormula β n) (x : β → (a : α) → M a) (v : Fin n → (a : α) → M a) : (φ.Realize (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' (v i)) ↔ ∀ᶠ (a : α) in ↑u, φ.Realize (fun i => x i a) fun i => v i a
• IsAddFoelner.mean 📋 Mathlib.MeasureTheory.Group.FoelnerFilter
  {X : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {ι : Type u_3} (u : Ultrafilter ι) (F : ι → Set X) (s : Set X) : ENNReal
• IsFoelner.mean 📋 Mathlib.MeasureTheory.Group.FoelnerFilter
  {X : Type u_2} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {ι : Type u_3} (u : Ultrafilter ι) (F : ι → Set X) (s : Set X) : ENNReal
• IsAddFoelner.mean_univ_eq_zero 📋 Mathlib.MeasureTheory.Group.FoelnerFilter
  {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} (hfoel : IsAddFoelner G μ (↑u) F) : IsAddFoelner.mean μ u F Set.univ = 1
• IsFoelner.mean_univ_eq_one 📋 Mathlib.MeasureTheory.Group.FoelnerFilter
  {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [Group G] [MulAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} (hfoel : IsFoelner G μ (↑u) F) : IsFoelner.mean μ u F Set.univ = 1
• IsAddFoelner.tendsto_nhds_mean 📋 Mathlib.MeasureTheory.Group.FoelnerFilter
  {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} (hfoel : IsAddFoelner G μ (↑u) F) (s : Set X) : Filter.Tendsto (fun i => μ (s ∩ F i) / μ (F i)) (↑u) (nhds (IsAddFoelner.mean μ u F s))
• IsFoelner.tendsto_nhds_mean 📋 Mathlib.MeasureTheory.Group.FoelnerFilter
  {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [Group G] [MulAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} (hfoel : IsFoelner G μ (↑u) F) (s : Set X) : Filter.Tendsto (fun i => μ (s ∩ F i) / μ (F i)) (↑u) (nhds (IsFoelner.mean μ u F s))
• IsAddFoelner.mean_vadd_eq_mean 📋 Mathlib.MeasureTheory.Group.FoelnerFilter
  {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} [MeasureTheory.VAddInvariantMeasure G X μ] (hfoel : IsAddFoelner G μ (↑u) F) (g : G) (s : Set X) : IsAddFoelner.mean μ u F (g +ᵥ s) = IsAddFoelner.mean μ u F s
• IsFoelner.mean_smul_eq_mean 📋 Mathlib.MeasureTheory.Group.FoelnerFilter
  {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [Group G] [MulAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} [MeasureTheory.SMulInvariantMeasure G X μ] (hfoel : IsFoelner G μ (↑u) F) (g : G) (s : Set X) : IsFoelner.mean μ u F (g • s) = IsFoelner.mean μ u F s
• IsAddFoelner.mean_union_eq_add_of_disjoint 📋 Mathlib.MeasureTheory.Group.FoelnerFilter
  {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} (hfoel : IsAddFoelner G μ (↑u) F) (s t : Set X) (ht : MeasurableSet t) (hdisj : Disjoint s t) : IsAddFoelner.mean μ u F (s ∪ t) = IsAddFoelner.mean μ u F s + IsAddFoelner.mean μ u F t
• IsFoelner.mean_union_eq_add_of_disjoint 📋 Mathlib.MeasureTheory.Group.FoelnerFilter
  {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [Group G] [MulAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} (hfoel : IsFoelner G μ (↑u) F) (s t : Set X) (ht : MeasurableSet t) (hdisj : Disjoint s t) : IsFoelner.mean μ u F (s ∪ t) = IsFoelner.mean μ u F s + IsFoelner.mean μ u F t
• IsAddFoelner.mean_vadd_eq_mean_vadd 📋 Mathlib.MeasureTheory.Group.FoelnerFilter
  {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} [MeasureTheory.VAddInvariantMeasure G X μ] (hfoel : IsAddFoelner G μ (↑u) F) (g h : G) (s : Set X) : IsAddFoelner.mean μ u F (g +ᵥ s) = IsAddFoelner.mean μ u F (h +ᵥ s)
• IsFoelner.mean_smul_eq_mean_smul 📋 Mathlib.MeasureTheory.Group.FoelnerFilter
  {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [Group G] [MulAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} [MeasureTheory.SMulInvariantMeasure G X μ] (hfoel : IsFoelner G μ (↑u) F) (g h : G) (s : Set X) : IsFoelner.mean μ u F (g • s) = IsFoelner.mean μ u F (h • s)
• IsAddFoelner.tendsto_meas_vadd_symmDiff_vadd 📋 Mathlib.MeasureTheory.Group.FoelnerFilter
  {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [AddGroup G] [AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} [MeasureTheory.VAddInvariantMeasure G X μ] (hfoel : IsAddFoelner G μ (↑u) F) (g h : G) : Filter.Tendsto (fun i => μ (symmDiff (g +ᵥ F i) (h +ᵥ F i)) / μ (F i)) (↑u) (nhds 0)
• IsFoelner.tendsto_meas_smul_symmDiff_smul 📋 Mathlib.MeasureTheory.Group.FoelnerFilter
  {G : Type u_1} {X : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [Group G] [MulAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X} [MeasureTheory.SMulInvariantMeasure G X μ] (hfoel : IsFoelner G μ (↑u) F) (g h : G) : Filter.Tendsto (fun i => μ (symmDiff (g • F i) (h • F i)) / μ (F i)) (↑u) (nhds 0)
• Compactum.instTopologicalSpaceA 📋 Mathlib.Topology.Category.Compactum
  {X : Compactum} : TopologicalSpace X.A
• Compactum.instCompactSpaceA 📋 Mathlib.Topology.Category.Compactum
  {X : Compactum} : CompactSpace X.A
• Compactum.instT2SpaceA 📋 Mathlib.Topology.Category.Compactum
  {X : Compactum} : T2Space X.A

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