Loogle!

Result

Found 1776 declarations mentioning PseudoMetricSpace. Of these, only the first 200 are shown.

• PseudoMetricSpace 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  (α : Type u) : Type u
• Real.pseudoMetricSpace 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  : PseudoMetricSpace ℝ
• PseudoMetricSpace.toBornology 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [self : PseudoMetricSpace α] : Bornology α
• PseudoMetricSpace.toDist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [self : PseudoMetricSpace α] : Dist α
• PseudoMetricSpace.toEDist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : EDist α
• PseudoMetricSpace.toNNDist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : NNDist α
• PseudoMetricSpace.toPseudoEMetricSpace 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : PseudoEMetricSpace α
• PseudoMetricSpace.toUniformSpace 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [self : PseudoMetricSpace α] : UniformSpace α
• instPseudoMetricSpaceAdditive 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : PseudoMetricSpace (Additive α)
• instPseudoMetricSpaceMultiplicative 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : PseudoMetricSpace (Multiplicative α)
• instPseudoMetricSpaceOrderDual 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : PseudoMetricSpace αᵒᵈ
• PseudoMetricSpace.edist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [self : PseudoMetricSpace α] : α → α → ENNReal
• Metric.ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α
• Metric.closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α
• Metric.sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α
• PseudoMetricSpace.replaceTopology 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {γ : Type u_3} [U : TopologicalSpace γ] (m : PseudoMetricSpace γ) (H : U = PseudoMetricSpace.toUniformSpace.toTopologicalSpace) : PseudoMetricSpace γ
• edist_ne_top 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y : α) : edist x y ≠ ⊤
• Metric.isOpen_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : IsOpen (Metric.ball x ε)
• dist_self 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) : dist x x = 0
• nndist_self 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (a : α) : nndist a a = 0
• Metric.sphere_isEmpty_of_subsingleton 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α] [NeZero ε] : IsEmpty ↑(Metric.sphere x ε)
• PseudoMetricSpace.dist_self 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [self : PseudoMetricSpace α] (x : α) : dist x x = 0
• PseudoMetricSpace.ext 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u_3} {m m' : PseudoMetricSpace α} (h : m.toDist = m'.toDist) : m = m'
• Metric.ball_subset_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.ball x ε ⊆ Metric.closedBall x ε
• Metric.sphere_subset_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.sphere x ε ⊆ Metric.closedBall x ε
• PseudoMetricSpace.edist_dist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [self : PseudoMetricSpace α] (x y : α) : PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
• PseudoMetricSpace.ext_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u_3} {m m' : PseudoMetricSpace α} : m = m' ↔ m.toDist = m'.toDist
• PseudoMetricSpace.replaceBornology 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u_3} [B : Bornology α] (m : PseudoMetricSpace α) (H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s) : PseudoMetricSpace α
• dist_comm 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y : α) : dist x y = dist y x
• dist_nonneg 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} : 0 ≤ dist x y
• nndist_comm 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y : α) : nndist x y = nndist y x
• Metric.iUnion_ball_nat 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) : ⋃ n, Metric.ball x ↑n = Set.univ
• Metric.iUnion_closedBall_nat 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) : ⋃ n, Metric.closedBall x ↑n = Set.univ
• PseudoMetricSpace.dist_comm 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [self : PseudoMetricSpace α] (x y : α) : dist x y = dist y x
• coe_nndist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y : α) : ↑(nndist x y) = dist x y
• coe_nnreal_ennreal_nndist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y : α) : ↑(nndist x y) = edist x y
• dist_edist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y : α) : dist x y = (edist x y).toReal
• dist_nndist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y : α) : dist x y = ↑(nndist x y)
• edist_dist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y : α) : edist x y = ENNReal.ofReal (dist x y)
• edist_lt_top 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u_3} [PseudoMetricSpace α] (x y : α) : edist x y < ⊤
• edist_nndist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y : α) : edist x y = ↑(nndist x y)
• nndist_dist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y : α) : nndist x y = (dist x y).toNNReal
• nndist_edist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y : α) : nndist x y = (edist x y).toNNReal
• Metric.ball_zero 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} : Metric.ball x 0 = ∅
• PseudoMetricSpace.replaceUniformity 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u_3} [U : UniformSpace α] (m : PseudoMetricSpace α) (H : uniformity α = uniformity α) : PseudoMetricSpace α
• swap_dist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : Function.swap dist = dist
• Metric.nonempty_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : (Metric.ball x ε).Nonempty ↔ 0 < ε
• Metric.nonempty_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : (Metric.closedBall x ε).Nonempty ↔ 0 ≤ ε
• PseudoMetricSpace.replaceTopology_eq 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {γ : Type u_3} [U : TopologicalSpace γ] (m : PseudoMetricSpace γ) (H : U = PseudoMetricSpace.toUniformSpace.toTopologicalSpace) : m.replaceTopology H = m
• abs_dist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {a b : α} : |dist a b| = dist a b
• Metric.boundedSpace_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : BoundedSpace α ↔ ∃ C, ∀ (a b : α), dist a b ≤ C
• Metric.toUniformSpace_eq 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : PseudoMetricSpace.toUniformSpace = UniformSpace.ofDist dist ⋯ ⋯ ⋯
• Metric.ball_subset_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε₁ ε₂ : ℝ} (h : ε₁ ≤ ε₂) : Metric.ball x ε₁ ⊆ Metric.ball x ε₂
• Metric.boundedSpace_iff_edist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : BoundedSpace α ↔ ∃ C, ∀ (a b : α), edist a b ≤ ↑C
• Metric.closedBall_subset_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε₁ ε₂ : ℝ} (h : ε₁ < ε₂) : Metric.closedBall x ε₁ ⊆ Metric.ball x ε₂
• Metric.closedBall_subset_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε₁ ε₂ : ℝ} (h : ε₁ ≤ ε₂) : Metric.closedBall x ε₁ ⊆ Metric.closedBall x ε₂
• Metric.sphere_subset_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {r R : ℝ} (h : r < R) : Metric.sphere x r ⊆ Metric.ball x R
• PseudoEMetricSpace.toPseudoMetricSpace 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoEMetricSpace α] (h : ∀ (x y : α), edist x y ≠ ⊤) : PseudoMetricSpace α
• Metric.ball_subset_interior_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.ball x ε ⊆ interior (Metric.closedBall x ε)
• Metric.mem_ball_self 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (h : 0 < ε) : x ∈ Metric.ball x ε
• Metric.mem_closedBall_self 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (h : 0 ≤ ε) : x ∈ Metric.closedBall x ε
• PseudoMetricSpace.replaceBornology_eq 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u_3} [m : PseudoMetricSpace α] [B : Bornology α] (H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s) : m.replaceBornology H = m
• Metric.ball_union_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.ball x ε ∪ Metric.sphere x ε = Metric.closedBall x ε
• Metric.closedBall_diff_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.closedBall x ε \ Metric.ball x ε = Metric.sphere x ε
• Metric.closedBall_diff_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.closedBall x ε \ Metric.sphere x ε = Metric.ball x ε
• Metric.closedBall_eq_sphere_of_nonpos 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (hε : ε ≤ 0) : Metric.closedBall x ε = Metric.sphere x ε
• Metric.closedBall_of_neg 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : ε < 0 → Metric.closedBall x ε = ∅
• Metric.closedBall_sdiff_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.closedBall x ε \ Metric.ball x ε = Metric.sphere x ε
• Metric.closedBall_sdiff_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.closedBall x ε \ Metric.sphere x ε = Metric.ball x ε
• Metric.iUnion_inter_closedBall_nat 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (s : Set α) (x : α) : ⋃ n, s ∩ Metric.closedBall x ↑n = s
• Metric.nonneg_of_mem_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} (hy : y ∈ Metric.closedBall x ε) : 0 ≤ ε
• Metric.nonneg_of_mem_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} (hy : y ∈ Metric.sphere x ε) : 0 ≤ ε
• Metric.pos_of_mem_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} (hy : y ∈ Metric.ball x ε) : 0 < ε
• Metric.sphere_eq_empty_of_neg 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (hε : ε < 0) : Metric.sphere x ε = ∅
• Metric.sphere_union_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.sphere x ε ∪ Metric.ball x ε = Metric.closedBall x ε
• Metric.ball_eq_empty 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.ball x ε = ∅ ↔ ε ≤ 0
• Metric.boundedSpace_iff_nndist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : BoundedSpace α ↔ ∃ C, ∀ (a b : α), nndist a b ≤ C
• Metric.closedBall_eq_empty 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.closedBall x ε = ∅ ↔ ε < 0
• Metric.eball_top 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) : Metric.eball x ⊤ = Set.univ
• Metric.eball_top_eq_univ 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) : Metric.eball x ⊤ = Set.univ
• Metric.mem_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : y ∈ Metric.sphere x ε ↔ dist y x = ε
• Metric.mem_sphere' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : y ∈ Metric.sphere x ε ↔ dist x y = ε
• Metric.sphere_eq_empty_of_subsingleton 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α] (hε : ε ≠ 0) : Metric.sphere x ε = ∅
• PseudoMetricSpace.replaceUniformity_eq 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u_3} [U : UniformSpace α] (m : PseudoMetricSpace α) (H : uniformity α = uniformity α) : m.replaceUniformity H = m
• Metric.forall_of_forall_mem_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (p : α → Prop) (x : α) (H : ∃ᶠ (R : ℝ) in Filter.atTop, ∀ y ∈ Metric.ball x R, p y) (y : α) : p y
• Metric.forall_of_forall_mem_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (p : α → Prop) (x : α) (H : ∃ᶠ (R : ℝ) in Filter.atTop, ∀ y ∈ Metric.closedBall x R, p y) (y : α) : p y
• Metric.mem_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : y ∈ Metric.ball x ε ↔ dist y x < ε
• Metric.mem_ball' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : y ∈ Metric.ball x ε ↔ dist x y < ε
• Metric.mem_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : y ∈ Metric.closedBall x ε ↔ dist y x ≤ ε
• Metric.mem_closedBall' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : y ∈ Metric.closedBall x ε ↔ dist x y ≤ ε
• Metric.nhds_basis_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} : (nhds x).HasBasis (fun x => 0 < x) (Metric.ball x)
• Metric.nhds_basis_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} : (nhds x).HasBasis (fun ε => 0 < ε) (Metric.closedBall x)
• Metric.mem_ball_comm 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : x ∈ Metric.ball y ε ↔ y ∈ Metric.ball x ε
• Metric.mem_closedBall_comm 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : x ∈ Metric.closedBall y ε ↔ y ∈ Metric.closedBall x ε
• Metric.mem_sphere_comm 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} : x ∈ Metric.sphere y ε ↔ y ∈ Metric.sphere x ε
• Metric.ne_of_mem_sphere 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} (h : y ∈ Metric.sphere x ε) (hε : ε ≠ 0) : y ≠ x
• Metric.ball_eq_singleton_of_subsingleton 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α] (h : 0 < ε) : Metric.ball x ε = {x}
• Metric.closedBall_eq_singleton_of_subsingleton 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α] (h : 0 ≤ ε) : Metric.closedBall x ε = {x}
• Metric.eball_ofReal 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.eball x (ENNReal.ofReal ε) = Metric.ball x ε
• Metric.closedEBall_coe 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : NNReal} : Metric.closedEBall x ↑ε = Metric.closedBall x ↑ε
• Metric.eball_coe 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : NNReal} : Metric.eball x ↑ε = Metric.ball x ↑ε
• dist_le_coe 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {c : NNReal} : dist x y ≤ ↑c ↔ nndist x y ≤ c
• dist_lt_coe 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {c : NNReal} : dist x y < ↑c ↔ nndist x y < c
• edist_le_coe 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {c : NNReal} : edist x y ≤ ↑c ↔ nndist x y ≤ c
• edist_lt_ofReal 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {r : ℝ} : edist x y < ENNReal.ofReal r ↔ dist x y < r
• Metric.closedBall_eq_bInter_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.closedBall x ε = ⋂ δ, ⋂ (_ : δ > ε), Metric.ball x δ
• Metric.iUnion_ball_nat_succ 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) : ⋃ n, Metric.ball x (↑n + 1) = Set.univ
• dist_dist_dist_le_left 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y z : α) : dist (dist x z) (dist y z) ≤ dist x y
• dist_dist_dist_le_right 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y z : α) : dist (dist x y) (dist x z) ≤ dist y z
• Metric.ball_mem_nhds 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) {ε : ℝ} (ε0 : 0 < ε) : Metric.ball x ε ∈ nhds x
• Metric.closedBall_mem_nhds 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) {ε : ℝ} (ε0 : 0 < ε) : Metric.closedBall x ε ∈ nhds x
• DiscreteTopology.of_forall_le_dist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u_3} [PseudoMetricSpace α] {r : ℝ} (hpos : 0 < r) (hr : Pairwise fun x1 x2 => r ≤ dist x1 x2) : DiscreteTopology α
• dist_triangle 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y z : α) : dist x z ≤ dist x y + dist y z
• dist_triangle_left 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y z : α) : dist x y ≤ dist z x + dist z y
• dist_triangle_right 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y z : α) : dist x y ≤ dist x z + dist y z
• PseudoMetricSpace.dist_eq_of_dist_zero 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x : α) {y z : α} (h : dist y z = 0) : dist x y = dist x z
• PseudoMetricSpace.dist_triangle 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [self : PseudoMetricSpace α] (x y z : α) : dist x z ≤ dist x y + dist y z
• edist_lt_coe 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {c : NNReal} : edist x y < ↑c ↔ nndist x y < c
• Metric.closedBall_mem_nhds_of_mem 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x c : α} {ε : ℝ} (h : x ∈ Metric.ball c ε) : Metric.closedBall c ε ∈ nhds x
• nhds_comap_dist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (a : α) : Filter.comap (fun x => dist x a) (nhds 0) = nhds a
• Metric.dense_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {s : Set α} : Dense s ↔ ∀ (x : α), ∀ r > 0, (Metric.ball x r ∩ s).Nonempty
• Metric.exists_lt_mem_ball_of_mem_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} (h : x ∈ Metric.ball y ε) : ∃ ε' < ε, x ∈ Metric.ball y ε'
• edist_le_ofReal 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {r : ℝ} (hr : 0 ≤ r) : edist x y ≤ ENNReal.ofReal r ↔ dist x y ≤ r
• Metric.ball_eq_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (ε : ℝ) (x : α) : UniformSpace.ball x {p | dist p.2 p.1 < ε} = Metric.ball x ε
• Metric.ball_eq_ball' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (ε : ℝ) (x : α) : UniformSpace.ball x {p | dist p.1 p.2 < ε} = Metric.ball x ε
• abs_dist_sub_le 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y z : α) : |dist x z - dist y z| ≤ dist x y
• Metric.ball_subset 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : dist x y ≤ ε₂ - ε₁) : Metric.ball x ε₁ ⊆ Metric.ball y ε₂
• Metric.ball_subset_ball' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : ε₁ + dist x y ≤ ε₂) : Metric.ball x ε₁ ⊆ Metric.ball y ε₂
• Metric.closedBall_subset_ball' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : ε₁ + dist x y < ε₂) : Metric.closedBall x ε₁ ⊆ Metric.ball y ε₂
• Metric.closedBall_subset_closedBall' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : ε₁ + dist x y ≤ ε₂) : Metric.closedBall x ε₁ ⊆ Metric.closedBall y ε₂
• Metric.nhdsWithin_basis_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {s : Set α} : (nhdsWithin x s).HasBasis (fun ε => 0 < ε) fun ε => Metric.ball x ε ∩ s
• DenseRange.exists_dist_lt 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {β : Type u_3} {f : β → α} (hf : DenseRange f) (x : α) {ε : ℝ} (hε : 0 < ε) : ∃ y, dist x (f y) < ε
• Metric.closedEBall_ofReal 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (h : 0 ≤ ε) : Metric.closedEBall x (ENNReal.ofReal ε) = Metric.closedBall x ε
• Metric.denseRange_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} : DenseRange f ↔ ∀ (x : α), ∀ r > 0, ∃ y, dist x (f y) < r
• Metric.dist_le_add_of_nonempty_closedBall_inter_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : (Metric.closedBall x ε₁ ∩ Metric.closedBall y ε₂).Nonempty) : dist x y ≤ ε₁ + ε₂
• Metric.dist_lt_add_of_nonempty_ball_inter_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : (Metric.ball x ε₁ ∩ Metric.ball y ε₂).Nonempty) : dist x y < ε₁ + ε₂
• Metric.dist_lt_add_of_nonempty_ball_inter_closedBall 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : (Metric.ball x ε₁ ∩ Metric.closedBall y ε₂).Nonempty) : dist x y < ε₁ + ε₂
• Metric.dist_lt_add_of_nonempty_closedBall_inter_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : (Metric.closedBall x ε₁ ∩ Metric.ball y ε₂).Nonempty) : dist x y < ε₁ + ε₂
• Metric.isBounded_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {s : Set α} : Bornology.IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
• Metric.uniformSpace_eq_bot 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : PseudoMetricSpace.toUniformSpace = ⊥ ↔ ∃ r, 0 < r ∧ Pairwise fun x1 x2 => r ≤ dist x1 x2
• PseudoEMetricSpace.toPseudoMetricSpaceOfDist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {X : Type u_3} [e : PseudoEMetricSpace X] (dist : X → X → ℝ) (dist_nonneg : ∀ (x y : X), 0 ≤ dist x y) (h : ∀ (x y : X), edist x y = ENNReal.ofReal (dist x y)) : PseudoMetricSpace X
• nndist_triangle 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y z : α) : nndist x z ≤ nndist x y + nndist y z
• nndist_triangle_left 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y z : α) : nndist x y ≤ nndist z x + nndist z y
• nndist_triangle_right 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y z : α) : nndist x y ≤ nndist x z + nndist y z
• Metric.exists_ball_subset_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} (h : y ∈ Metric.ball x ε) : ∃ ε' > 0, Metric.ball y ε' ⊆ Metric.ball x ε
• Metric.isBounded_iff_eventually 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {s : Set α} : Bornology.IsBounded s ↔ ∀ᶠ (C : ℝ) in Filter.atTop, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
• Metric.uniformity_eq_comap_nhds_zero 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : uniformity α = Filter.comap (fun p => dist p.1 p.2) (nhds 0)
• Dense.exists_dist_lt 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : Dense s) (x : α) {ε : ℝ} (hε : 0 < ε) : ∃ y ∈ s, dist x y < ε
• Metric.eventually_nhds_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {p : α → Prop} : (∀ᶠ (y : α) in nhds x, p y) ↔ ∃ ε > 0, ∀ ⦃y : α⦄, dist y x < ε → p y
• Metric.isBounded_iff_nndist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {s : Set α} : Bornology.IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → nndist x y ≤ C
• Metric.isOpen_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {s : Set α} : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, Metric.ball x ε ⊆ s
• Metric.mem_nhds_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {s : Set α} : s ∈ nhds x ↔ ∃ ε > 0, Metric.ball x ε ⊆ s
• tendsto_iff_dist_tendsto_zero 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} {x : Filter β} {a : α} : Filter.Tendsto f x (nhds a) ↔ Filter.Tendsto (fun b => dist (f b) a) x (nhds 0)
• Metric.eventually_nhds_iff_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {p : α → Prop} : (∀ᶠ (y : α) in nhds x, p y) ↔ ∃ ε > 0, ∀ y ∈ Metric.ball x ε, p y
• Metric.isOpen_singleton_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u_3} [PseudoMetricSpace α] {x : α} : IsOpen {x} ↔ ∃ ε > 0, ∀ (y : α), dist y x < ε → y = x
• Metric.nhds_basis_ball_inv_nat_pos 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} : (nhds x).HasBasis (fun n => 0 < n) fun n => Metric.ball x (1 / ↑n)
• Metric.nhds_basis_closedBall_inv_nat_pos 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} : (nhds x).HasBasis (fun n => 0 < n) fun n => Metric.closedBall x (1 / ↑n)
• Metric.uniformity_basis_dist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : (uniformity α).HasBasis (fun ε => 0 < ε) fun ε => {p | dist p.1 p.2 < ε}
• Metric.uniformity_basis_dist_le 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : (uniformity α).HasBasis (fun x => 0 < x) fun ε => {p | dist p.1 p.2 ≤ ε}
• dist_dist_dist_le 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y x' y' : α) : dist (dist x y) (dist x' y') ≤ dist x x' + dist y y'
• Metric.tendsto_nhds 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : Filter β} {u : β → α} {a : α} : Filter.Tendsto u f (nhds a) ↔ ∀ ε > 0, ∀ᶠ (x : β) in f, dist (u x) a < ε
• Metric.continuous_iff' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : β → α} : Continuous f ↔ ∀ (a : β), ∀ ε > 0, ∀ᶠ (x : β) in nhds a, dist (f x) (f a) < ε
• Metric.isBounded_iff_exists_ge 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {s : Set α} (c : ℝ) : Bornology.IsBounded s ↔ ∃ C, c ≤ C ∧ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
• Metric.uniformity_basis_dist_rat 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : (uniformity α).HasBasis (fun r => 0 < r) fun r => {p | dist p.1 p.2 < ↑r}
• dist_triangle4 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x y z w : α) : dist x w ≤ dist x y + dist y z + dist z w
• dist_triangle4_left 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x₁ y₁ x₂ y₂ : α) : dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)
• dist_triangle4_right 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (x₁ y₁ x₂ y₂ : α) : dist x₁ y₁ ≤ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂
• Metric.continuousAt_iff' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : β → α} {b : β} : ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in nhds b, dist (f x) (f b) < ε
• Metric.mem_closure_range_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {β : Type v} [PseudoMetricSpace α] {e : β → α} {a : α} : a ∈ closure (Set.range e) ↔ ∀ ε > 0, ∃ k, dist a (e k) < ε
• Metric.nhds_basis_ball_inv_nat_succ 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} : (nhds x).HasBasis (fun x => True) fun n => Metric.ball x (1 / (↑n + 1))
• Metric.nhds_basis_closedBall_inv_nat_succ 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} : (nhds x).HasBasis (fun x => True) fun n => Metric.closedBall x (1 / (↑n + 1))
• Metric.sphere_disjoint_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Disjoint (Metric.sphere x ε) (Metric.ball x ε)
• tendsto_uniformity_iff_dist_tendsto_zero 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f : ι → α × α} {p : Filter ι} : Filter.Tendsto f p (uniformity α) ↔ Filter.Tendsto (fun x => dist (f x).1 (f x).2) p (nhds 0)
• Metric.continuousWithinAt_iff' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} : ContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ (x : β) in nhdsWithin b s, dist (f x) (f b) < ε
• Metric.dist_mem_uniformity 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {ε : ℝ} (ε0 : 0 < ε) : {p | dist p.1 p.2 < ε} ∈ uniformity α
• Metric.mem_closure_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {s : Set α} {a : α} : a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε
• Metric.dense_iff_iUnion_ball 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] (s : Set α) : Dense s ↔ ∀ r > 0, ⋃ c ∈ s, Metric.ball c r = Set.univ
• Metric.mem_nhdsWithin_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {s t : Set α} : s ∈ nhdsWithin x t ↔ ∃ ε > 0, Metric.ball x ε ∩ t ⊆ s
• Metric.mem_of_closed' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : IsClosed s) {a : α} : a ∈ s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε
• Metric.nhds_basis_ball_pow 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {r : ℝ} (h0 : 0 < r) (h1 : r < 1) : (nhds x).HasBasis (fun x => True) fun n => Metric.ball x (r ^ n)
• Metric.nhds_basis_closedBall_pow 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {x : α} {r : ℝ} (h0 : 0 < r) (h1 : r < 1) : (nhds x).HasBasis (fun x => True) fun n => Metric.closedBall x (r ^ n)
• PseudoMetricSpace.cobounded_sets 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [self : PseudoMetricSpace α] : (Bornology.cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• Metric.continuousOn_iff' 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : β → α} {s : Set β} : ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ (x : β) in nhdsWithin b s, dist (f x) (f b) < ε
• tendsto_of_tendsto_of_dist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f₁ f₂ : ι → α} {p : Filter ι} {a : α} (h₁ : Filter.Tendsto f₁ p (nhds a)) (h : Filter.Tendsto (fun x => dist (f₁ x) (f₂ x)) p (nhds 0)) : Filter.Tendsto f₂ p (nhds a)
• Filter.Tendsto.congr_dist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f₁ f₂ : ι → α} {p : Filter ι} {a : α} (h₁ : Filter.Tendsto f₁ p (nhds a)) (h : Filter.Tendsto (fun x => dist (f₁ x) (f₂ x)) p (nhds 0)) : Filter.Tendsto f₂ p (nhds a)
• tendsto_iff_of_dist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f₁ f₂ : ι → α} {p : Filter ι} {a : α} (h : Filter.Tendsto (fun x => dist (f₁ x) (f₂ x)) p (nhds 0)) : Filter.Tendsto f₁ p (nhds a) ↔ Filter.Tendsto f₂ p (nhds a)
• Metric.uniformity_basis_dist_inv_nat_pos 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : (uniformity α).HasBasis (fun n => 0 < n) fun n => {p | dist p.1 p.2 < 1 / ↑n}
• Metric.uniformity_basis_dist_le_inv_nat_pos 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : (uniformity α).HasBasis (fun n => 0 < n) fun n => {p | dist p.1 p.2 ≤ 1 / ↑n}
• Metric.uniformity_basis_dist_lt 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {R : ℝ} (hR : 0 < R) : (uniformity α).HasBasis (fun r => 0 < r ∧ r < R) fun r => {p | dist p.1 p.2 < r}
• Metric.tendsto_atTop 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} {a : α} : Filter.Tendsto u Filter.atTop (nhds a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε
• Metric.uniformContinuous_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} : UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃a b : α⦄, dist a b < δ → dist (f a) (f b) < ε
• Metric.uniformContinuous_iff_le 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} : UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃a b : α⦄, dist a b ≤ δ → dist (f a) (f b) ≤ ε
• nndist_ofAdd 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {X : Type u_1} [PseudoMetricSpace X] (a b : X) : nndist (Multiplicative.ofAdd a) (Multiplicative.ofAdd b) = nndist a b
• nndist_ofMul 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {X : Type u_1} [PseudoMetricSpace X] (a b : X) : nndist (Additive.ofMul a) (Additive.ofMul b) = nndist a b
• nndist_toDual 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {X : Type u_1} [PseudoMetricSpace X] (a b : X) : nndist (OrderDual.toDual a) (OrderDual.toDual b) = nndist a b
• Metric.uniformity_basis_dist_inv_nat_succ 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : (uniformity α).HasBasis (fun x => True) fun n => {p | dist p.1 p.2 < 1 / (↑n + 1)}
• Metric.uniformity_basis_dist_le_inv_nat_succ 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] : (uniformity α).HasBasis (fun x => True) fun n => {p | dist p.1 p.2 ≤ 1 / (↑n + 1)}
• Metric.mem_uniformity_dist 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} [PseudoMetricSpace α] {s : Set (α × α)} : s ∈ uniformity α ↔ ∃ ε > 0, ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ s
• Metric.mem_closure_range_iff_nat 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {β : Type v} [PseudoMetricSpace α] {e : β → α} {a : α} : a ∈ closure (Set.range e) ↔ ∀ (n : ℕ), ∃ k, dist a (e k) < 1 / (↑n + 1)
• Metric.continuous_iff 📋 Mathlib.Topology.MetricSpace.Pseudo.Defs
  {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} : Continuous f ↔ ∀ (b : α), ∀ ε > 0, ∃ δ > 0, ∀ (a : α), dist a b < δ → dist (f a) (f b) < ε

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