Loogle!

Result

Found 498 declarations mentioning uniformity. Of these, only the first 200 are shown.

• uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  (α : Type u) [UniformSpace α] : Filter (α × α)
• uniformity.neBot 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] [Nonempty α] : (uniformity α).NeBot
• tendsto_swap_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] : Filter.Tendsto Prod.swap (uniformity α) (uniformity α)
• UniformSpace.ext 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {u₁ u₂ : UniformSpace α} (h : uniformity α = uniformity α) : u₁ = u₂
• tendsto_const_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {β : Type ub} [UniformSpace α] {a : α} {f : Filter β} : Filter.Tendsto (fun x => (a, a)) f (uniformity α)
• comap_swap_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] : Filter.comap Prod.swap (uniformity α) = uniformity α
• nhds_eq_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {x : α} : nhds x = (uniformity α).lift' (UniformSpace.ball x)
• tendsto_left_nhds_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {a : α} : Filter.Tendsto (fun a' => (a, a')) (nhds a) (uniformity α)
• tendsto_right_nhds_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {a : α} : Filter.Tendsto (fun a' => (a', a)) (nhds a) (uniformity α)
• uniformity_eq_symm 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] : uniformity α = Filter.map Prod.swap (uniformity α)
• isRefl_of_mem_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {s : SetRel α α} (h : s ∈ uniformity α) : s.IsRefl
• nhds_eq_comap_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {x : α} : nhds x = Filter.comap (Prod.mk x) (uniformity α)
• tendsto_diag_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {β : Type ub} [UniformSpace α] (f : β → α) (l : Filter β) : Filter.Tendsto (fun x => (f x, f x)) l (uniformity α)
• nhds_eq_comap_uniformity' 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {x : α} : nhds x = Filter.comap (fun y => (y, x)) (uniformity α)
• lift'_comp_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] : ((uniformity α).lift' fun s => s.comp s) = uniformity α
• refl_le_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] : Filter.principal SetRel.id ≤ uniformity α
• UniformSpace.mem_ball_self 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] (x : α) {V : SetRel α α} : V ∈ uniformity α → x ∈ UniformSpace.ball x V
• nhds_basis_uniformity' 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ι → Prop} {s : ι → SetRel α α} (h : (uniformity α).HasBasis p s) {x : α} : (nhds x).HasBasis p fun i => UniformSpace.ball x (s i)
• subset_comp_self_of_mem_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {s : SetRel α α} (h : s ∈ uniformity α) : s ⊆ s.comp s
• symm_le_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] : Filter.map Prod.swap (uniformity α) ≤ uniformity α
• uniformity_le_symm 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] : uniformity α ≤ Filter.map Prod.swap (uniformity α)
• refl_mem_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {x : α} {s : SetRel α α} (h : s ∈ uniformity α) : (x, x) ∈ s
• symmetrize_mem_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {V : SetRel α α} (h : V ∈ uniformity α) : V.symmetrize ∈ uniformity α
• UniformSpace.ball_mem_nhds 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] (x : α) ⦃V : SetRel α α⦄ (V_in : V ∈ uniformity α) : UniformSpace.ball x V ∈ nhds x
• UniformSpace.closure_subset_image 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {U : SetRel α α} (hU : U ∈ uniformity α) (s : Set α) : closure s ⊆ U.image s
• UniformSpace.closure_subset_preimage 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {U : SetRel α α} (hU : U ∈ uniformity α) (s : Set α) : closure s ⊆ U.preimage s
• UniformSpace.hasBasis_symmetric 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] : (uniformity α).HasBasis (fun s => s ∈ uniformity α ∧ s.IsSymm) id
• UniformSpace.mem_uniformity_ofCore_iff 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {u : UniformSpace.Core α} {s : SetRel α α} : s ∈ uniformity α ↔ s ∈ u.uniformity
• Filter.Tendsto.uniformity_symm 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {β : Type ub} [UniformSpace α] {l : Filter β} {f : β → α × α} (h : Filter.Tendsto f l (uniformity α)) : Filter.Tendsto (fun x => ((f x).2, (f x).1)) l (uniformity α)
• comp_le_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] : ((uniformity α).lift' fun s => s.comp s) ≤ uniformity α
• mem_uniformity_of_eq 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {x y : α} {s : SetRel α α} (h : s ∈ uniformity α) (hx : x = y) : (x, y) ∈ s
• UniformSpace.hasBasis_nhds 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] (x : α) : (nhds x).HasBasis (fun s => s ∈ uniformity α ∧ s.IsSymm) fun s => UniformSpace.ball x s
• nhds_eq_uniformity' 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {x : α} : nhds x = (uniformity α).lift' fun s => {y | (y, x) ∈ s}
• IsUniformInducing.comap_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} (self : IsUniformInducing f) : Filter.comap (fun x => (f x.1, f x.2)) (uniformity β) = uniformity α
• IsUniformInducing.mk 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} (comap_uniformity : Filter.comap (fun x => (f x.1, f x.2)) (uniformity β) = uniformity α) : IsUniformInducing f
• comp_le_uniformity3 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] : ((uniformity α).lift' fun s => s.comp (s.comp s)) ≤ uniformity α
• isUniformInducing_iff 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] (f : α → β) : IsUniformInducing f ↔ Filter.comap (fun x => (f x.1, f x.2)) (uniformity β) = uniformity α
• UniformSpace.ext_iff 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {u₁ u₂ : UniformSpace α} : u₁ = u₂ ↔ ∀ (s : Set (α × α)), s ∈ uniformity α ↔ s ∈ uniformity α
• nhds_basis_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ι → Prop} {s : ι → SetRel α α} (h : (uniformity α).HasBasis p s) {x : α} : (nhds x).HasBasis p fun i => {y | (y, x) ∈ s i}
• UniformSpace.mem_closure_iff_ball 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {s : Set α} {x : α} : x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ uniformity α → (UniformSpace.ball x V ∩ s).Nonempty
• mem_nhds_left 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] (x : α) {s : SetRel α α} (h : s ∈ uniformity α) : {y | (x, y) ∈ s} ∈ nhds x
• mem_nhds_right 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] (y : α) {s : SetRel α α} (h : s ∈ uniformity α) : {x | (x, y) ∈ s} ∈ nhds y
• nhdsWithin_eq_comap_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {x : α} (S : Set α) : nhdsWithin x S = Filter.comap (Prod.mk x) (uniformity α ⊓ Filter.principal (Set.univ ×ˢ S))
• UniformSpace.mem_closure_iff_symm_ball 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {s : Set α} {x : α} : x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ uniformity α → SetRel.IsSymm V → (s ∩ UniformSpace.ball x V).Nonempty
• isOpen_iff_ball_subset 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {s : Set α} : IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ uniformity α, UniformSpace.ball x V ⊆ s
• UniformSpace.mem_nhds_iff 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {x : α} {s : Set α} : s ∈ nhds x ↔ ∃ V ∈ uniformity α, UniformSpace.ball x V ⊆ s
• isOpen_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {s : Set α} : IsOpen s ↔ ∀ x ∈ s, {p | p.1 = x → p.2 ∈ s} ∈ uniformity α
• mem_nhds_uniformity_iff_left 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {x : α} {s : Set α} : s ∈ nhds x ↔ {p | p.2 = x → p.1 ∈ s} ∈ uniformity α
• mem_nhds_uniformity_iff_right 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {x : α} {s : Set α} : s ∈ nhds x ↔ {p | p.1 = x → p.2 ∈ s} ∈ uniformity α
• UniformSpace.mem_nhds_iff_symm 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {x : α} {s : Set α} : s ∈ nhds x ↔ ∃ V ∈ uniformity α, SetRel.IsSymm V ∧ UniformSpace.ball x V ⊆ s
• Filter.Tendsto.uniformity_trans 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {β : Type ub} [UniformSpace α] {l : Filter β} {f₁ f₂ f₃ : β → α} (h₁₂ : Filter.Tendsto (fun x => (f₁ x, f₂ x)) l (uniformity α)) (h₂₃ : Filter.Tendsto (fun x => (f₂ x, f₃ x)) l (uniformity α)) : Filter.Tendsto (fun x => (f₁ x, f₃ x)) l (uniformity α)
• comp_mem_uniformity_sets 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) : ∃ t ∈ uniformity α, SetRel.comp t t ⊆ s
• symm_of_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) : ∃ t ∈ uniformity α, SetRel.IsSymm t ∧ t ⊆ s
• nhdsWithin_eq_comap_uniformity_of_mem 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {x : α} {T : Set α} (hx : x ∈ T) (S : Set α) : nhdsWithin x S = Filter.comap (Prod.mk x) (uniformity α ⊓ Filter.principal (T ×ˢ S))
• comp_symm_mem_uniformity_sets 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) : ∃ t ∈ uniformity α, SetRel.IsSymm t ∧ SetRel.comp t t ⊆ s
• Filter.HasBasis.biInter_biUnion_ball 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ι → Prop} {U : ι → SetRel α α} (h : (uniformity α).HasBasis p U) (s : Set α) : ⋂ i, ⋂ (_ : p i), ⋃ x ∈ s, UniformSpace.ball x (U i) = closure s
• comp3_mem_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) : ∃ t ∈ uniformity α, SetRel.comp t (SetRel.comp t t) ⊆ s
• lift_nhds_left 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {β : Type ub} [UniformSpace α] {x : α} {g : Set α → Filter β} (hg : Monotone g) : (nhds x).lift g = (uniformity α).lift fun s => g (UniformSpace.ball x s)
• uniformContinuous_iff_eventually 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} : UniformContinuous f ↔ ∀ r ∈ uniformity β, ∀ᶠ (x : α × α) in uniformity α, (f x.1, f x.2) ∈ r
• comp_comp_symm_mem_uniformity_sets 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) : ∃ t ∈ uniformity α, SetRel.IsSymm t ∧ (SetRel.comp t t).comp t ⊆ s
• UniformSpace.ball_mem_nhdsWithin 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {x : α} {S : Set α} ⦃V : SetRel α α⦄ (x_in : x ∈ S) (V_in : V ∈ uniformity α ⊓ Filter.principal (S ×ˢ S)) : UniformSpace.ball x V ∈ nhdsWithin x S
• uniformContinuous_def 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} : UniformContinuous f ↔ ∀ r ∈ uniformity β, {x | (f x.1, f x.2) ∈ r} ∈ uniformity α
• exists_mem_nhds_ball_subset_of_mem_nhds 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {a : α} {U : Set α} (h : U ∈ nhds a) : ∃ V ∈ nhds a, ∃ t ∈ uniformity α, ∀ a' ∈ V, UniformSpace.ball a' t ⊆ U
• lift_nhds_right 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {β : Type ub} [UniformSpace α] {x : α} {g : Set α → Filter β} (hg : Monotone g) : (nhds x).lift g = (uniformity α).lift fun s => g {y | (y, x) ∈ s}
• uniformity_lift_le_comp 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {β : Type ub} [UniformSpace α] {f : SetRel α α → Filter β} (h : Monotone f) : ((uniformity α).lift fun s => f (SetRel.comp s s)) ≤ (uniformity α).lift f
• Filter.HasBasis.uniformContinuous_iff 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {β : Type ub} {ι : Sort u_1} [UniformSpace α] [UniformSpace β] {ι' : Sort u_2} {p : ι → Prop} {s : ι → SetRel α α} (ha : (uniformity α).HasBasis p s) {q : ι' → Prop} {t : ι' → Set (β × β)} (hb : (uniformity β).HasBasis q t) {f : α → β} : UniformContinuous f ↔ ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ t i
• comp_symm_of_uniformity 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) : ∃ t ∈ uniformity α, (∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t) ∧ SetRel.comp t t ⊆ s
• uniformity_lift_le_swap 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {β : Type ub} [UniformSpace α] {g : SetRel α α → Filter β} {f : Filter β} (hg : Monotone g) (h : ((uniformity α).lift fun s => g (Prod.swap ⁻¹' s)) ≤ f) : (uniformity α).lift g ≤ f
• nhds_nhds_eq_uniformity_uniformity_prod 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} [UniformSpace α] {a b : α} : nhds a ×ˢ nhds b = (uniformity α).lift fun s => (uniformity α).lift' fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}
• Filter.HasBasis.uniformContinuousOn_iff 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {β : Type ub} {ι : Sort u_1} [UniformSpace α] [UniformSpace β] {ι' : Sort u_2} {p : ι → Prop} {s : ι → SetRel α α} (ha : (uniformity α).HasBasis p s) {q : ι' → Prop} {t : ι' → Set (β × β)} (hb : (uniformity β).HasBasis q t) {f : α → β} {S : Set α} : UniformContinuousOn f S ↔ ∀ (i : ι'), q i → ∃ j, p j ∧ ∀ x ∈ S, ∀ y ∈ S, (x, y) ∈ s j → (f x, f y) ∈ t i
• bot_uniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} : uniformity α = Filter.principal SetRel.id
• discreteTopology_of_discrete_uniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [hα : UniformSpace α] (h : uniformity α = Filter.principal SetRel.id) : DiscreteTopology α
• top_uniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} : uniformity α = ⊤
• UniformSpace.uniformSpace_eq_bot 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {u : UniformSpace α} : u = ⊥ ↔ SetRel.id ∈ uniformity α
• iInf_uniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {ι : Sort u_2} {u : ι → UniformSpace α} : uniformity α = ⨅ i, uniformity α
• inf_uniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {u v : UniformSpace α} : uniformity α = uniformity α ⊓ uniformity α
• uniformity_eq_uniformity_closure 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] : uniformity α = (uniformity α).lift' closure
• uniformity_eq_uniformity_interior 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] : uniformity α = (uniformity α).lift' interior
• uniformity_comap 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} {x✝ : UniformSpace β} (f : α → β) : uniformity α = Filter.comap (Prod.map f f) (uniformity β)
• UniformSpace.has_seq_basis 📋 Mathlib.Topology.UniformSpace.Basic
  (α : Type ua) [UniformSpace α] [(uniformity α).IsCountablyGenerated] : ∃ V, (uniformity α).HasAntitoneBasis V ∧ ∀ (n : ℕ), (V n).IsSymm
• instIsCountablyGeneratedProdElemUniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] [(uniformity α).IsCountablyGenerated] (s : Set α) : (uniformity ↑s).IsCountablyGenerated
• instIsCountablyGeneratedProdSumUniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] [(uniformity α).IsCountablyGenerated] [(uniformity β).IsCountablyGenerated] : (uniformity (α ⊕ β)).IsCountablyGenerated
• instIsCountablyGeneratedProdUniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [(uniformity α).IsCountablyGenerated] [UniformSpace β] [(uniformity β).IsCountablyGenerated] : (uniformity (α × β)).IsCountablyGenerated
• Uniform.tendsto_nhds_left 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] {f : Filter β} {u : β → α} {a : α} : Filter.Tendsto u f (nhds a) ↔ Filter.Tendsto (fun x => (u x, a)) f (uniformity α)
• Uniform.tendsto_nhds_right 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] {f : Filter β} {u : β → α} {a : α} : Filter.Tendsto u f (nhds a) ↔ Filter.Tendsto (fun x => (a, u x)) f (uniformity α)
• Uniform.continuous_iff'_left 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} : Continuous f ↔ ∀ (b : β), Filter.Tendsto (fun x => (f x, f b)) (nhds b) (uniformity α)
• Uniform.continuous_iff'_right 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} : Continuous f ↔ ∀ (b : β), Filter.Tendsto (fun x => (f b, f x)) (nhds b) (uniformity α)
• Uniform.continuousAt_iff'_left 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} {b : β} : ContinuousAt f b ↔ Filter.Tendsto (fun x => (f x, f b)) (nhds b) (uniformity α)
• Uniform.continuousAt_iff'_right 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} {b : β} : ContinuousAt f b ↔ Filter.Tendsto (fun x => (f b, f x)) (nhds b) (uniformity α)
• nhdsSet_diagonal_le_uniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] : nhdsSet (Set.diagonal α) ≤ uniformity α
• Uniform.continuousWithinAt_iff'_left 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} : ContinuousWithinAt f s b ↔ Filter.Tendsto (fun x => (f x, f b)) (nhdsWithin b s) (uniformity α)
• Uniform.continuousWithinAt_iff'_right 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} : ContinuousWithinAt f s b ↔ Filter.Tendsto (fun x => (f b, f x)) (nhdsWithin b s) (uniformity α)
• nhds_le_uniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] (x : α) : nhds (x, x) ≤ uniformity α
• UniformSpace.le_def 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {u₁ u₂ : UniformSpace α} : u₁ ≤ u₂ ↔ uniformity α ≤ uniformity α
• uniformity_hasBasis_closure 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] : (uniformity α).HasBasis (fun V => V ∈ uniformity α) closure
• Filter.HasBasis.uniformity_closure 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ι → Prop} {U : ι → SetRel α α} (h : (uniformity α).HasBasis p U) : (uniformity α).HasBasis p fun i => closure (U i)
• comap_uniformity_addOpposite 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] : Filter.comap (fun p => (AddOpposite.op p.1, AddOpposite.op p.2)) (uniformity αᵃᵒᵖ) = uniformity α
• comap_uniformity_mulOpposite 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] : Filter.comap (fun p => (MulOpposite.op p.1, MulOpposite.op p.2)) (uniformity αᵐᵒᵖ) = uniformity α
• DenseRange.iUnion_uniformity_ball 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] {ι : Type u_2} {xs : ι → α} (xs_dense : DenseRange xs) {U : SetRel α α} (hU : U ∈ uniformity α) : ⋃ i, UniformSpace.ball (xs i) U = Set.univ
• Uniform.continuousOn_iff'_left 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} {s : Set β} : ContinuousOn f s ↔ ∀ b ∈ s, Filter.Tendsto (fun x => (f x, f b)) (nhdsWithin b s) (uniformity α)
• Uniform.continuousOn_iff'_right 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} {s : Set β} : ContinuousOn f s ↔ ∀ b ∈ s, Filter.Tendsto (fun x => (f b, f x)) (nhdsWithin b s) (uniformity α)
• Filter.Tendsto.congr_uniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type u_2} {β : Type u_3} [UniformSpace β] {f g : α → β} {l : Filter α} {b : β} (hf : Filter.Tendsto f l (nhds b)) (hg : Filter.Tendsto (fun x => (f x, g x)) l (uniformity β)) : Filter.Tendsto g l (nhds b)
• eventually_uniformity_comp_subset 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) : ∀ᶠ (t : SetRel α α) in (uniformity α).smallSets, t.comp t ⊆ s
• uniformity_hasBasis_closed 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] : (uniformity α).HasBasis (fun V => V ∈ uniformity α ∧ IsClosed V) id
• uniformity_hasBasis_open 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] : (uniformity α).HasBasis (fun V => V ∈ uniformity α ∧ IsOpen V) id
• Uniform.tendsto_congr 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type u_2} {β : Type u_3} [UniformSpace β] {f g : α → β} {l : Filter α} {b : β} (hfg : Filter.Tendsto (fun x => (f x, g x)) l (uniformity β)) : Filter.Tendsto f l (nhds b) ↔ Filter.Tendsto g l (nhds b)
• interior_mem_uniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) : interior s ∈ uniformity α
• uniformity_addOpposite 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] : uniformity αᵃᵒᵖ = Filter.comap (fun q => (AddOpposite.unop q.1, AddOpposite.unop q.2)) (uniformity α)
• uniformity_mulOpposite 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] : uniformity αᵐᵒᵖ = Filter.comap (fun q => (MulOpposite.unop q.1, MulOpposite.unop q.2)) (uniformity α)
• iSup_nhds_le_uniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] : ⨆ x, nhds (x, x) ≤ uniformity α
• uniformity_hasBasis_open_symmetric 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] : (uniformity α).HasBasis (fun V => V ∈ uniformity α ∧ IsOpen V ∧ V.IsSymm) id
• Uniform.continuousAt_iff_prod 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} {b : β} : ContinuousAt f b ↔ Filter.Tendsto (fun x => (f x.1, f x.2)) (nhds (b, b)) (uniformity α)
• Filter.HasBasis.uniformSpace_eq_bot 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {ι : Sort u_2} {p : ι → Prop} {s : ι → SetRel α α} {u : UniformSpace α} (h : (uniformity α).HasBasis p s) : u = ⊥ ↔ ∃ i, p i ∧ Pairwise fun x y => (x, y) ∉ s i
• eventually_uniformity_iterate_comp_subset 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) (n : ℕ) : ∀ᶠ (t : SetRel α α) in (uniformity α).smallSets, (fun x => t.comp x)^[n] t ⊆ s
• tendsto_prod_uniformity_fst 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : Filter.Tendsto (fun p => (p.1.1, p.2.1)) (uniformity (α × β)) (uniformity α)
• tendsto_prod_uniformity_snd 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : Filter.Tendsto (fun p => (p.1.2, p.2.2)) (uniformity (α × β)) (uniformity β)
• Dense.biUnion_uniformity_ball 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] {s : Set α} {U : SetRel α α} (hs : Dense s) (hU : U ∈ uniformity α) : ⋃ x ∈ s, UniformSpace.ball x U = Set.univ
• uniformity_subtype 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {p : α → Prop} [UniformSpace α] : uniformity (Subtype p) = Filter.comap (fun q => (↑q.1, ↑q.2)) (uniformity α)
• isOpen_iff_isOpen_ball_subset 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] {s : Set α} : IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ uniformity α, IsOpen V ∧ UniformSpace.ball x V ⊆ s
• mem_uniformity_isClosed 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] {s : SetRel α α} (h : s ∈ uniformity α) : ∃ t ∈ uniformity α, IsClosed t ∧ t ⊆ s
• UniformSpace.hasBasis_nhds_prod 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] (x y : α) : (nhds (x, y)).HasBasis (fun s => s ∈ uniformity α ∧ SetRel.IsSymm s) fun s => UniformSpace.ball x s ×ˢ UniformSpace.ball y s
• uniformity_additive 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] : uniformity (Additive α) = Filter.map (Prod.map ⇑Additive.ofMul ⇑Additive.ofMul) (uniformity α)
• uniformity_multiplicative 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] : uniformity (Multiplicative α) = Filter.map (Prod.map ⇑Multiplicative.ofAdd ⇑Multiplicative.ofAdd) (uniformity α)
• entourageProd_mem_uniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [t₁ : UniformSpace α] [t₂ : UniformSpace β] {u : SetRel α α} {v : SetRel β β} (hu : u ∈ uniformity α) (hv : v ∈ uniformity β) : entourageProd u v ∈ uniformity (α × β)
• comp_open_symm_mem_uniformity_sets 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) : ∃ t ∈ uniformity α, IsOpen t ∧ SetRel.IsSymm t ∧ SetRel.comp t t ⊆ s
• Filter.HasBasis.mem_uniformity_iff 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] {p : β → Prop} {s : β → SetRel α α} (h : (uniformity α).HasBasis p s) {t : SetRel α α} : t ∈ uniformity α ↔ ∃ i, p i ∧ ∀ (a b : α), (a, b) ∈ s i → (a, b) ∈ t
• closure_eq_inter_uniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] {t : SetRel α α} : closure t = ⋂ d ∈ uniformity α, SetRel.comp d (t.comp d)
• Filter.HasBasis.uniformity_prod 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} {ιa : Type u_2} {ιb : Type u_3} [UniformSpace α] [UniformSpace β] {pa : ιa → Prop} {pb : ιb → Prop} {sa : ιa → SetRel α α} {sb : ιb → SetRel β β} (ha : (uniformity α).HasBasis pa sa) (hb : (uniformity β).HasBasis pb sb) : (uniformity (α × β)).HasBasis (fun i => pa i.1 ∧ pb i.2) fun i => entourageProd (sa i.1) (sb i.2)
• nhds_eq_uniformity_prod 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] {a b : α} : nhds (a, b) = (uniformity α).lift' fun s => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ s}
• map_uniformity_set_coe 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {s : Set α} [UniformSpace α] : Filter.map (Prod.map Subtype.val Subtype.val) (uniformity ↑s) = uniformity α ⊓ Filter.principal (s ×ˢ s)
• Sum.uniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : uniformity (α ⊕ β) = Filter.map (Prod.map Sum.inl Sum.inl) (uniformity α) ⊔ Filter.map (Prod.map Sum.inr Sum.inr) (uniformity β)
• uniformity_setCoe 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {s : Set α} [UniformSpace α] : uniformity ↑s = Filter.comap (Prod.map Subtype.val Subtype.val) (uniformity α)
• Uniform.exists_is_open_mem_uniformity_of_forall_mem_eq 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {r : SetRel α α} {s : Set β} {f g : β → α} (hf : ∀ x ∈ s, ContinuousAt f x) (hg : ∀ x ∈ s, ContinuousAt g x) (hfg : Set.EqOn f g s) (hr : r ∈ uniformity α) : ∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r
• mem_uniformity_of_uniformContinuous_invariant 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {s : SetRel β β} {f : α → α → β} (hf : UniformContinuous fun p => f p.1 p.2) (hs : s ∈ uniformity β) : ∃ u ∈ uniformity α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
• entourageProd_subset 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {s : Set ((α × β) × α × β)} (h : s ∈ uniformity (α × β)) : ∃ u ∈ uniformity α, ∃ v ∈ uniformity β, entourageProd u v ⊆ s
• uniformity_prod 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : uniformity (α × β) = Filter.comap (fun p => (p.1.1, p.2.1)) (uniformity α) ⊓ Filter.comap (fun p => (p.1.2, p.2.2)) (uniformity β)
• uniformity_prod_eq_comap_prod 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : uniformity (α × β) = Filter.comap (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (uniformity α ×ˢ uniformity β)
• uniformity_prod_eq_prod 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : uniformity (α × β) = Filter.map (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (uniformity α ×ˢ uniformity β)
• nhdset_of_mem_uniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] {d : SetRel α α} (s : SetRel α α) (hd : d ∈ uniformity α) : ∃ t, IsOpen t ∧ s ⊆ t ∧ t ⊆ {p | ∃ x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
• closure_eq_uniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] (s : Set (α × α)) : closure s = ⋂ V ∈ {V | V ∈ uniformity α ∧ SetRel.IsSymm V}, (SetRel.comp V s).comp V
• union_mem_uniformity_sum 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {a : SetRel α α} (ha : a ∈ uniformity α) {b : SetRel β β} (hb : b ∈ uniformity β) : Prod.map Sum.inl Sum.inl '' a ∪ Prod.map Sum.inr Sum.inr '' b ∈ uniformity (α ⊕ β)
• DiscreteUniformity.eq_principal_setRelId 📋 Mathlib.Topology.UniformSpace.DiscreteUniformity
  (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] : uniformity X = Filter.principal SetRel.id
• discreteUniformity_iff_eq_principal_setRelId 📋 Mathlib.Topology.UniformSpace.DiscreteUniformity
  {X : Type u_2} [UniformSpace X] : DiscreteUniformity X ↔ uniformity X = Filter.principal SetRel.id
• DiscreteUniformity.relId_mem_uniformity 📋 Mathlib.Topology.UniformSpace.DiscreteUniformity
  (X : Type u_1) [u : UniformSpace X] [DiscreteUniformity X] : SetRel.id ∈ uniformity X
• discreteUniformity_iff_setRelId_mem_uniformity 📋 Mathlib.Topology.UniformSpace.DiscreteUniformity
  {X : Type u_2} [UniformSpace X] : DiscreteUniformity X ↔ SetRel.id ∈ uniformity X
• UniformSpace.firstCountableTopology 📋 Mathlib.Topology.UniformSpace.Cauchy
  (α : Type u) [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] : FirstCountableTopology α
• UniformSpace.secondCountable_of_separable 📋 Mathlib.Topology.UniformSpace.Cauchy
  (α : Type u) [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] [TopologicalSpace.SeparableSpace α] : SecondCountableTopology α
• TotallyBounded.isSeparable 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] {s : Set α} (h : TotallyBounded s) : TopologicalSpace.IsSeparable s
• totallyBounded_interUnionBalls 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {p : ℕ → Prop} {U : ℕ → SetRel α α} (H : (uniformity α).HasBasis p U) (xs : ℕ → α) (u : ℕ → ℕ) : TotallyBounded (interUnionBalls xs u U)
• SequentiallyComplete.seq 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) : α
• SequentiallyComplete.setSeq 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) : Set α
• UniformSpace.complete_of_cauchySeq_tendsto 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] (H' : ∀ (u : ℕ → α), CauchySeq u → ∃ a, Filter.Tendsto u Filter.atTop (nhds a)) : CompleteSpace α
• CauchySeq.tendsto_uniformity 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] {u : β → α} (h : CauchySeq u) : Filter.Tendsto (Prod.map u u) Filter.atTop (uniformity α)
• isCompact_closure_interUnionBalls 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {p : ℕ → Prop} {U : ℕ → SetRel α α} (H : (uniformity α).HasBasis p U) [CompleteSpace α] (xs : ℕ → α) (u : ℕ → ℕ) : IsCompact (closure (interUnionBalls xs u U))
• SequentiallyComplete.setSeq_mem 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) : SequentiallyComplete.setSeq hf U_mem n ∈ f
• cauchy_iff_le 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {l : Filter α} [hl : l.NeBot] : Cauchy l ↔ l ×ˢ l ≤ uniformity α
• Filter.HasBasis.filter_totallyBounded_iff 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {U : ι → SetRel α α} (H : (uniformity α).HasBasis p U) {f : Filter α} : f.TotallyBounded ↔ ∀ (i : ι), p i → ∃ t, t.Finite ∧ (U i).preimage t ∈ f
• SequentiallyComplete.seq_mem 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) : SequentiallyComplete.seq hf U_mem n ∈ SequentiallyComplete.setSeq hf U_mem n
• cauchySeq_iff_tendsto 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} : CauchySeq u ↔ Filter.Tendsto (Prod.map u u) Filter.atTop (uniformity α)
• Cauchy.ultrafilter_of 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {l : Filter α} (h : Cauchy l) : Cauchy ↑(Ultrafilter.of l)
• SequentiallyComplete.setSeq_mono 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) ⦃m n : ℕ⦄ (h : m ≤ n) : SequentiallyComplete.setSeq hf U_mem n ⊆ SequentiallyComplete.setSeq hf U_mem m
• cauchy_map_iff' 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {l : Filter β} [hl : l.NeBot] {f : β → α} : Cauchy (Filter.map f l) ↔ Filter.Tendsto (fun p => (f p.1, f p.2)) (l ×ˢ l) (uniformity α)
• cauchy_map_iff 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {l : Filter β} {f : β → α} : Cauchy (Filter.map f l) ↔ l.NeBot ∧ Filter.Tendsto (fun p => (f p.1, f p.2)) (l ×ˢ l) (uniformity α)
• CauchySeq.eventually_eventually 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] {u : β → α} (hu : CauchySeq u) {V : SetRel α α} (hV : V ∈ uniformity α) : ∀ᶠ (k : β) (l : β) in Filter.atTop, (u k, u l) ∈ V
• cauchySeq_iff 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {u : ℕ → α} : CauchySeq u ↔ ∀ V ∈ uniformity α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
• Filter.TotallyBounded.exists_subset_of_mem 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : f.TotallyBounded) {s : Set α} (hs : s ∈ f) {U : SetRel α α} (hU : U ∈ uniformity α) : ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f
• SequentiallyComplete.setSeqAux 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) : { s // s ∈ f ∧ s ×ˢ s ⊆ U n }
• cauchy_iff 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} : Cauchy f ↔ f.NeBot ∧ ∀ s ∈ uniformity α, ∃ t ∈ f, t ×ˢ t ⊆ s
• totallyBounded_of_forall_isSymm 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (h : ∀ V ∈ uniformity α, SetRel.IsSymm V → ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, UniformSpace.ball y V) : TotallyBounded s
• SequentiallyComplete.seq_pair_mem 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) ⦃N m n : ℕ⦄ (hm : N ≤ m) (hn : N ≤ n) : (SequentiallyComplete.seq hf U_mem m, SequentiallyComplete.seq hf U_mem n) ∈ U N
• UniformSpace.secondCountable_of_almost_dense_set 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] (hs : ∀ U ∈ uniformity α, ∃ t, t.Countable ∧ ⋃ x ∈ t, UniformSpace.ball x U = Set.univ) : SecondCountableTopology α
• Filter.HasBasis.cauchySeq_iff' 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Sort u_1} [Nonempty β] [SemilatticeSup β] {u : β → α} {p : γ → Prop} {s : γ → SetRel α α} (H : (uniformity α).HasBasis p s) : CauchySeq u ↔ ∀ (i : γ), p i → ∃ N, ∀ n ≥ N, (u n, u N) ∈ s i
• cauchySeq_iff' 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {u : ℕ → α} : CauchySeq u ↔ ∀ V ∈ uniformity α, ∀ᶠ (k : ℕ × ℕ) in Filter.atTop, k ∈ Prod.map u u ⁻¹' V
• Cauchy.comap 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : Filter β} {m : α → β} (hf : Cauchy f) (hm : Filter.comap (fun p => (m p.1, m p.2)) (uniformity β) ≤ uniformity α) [(Filter.comap m f).NeBot] : Cauchy (Filter.comap m f)
• Cauchy.comap' 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [UniformSpace β] {f : Filter β} {m : α → β} (hf : Cauchy f) (hm : Filter.comap (fun p => (m p.1, m p.2)) (uniformity β) ≤ uniformity α) : (Filter.comap m f).NeBot → Cauchy (Filter.comap m f)
• SequentiallyComplete.seq_is_cauchySeq 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (U_le : ∀ s ∈ uniformity α, ∃ n, U n ⊆ s) : CauchySeq (SequentiallyComplete.seq hf U_mem)
• Cauchy.le_nhds_lim 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {f : Filter α} (hf : Cauchy f) : f ≤ nhds f.lim
• CauchySeq.subseq_mem 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {V : ℕ → SetRel α α} (hV : ∀ (n : ℕ), V n ∈ uniformity α) {u : ℕ → α} (hu : CauchySeq u) : ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V n
• CauchySeq.mem_entourage 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {β : Type u_1} [SemilatticeSup β] {u : β → α} (h : CauchySeq u) {V : SetRel α α} (hV : V ∈ uniformity α) : ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V
• SequentiallyComplete.setSeq_prod_subset 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) {N m n : ℕ} (hm : N ≤ m) (hn : N ≤ n) : SequentiallyComplete.setSeq hf U_mem m ×ˢ SequentiallyComplete.setSeq hf U_mem n ⊆ U N
• isComplete_iUnion_separated 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {s : ι → Set α} (hs : ∀ (i : ι), IsComplete (s i)) {U : SetRel α α} (hU : U ∈ uniformity α) (hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j) : IsComplete (⋃ i, s i)
• Filter.HasBasis.cauchy_iff 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {s : ι → SetRel α α} (h : (uniformity α).HasBasis p s) {f : Filter α} : Cauchy f ↔ f.NeBot ∧ ∀ (i : ι), p i → ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s i
• cauchy_iff' 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} : Cauchy f ↔ f.NeBot ∧ ∀ s ∈ uniformity α, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s
• UniformSpace.complete_of_convergent_controlled_sequences 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] (U : ℕ → SetRel α α) (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Filter.Tendsto u Filter.atTop (nhds a)) : CompleteSpace α
• Filter.HasBasis.cauchySeq_iff 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Sort u_1} [Nonempty β] [SemilatticeSup β] {u : β → α} {p : γ → Prop} {s : γ → SetRel α α} (h : (uniformity α).HasBasis p s) : CauchySeq u ↔ ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
• Filter.HasBasis.totallyBounded_iff 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {U : ι → SetRel α α} (H : (uniformity α).HasBasis p U) {s : Set α} : TotallyBounded s ↔ ∀ (i : ι), p i → ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}
• SequentiallyComplete.setSeq_sub_aux 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ) : SequentiallyComplete.setSeq hf U_mem n ⊆ ↑(SequentiallyComplete.setSeqAux hf U_mem n)
• TotallyBounded.exists_subset 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} (hs : TotallyBounded s) {U : SetRel α α} (hU : U ∈ uniformity α) : ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}
• totallyBounded_iff_subset 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {s : Set α} : TotallyBounded s ↔ ∀ d ∈ uniformity α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
• UniformSpace.subset_countable_closure_of_almost_dense_set 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] [(uniformity α).IsCountablyGenerated] (s : Set α) (hs : ∀ U ∈ uniformity α, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U) : ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
• cauchySeq_of_controlled 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [SemilatticeSup β] [Nonempty β] (U : β → SetRel α α) (hU : ∀ s ∈ uniformity α, ∃ n, U n ⊆ s) {f : β → α} (hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N) : CauchySeq f
• SequentiallyComplete.le_nhds_of_seq_tendsto_nhds 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α} (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (U_le : ∀ s ∈ uniformity α, ∃ n, U n ⊆ s) ⦃a : α⦄ (ha : Filter.Tendsto (SequentiallyComplete.seq hf U_mem) Filter.atTop (nhds a)) : f ≤ nhds a
• CauchySeq.tendsto_limUnder 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] [CompleteSpace α] {u : β → α} (h : CauchySeq u) : Filter.Tendsto u Filter.atTop (nhds (Filter.atTop.limUnder u))
• CauchySeq.subseq_subseq_mem 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {V : ℕ → SetRel α α} (hV : ∀ (n : ℕ), V n ∈ uniformity α) {u : ℕ → α} (hu : CauchySeq u) {f g : ℕ → ℕ} (hf : Filter.Tendsto f Filter.atTop Filter.atTop) (hg : Filter.Tendsto g Filter.atTop Filter.atTop) : ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n
• le_nhds_of_cauchy_adhp_aux 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} {x : α} (adhs : ∀ s ∈ uniformity α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t) : f ≤ nhds x
• Filter.Tendsto.subseq_mem_entourage 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {V : ℕ → SetRel α α} (hV : ∀ (n : ℕ), V n ∈ uniformity α) {u : ℕ → α} {a : α} (hu : Filter.Tendsto u Filter.atTop (nhds a)) : ∃ φ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)
• tendstoUniformlyOnFilter_iff_tendsto 📋 Mathlib.Topology.UniformSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} : TendstoUniformlyOnFilter F f p p' ↔ Filter.Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ p') (uniformity β)
• tendstoUniformly_iff_tendsto 📋 Mathlib.Topology.UniformSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} : TendstoUniformly F f p ↔ Filter.Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ ⊤) (uniformity β)
• Filter.HasBasis.tendstoUniformly_iff_of_uniformity 📋 Mathlib.Topology.UniformSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} [UniformSpace β] {X : Type u_5} {ιβ : Type u_8} {F : X → α → β} {f : α → β} {l : Filter X} {pβ : ιβ → Prop} {sβ : ιβ → Set (β × β)} (hβ : (uniformity β).HasBasis pβ sβ) : TendstoUniformly F f l ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i
• tendstoUniformlyOn_iff_tendsto 📋 Mathlib.Topology.UniformSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} : TendstoUniformlyOn F f p s ↔ Filter.Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ Filter.principal s) (uniformity β)

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