Documentation

Mathlib.Topology.MetricSpace.PseudoMetric

Pseudo-metric spaces #

This file defines pseudo-metric spaces: these differ from metric spaces by not imposing the condition dist x y = 0 → x = y. Many definitions and theorems expected on (pseudo-)metric spaces are already introduced on uniform spaces and topological spaces. For example: open and closed sets, compactness, completeness, continuity and uniform continuity.

Main definitions #

Additional useful definitions:

TODO (anyone): Add "Main results" section.

Tags #

pseudo_metric, dist

theorem UniformSpace.ofDist_aux (ε : ) (hε : 0 < ε) :
∃ δ > 0, x < δ, y < δ, x + y < ε
def UniformSpace.ofDist {α : Type u} (dist : αα) (dist_self : ∀ (x : α), dist x x = 0) (dist_comm : ∀ (x y : α), dist x y = dist y x) (dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z) :

Construct a uniform structure from a distance function and metric space axioms

Equations
Instances For
    @[reducible]
    def Bornology.ofDist {α : Type u_3} (dist : αα) (dist_comm : ∀ (x y : α), dist x y = dist y x) (dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z) :

    Construct a bornology from a distance function and metric space axioms.

    Equations
    Instances For
      theorem Dist.ext {α : Type u_3} (x : Dist α) (y : Dist α) (dist : Dist.dist = Dist.dist) :
      x = y
      theorem Dist.ext_iff {α : Type u_3} (x : Dist α) (y : Dist α) :
      x = y dist = dist
      class Dist (α : Type u_3) :
      Type u_3

      The distance function (given an ambient metric space on α), which returns a nonnegative real number dist x y given x y : α.

      • dist : αα
      Instances
        class PseudoMetricSpace (α : Type u) extends Dist :

        Pseudo metric and Metric spaces

        A pseudo metric space is endowed with a distance for which the requirement d(x,y)=0 → x = y might not hold. A metric space is a pseudo metric space such that d(x,y)=0 → x = y. Each pseudo metric space induces a canonical UniformSpace and hence a canonical TopologicalSpace This is enforced in the type class definition, by extending the UniformSpace structure. When instantiating a PseudoMetricSpace structure, the uniformity fields are not necessary, they will be filled in by default. In the same way, each (pseudo) metric space induces a (pseudo) emetric space structure. It is included in the structure, but filled in by default.

        Instances
          theorem PseudoMetricSpace.ext {α : Type u_3} {m : PseudoMetricSpace α} {m' : PseudoMetricSpace α} (h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist) :
          m = m'

          Two pseudo metric space structures with the same distance function coincide.

          Equations
          • PseudoMetricSpace.toEDist = { edist := PseudoMetricSpace.edist }
          def PseudoMetricSpace.ofDistTopology {α : Type u} [TopologicalSpace α] (dist : αα) (dist_self : ∀ (x : α), dist x x = 0) (dist_comm : ∀ (x y : α), dist x y = dist y x) (dist_triangle : ∀ (x y z : α), dist x z dist x y + dist y z) (H : ∀ (s : Set α), IsOpen s xs, ∃ ε > 0, ∀ (y : α), dist x y < εy s) :

          Construct a pseudo-metric space structure whose underlying topological space structure (definitionally) agrees which a pre-existing topology which is compatible with a given distance function.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem dist_self {α : Type u} [PseudoMetricSpace α] (x : α) :
            dist x x = 0
            theorem dist_comm {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) :
            dist x y = dist y x
            theorem edist_dist {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) :
            theorem dist_triangle {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) :
            dist x z dist x y + dist y z
            theorem dist_triangle_left {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) :
            dist x y dist z x + dist z y
            theorem dist_triangle_right {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) :
            dist x y dist x z + dist y z
            theorem dist_triangle4 {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) (w : α) :
            dist x w dist x y + dist y z + dist z w
            theorem dist_triangle4_left {α : Type u} [PseudoMetricSpace α] (x₁ : α) (y₁ : α) (x₂ : α) (y₂ : α) :
            dist x₂ y₂ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)
            theorem dist_triangle4_right {α : Type u} [PseudoMetricSpace α] (x₁ : α) (y₁ : α) (x₂ : α) (y₂ : α) :
            dist x₁ y₁ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂
            theorem dist_le_Ico_sum_dist {α : Type u} [PseudoMetricSpace α] (f : α) {m : } {n : } (h : m n) :
            dist (f m) (f n) Finset.sum (Finset.Ico m n) fun (i : ) => dist (f i) (f (i + 1))

            The triangle (polygon) inequality for sequences of points; Finset.Ico version.

            theorem dist_le_range_sum_dist {α : Type u} [PseudoMetricSpace α] (f : α) (n : ) :
            dist (f 0) (f n) Finset.sum (Finset.range n) fun (i : ) => dist (f i) (f (i + 1))

            The triangle (polygon) inequality for sequences of points; Finset.range version.

            theorem dist_le_Ico_sum_of_dist_le {α : Type u} [PseudoMetricSpace α] {f : α} {m : } {n : } (hmn : m n) {d : } (hd : ∀ {k : }, m kk < ndist (f k) (f (k + 1)) d k) :
            dist (f m) (f n) Finset.sum (Finset.Ico m n) fun (i : ) => d i

            A version of dist_le_Ico_sum_dist with each intermediate distance replaced with an upper estimate.

            theorem dist_le_range_sum_of_dist_le {α : Type u} [PseudoMetricSpace α] {f : α} (n : ) {d : } (hd : ∀ {k : }, k < ndist (f k) (f (k + 1)) d k) :
            dist (f 0) (f n) Finset.sum (Finset.range n) fun (i : ) => d i

            A version of dist_le_range_sum_dist with each intermediate distance replaced with an upper estimate.

            theorem swap_dist {α : Type u} [PseudoMetricSpace α] :
            Function.swap dist = dist
            theorem abs_dist_sub_le {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) :
            |dist x z - dist y z| dist x y
            theorem dist_nonneg {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} :
            0 dist x y

            Extension for the positivity tactic: distances are nonnegative.

            Instances For
              @[simp]
              theorem abs_dist {α : Type u} [PseudoMetricSpace α] {a : α} {b : α} :
              |dist a b| = dist a b
              class NNDist (α : Type u_3) :
              Type u_3

              A version of Dist that takes value in ℝ≥0.

              Instances

                Distance as a nonnegative real number.

                Equations
                • PseudoMetricSpace.toNNDist = { nndist := fun (a b : α) => { val := dist a b, property := } }
                theorem dist_nndist {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) :
                dist x y = (nndist x y)

                Express dist in terms of nndist

                @[simp]
                theorem coe_nndist {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) :
                (nndist x y) = dist x y
                theorem edist_nndist {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) :
                edist x y = (nndist x y)

                Express edist in terms of nndist

                theorem nndist_edist {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) :
                nndist x y = (edist x y).toNNReal

                Express nndist in terms of edist

                @[simp]
                theorem coe_nnreal_ennreal_nndist {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) :
                (nndist x y) = edist x y
                @[simp]
                theorem edist_lt_coe {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {c : NNReal} :
                edist x y < c nndist x y < c
                @[simp]
                theorem edist_le_coe {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {c : NNReal} :
                edist x y c nndist x y c
                theorem edist_lt_top {α : Type u_3} [PseudoMetricSpace α] (x : α) (y : α) :
                edist x y <

                In a pseudometric space, the extended distance is always finite

                theorem edist_ne_top {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) :

                In a pseudometric space, the extended distance is always finite

                @[simp]
                theorem nndist_self {α : Type u} [PseudoMetricSpace α] (a : α) :
                nndist a a = 0

                nndist x x vanishes

                @[simp]
                theorem dist_lt_coe {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {c : NNReal} :
                dist x y < c nndist x y < c
                @[simp]
                theorem dist_le_coe {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {c : NNReal} :
                dist x y c nndist x y c
                @[simp]
                theorem edist_lt_ofReal {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {r : } :
                @[simp]
                theorem edist_le_ofReal {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {r : } (hr : 0 r) :
                theorem nndist_dist {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) :

                Express nndist in terms of dist

                theorem nndist_comm {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) :
                nndist x y = nndist y x
                theorem nndist_triangle {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) :
                nndist x z nndist x y + nndist y z

                Triangle inequality for the nonnegative distance

                theorem nndist_triangle_left {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) :
                nndist x y nndist z x + nndist z y
                theorem nndist_triangle_right {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) :
                nndist x y nndist x z + nndist y z
                theorem dist_edist {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) :
                dist x y = (edist x y).toReal

                Express dist in terms of edist

                def Metric.ball {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ) :
                Set α

                ball x ε is the set of all points y with dist y x < ε

                Equations
                Instances For
                  @[simp]
                  theorem Metric.mem_ball {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : } :
                  y Metric.ball x ε dist y x < ε
                  theorem Metric.mem_ball' {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : } :
                  y Metric.ball x ε dist x y < ε
                  theorem Metric.pos_of_mem_ball {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : } (hy : y Metric.ball x ε) :
                  0 < ε
                  theorem Metric.mem_ball_self {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } (h : 0 < ε) :
                  @[simp]
                  theorem Metric.nonempty_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } :
                  @[simp]
                  theorem Metric.ball_eq_empty {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } :
                  Metric.ball x ε = ε 0
                  @[simp]
                  theorem Metric.ball_zero {α : Type u} [PseudoMetricSpace α] {x : α} :
                  theorem Metric.exists_lt_mem_ball_of_mem_ball {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : } (h : x Metric.ball y ε) :
                  ∃ ε' < ε, x Metric.ball y ε'

                  If a point belongs to an open ball, then there is a strictly smaller radius whose ball also contains it.

                  See also exists_lt_subset_ball.

                  theorem Metric.ball_eq_ball {α : Type u} [PseudoMetricSpace α] (ε : ) (x : α) :
                  UniformSpace.ball x {p : α × α | dist p.2 p.1 < ε} = Metric.ball x ε
                  theorem Metric.ball_eq_ball' {α : Type u} [PseudoMetricSpace α] (ε : ) (x : α) :
                  UniformSpace.ball x {p : α × α | dist p.1 p.2 < ε} = Metric.ball x ε
                  @[simp]
                  theorem Metric.iUnion_ball_nat {α : Type u} [PseudoMetricSpace α] (x : α) :
                  ⋃ (n : ), Metric.ball x n = Set.univ
                  @[simp]
                  theorem Metric.iUnion_ball_nat_succ {α : Type u} [PseudoMetricSpace α] (x : α) :
                  ⋃ (n : ), Metric.ball x (n + 1) = Set.univ
                  def Metric.closedBall {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ) :
                  Set α

                  closedBall x ε is the set of all points y with dist y x ≤ ε

                  Equations
                  Instances For
                    @[simp]
                    theorem Metric.mem_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : } :
                    theorem Metric.mem_closedBall' {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : } :
                    def Metric.sphere {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ) :
                    Set α

                    sphere x ε is the set of all points y with dist y x = ε

                    Equations
                    Instances For
                      @[simp]
                      theorem Metric.mem_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : } :
                      y Metric.sphere x ε dist y x = ε
                      theorem Metric.mem_sphere' {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : } :
                      y Metric.sphere x ε dist x y = ε
                      theorem Metric.ne_of_mem_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : } (h : y Metric.sphere x ε) (hε : ε 0) :
                      y x
                      theorem Metric.nonneg_of_mem_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : } (hy : y Metric.sphere x ε) :
                      0 ε
                      @[simp]
                      theorem Metric.sphere_eq_empty_of_neg {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } (hε : ε < 0) :
                      theorem Metric.sphere_eq_empty_of_subsingleton {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } [Subsingleton α] (hε : ε 0) :
                      instance Metric.sphere_isEmpty_of_subsingleton {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } [Subsingleton α] [NeZero ε] :
                      Equations
                      • =
                      theorem Metric.mem_closedBall_self {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } (h : 0 ε) :
                      @[simp]
                      theorem Metric.nonempty_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } :
                      @[simp]
                      theorem Metric.closedBall_eq_empty {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } :
                      theorem Metric.closedBall_eq_sphere_of_nonpos {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } (hε : ε 0) :

                      Closed balls and spheres coincide when the radius is non-positive

                      theorem Metric.sphere_subset_ball {α : Type u} [PseudoMetricSpace α] {x : α} {r : } {R : } (h : r < R) :
                      theorem Metric.closedBall_disjoint_ball {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {δ : } {ε : } (h : δ + ε dist x y) :
                      theorem Metric.ball_disjoint_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {δ : } {ε : } (h : δ + ε dist x y) :
                      theorem Metric.ball_disjoint_ball {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {δ : } {ε : } (h : δ + ε dist x y) :
                      theorem Metric.closedBall_disjoint_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {δ : } {ε : } (h : δ + ε < dist x y) :
                      @[simp]
                      theorem Metric.ball_union_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } :
                      @[simp]
                      theorem Metric.sphere_union_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } :
                      @[simp]
                      @[simp]
                      theorem Metric.mem_ball_comm {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : } :
                      theorem Metric.mem_closedBall_comm {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : } :
                      theorem Metric.mem_sphere_comm {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : } :
                      theorem Metric.ball_subset_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε₁ : } {ε₂ : } (h : ε₁ ε₂) :
                      Metric.ball x ε₁ Metric.ball x ε₂
                      theorem Metric.closedBall_eq_bInter_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } :
                      Metric.closedBall x ε = ⋂ (δ : ), ⋂ (_ : δ > ε), Metric.ball x δ
                      theorem Metric.ball_subset_ball' {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε₁ : } {ε₂ : } (h : ε₁ + dist x y ε₂) :
                      Metric.ball x ε₁ Metric.ball y ε₂
                      theorem Metric.closedBall_subset_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {ε₁ : } {ε₂ : } (h : ε₁ ε₂) :
                      theorem Metric.closedBall_subset_closedBall' {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε₁ : } {ε₂ : } (h : ε₁ + dist x y ε₂) :
                      theorem Metric.closedBall_subset_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε₁ : } {ε₂ : } (h : ε₁ < ε₂) :
                      theorem Metric.closedBall_subset_ball' {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε₁ : } {ε₂ : } (h : ε₁ + dist x y < ε₂) :
                      theorem Metric.dist_le_add_of_nonempty_closedBall_inter_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε₁ : } {ε₂ : } (h : Set.Nonempty (Metric.closedBall x ε₁ Metric.closedBall y ε₂)) :
                      dist x y ε₁ + ε₂
                      theorem Metric.dist_lt_add_of_nonempty_closedBall_inter_ball {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε₁ : } {ε₂ : } (h : Set.Nonempty (Metric.closedBall x ε₁ Metric.ball y ε₂)) :
                      dist x y < ε₁ + ε₂
                      theorem Metric.dist_lt_add_of_nonempty_ball_inter_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε₁ : } {ε₂ : } (h : Set.Nonempty (Metric.ball x ε₁ Metric.closedBall y ε₂)) :
                      dist x y < ε₁ + ε₂
                      theorem Metric.dist_lt_add_of_nonempty_ball_inter_ball {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε₁ : } {ε₂ : } (h : Set.Nonempty (Metric.ball x ε₁ Metric.ball y ε₂)) :
                      dist x y < ε₁ + ε₂
                      @[simp]
                      theorem Metric.iUnion_closedBall_nat {α : Type u} [PseudoMetricSpace α] (x : α) :
                      ⋃ (n : ), Metric.closedBall x n = Set.univ
                      theorem Metric.iUnion_inter_closedBall_nat {α : Type u} [PseudoMetricSpace α] (s : Set α) (x : α) :
                      ⋃ (n : ), s Metric.closedBall x n = s
                      theorem Metric.ball_subset {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε₁ : } {ε₂ : } (h : dist x y ε₂ - ε₁) :
                      Metric.ball x ε₁ Metric.ball y ε₂
                      theorem Metric.ball_half_subset {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } (y : α) (h : y Metric.ball x (ε / 2)) :
                      theorem Metric.exists_ball_subset_ball {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : } (h : y Metric.ball x ε) :
                      ∃ ε' > 0, Metric.ball y ε' Metric.ball x ε
                      theorem Metric.forall_of_forall_mem_closedBall {α : Type u} [PseudoMetricSpace α] (p : αProp) (x : α) (H : ∃ᶠ (R : ) in Filter.atTop, yMetric.closedBall x R, p y) (y : α) :
                      p y

                      If a property holds for all points in closed balls of arbitrarily large radii, then it holds for all points.

                      theorem Metric.forall_of_forall_mem_ball {α : Type u} [PseudoMetricSpace α] (p : αProp) (x : α) (H : ∃ᶠ (R : ) in Filter.atTop, yMetric.ball x R, p y) (y : α) :
                      p y

                      If a property holds for all points in balls of arbitrarily large radii, then it holds for all points.

                      theorem Metric.isBounded_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} :
                      Bornology.IsBounded s ∃ (C : ), ∀ ⦃x : α⦄, x s∀ ⦃y : α⦄, y sdist x y C
                      theorem Metric.isBounded_iff_eventually {α : Type u} [PseudoMetricSpace α] {s : Set α} :
                      Bornology.IsBounded s ∀ᶠ (C : ) in Filter.atTop, ∀ ⦃x : α⦄, x s∀ ⦃y : α⦄, y sdist x y C
                      theorem Metric.isBounded_iff_exists_ge {α : Type u} [PseudoMetricSpace α] {s : Set α} (c : ) :
                      Bornology.IsBounded s ∃ (C : ), c C ∀ ⦃x : α⦄, x s∀ ⦃y : α⦄, y sdist x y C
                      theorem Metric.isBounded_iff_nndist {α : Type u} [PseudoMetricSpace α] {s : Set α} :
                      Bornology.IsBounded s ∃ (C : NNReal), ∀ ⦃x : α⦄, x s∀ ⦃y : α⦄, y snndist x y C
                      theorem Metric.toUniformSpace_eq {α : Type u} [PseudoMetricSpace α] :
                      PseudoMetricSpace.toUniformSpace = UniformSpace.ofDist dist
                      theorem Metric.uniformity_basis_dist {α : Type u} [PseudoMetricSpace α] :
                      Filter.HasBasis (uniformity α) (fun (ε : ) => 0 < ε) fun (ε : ) => {p : α × α | dist p.1 p.2 < ε}
                      theorem Metric.mk_uniformity_basis {α : Type u} [PseudoMetricSpace α] {β : Type u_3} {p : βProp} {f : β} (hf₀ : ∀ (i : β), p i0 < f i) (hf : ∀ ⦃ε : ⦄, 0 < ε∃ (i : β), p i f i ε) :
                      Filter.HasBasis (uniformity α) p fun (i : β) => {p : α × α | dist p.1 p.2 < f i}

                      Given f : β → ℝ, if f sends {i | p i} to a set of positive numbers accumulating to zero, then f i-neighborhoods of the diagonal form a basis of 𝓤 α.

                      For specific bases see uniformity_basis_dist, uniformity_basis_dist_inv_nat_succ, and uniformity_basis_dist_inv_nat_pos.

                      theorem Metric.uniformity_basis_dist_rat {α : Type u} [PseudoMetricSpace α] :
                      Filter.HasBasis (uniformity α) (fun (r : ) => 0 < r) fun (r : ) => {p : α × α | dist p.1 p.2 < r}
                      theorem Metric.uniformity_basis_dist_inv_nat_succ {α : Type u} [PseudoMetricSpace α] :
                      Filter.HasBasis (uniformity α) (fun (x : ) => True) fun (n : ) => {p : α × α | dist p.1 p.2 < 1 / (n + 1)}
                      theorem Metric.uniformity_basis_dist_inv_nat_pos {α : Type u} [PseudoMetricSpace α] :
                      Filter.HasBasis (uniformity α) (fun (n : ) => 0 < n) fun (n : ) => {p : α × α | dist p.1 p.2 < 1 / n}
                      theorem Metric.uniformity_basis_dist_pow {α : Type u} [PseudoMetricSpace α] {r : } (h0 : 0 < r) (h1 : r < 1) :
                      Filter.HasBasis (uniformity α) (fun (x : ) => True) fun (n : ) => {p : α × α | dist p.1 p.2 < r ^ n}
                      theorem Metric.uniformity_basis_dist_lt {α : Type u} [PseudoMetricSpace α] {R : } (hR : 0 < R) :
                      Filter.HasBasis (uniformity α) (fun (r : ) => 0 < r r < R) fun (r : ) => {p : α × α | dist p.1 p.2 < r}
                      theorem Metric.mk_uniformity_basis_le {α : Type u} [PseudoMetricSpace α] {β : Type u_3} {p : βProp} {f : β} (hf₀ : ∀ (x : β), p x0 < f x) (hf : ∀ (ε : ), 0 < ε∃ (x : β), p x f x ε) :
                      Filter.HasBasis (uniformity α) p fun (x : β) => {p : α × α | dist p.1 p.2 f x}

                      Given f : β → ℝ, if f sends {i | p i} to a set of positive numbers accumulating to zero, then closed neighborhoods of the diagonal of sizes {f i | p i} form a basis of 𝓤 α.

                      Currently we have only one specific basis uniformity_basis_dist_le based on this constructor. More can be easily added if needed in the future.

                      theorem Metric.uniformity_basis_dist_le {α : Type u} [PseudoMetricSpace α] :
                      Filter.HasBasis (uniformity α) (fun (x : ) => 0 < x) fun (ε : ) => {p : α × α | dist p.1 p.2 ε}

                      Constant size closed neighborhoods of the diagonal form a basis of the uniformity filter.

                      theorem Metric.uniformity_basis_dist_le_pow {α : Type u} [PseudoMetricSpace α] {r : } (h0 : 0 < r) (h1 : r < 1) :
                      Filter.HasBasis (uniformity α) (fun (x : ) => True) fun (n : ) => {p : α × α | dist p.1 p.2 r ^ n}
                      theorem Metric.mem_uniformity_dist {α : Type u} [PseudoMetricSpace α] {s : Set (α × α)} :
                      s uniformity α ∃ ε > 0, ∀ {a b : α}, dist a b < ε(a, b) s
                      theorem Metric.dist_mem_uniformity {α : Type u} [PseudoMetricSpace α] {ε : } (ε0 : 0 < ε) :
                      {p : α × α | dist p.1 p.2 < ε} uniformity α

                      A constant size neighborhood of the diagonal is an entourage.

                      theorem Metric.uniformContinuous_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : αβ} :
                      UniformContinuous f ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δdist (f a) (f b) < ε
                      theorem Metric.uniformContinuousOn_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : αβ} {s : Set α} :
                      UniformContinuousOn f s ε > 0, ∃ δ > 0, xs, ys, dist x y < δdist (f x) (f y) < ε
                      theorem Metric.uniformContinuousOn_iff_le {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : αβ} {s : Set α} :
                      UniformContinuousOn f s ε > 0, ∃ δ > 0, xs, ys, dist x y δdist (f x) (f y) ε
                      theorem Metric.uniformInducing_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : αβ} :
                      UniformInducing f UniformContinuous f δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < εdist a b < δ
                      theorem Metric.uniformEmbedding_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : αβ} :
                      UniformEmbedding f Function.Injective f UniformContinuous f δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < εdist a b < δ
                      theorem Metric.controlled_of_uniformEmbedding {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : αβ} (h : UniformEmbedding f) :
                      (ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δdist (f a) (f b) < ε) δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < εdist a b < δ

                      If a map between pseudometric spaces is a uniform embedding then the distance between f x and f y is controlled in terms of the distance between x and y.

                      theorem Metric.totallyBounded_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} :
                      TotallyBounded s ε > 0, ∃ (t : Set α), Set.Finite t s ⋃ y ∈ t, Metric.ball y ε
                      theorem Metric.totallyBounded_of_finite_discretization {α : Type u} [PseudoMetricSpace α] {s : Set α} (H : ε > 0, ∃ (β : Type u) (x : Fintype β) (F : sβ), ∀ (x y : s), F x = F ydist x y < ε) :

                      A pseudometric space is totally bounded if one can reconstruct up to any ε>0 any element of the space from finitely many data.

                      theorem Metric.finite_approx_of_totallyBounded {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : TotallyBounded s) (ε : ) :
                      ε > 0∃ t ⊆ s, Set.Finite t s ⋃ y ∈ t, Metric.ball y ε
                      theorem Metric.tendstoUniformlyOnFilter_iff {α : Type u} {β : Type v} {ι : Type u_2} [PseudoMetricSpace α] {F : ιβα} {f : βα} {p : Filter ι} {p' : Filter β} :
                      TendstoUniformlyOnFilter F f p p' ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε

                      Expressing uniform convergence using dist

                      theorem Metric.tendstoLocallyUniformlyOn_iff {α : Type u} {β : Type v} {ι : Type u_2} [PseudoMetricSpace α] [TopologicalSpace β] {F : ιβα} {f : βα} {p : Filter ι} {s : Set β} :
                      TendstoLocallyUniformlyOn F f p s ε > 0, xs, ∃ t ∈ nhdsWithin x s, ∀ᶠ (n : ι) in p, yt, dist (f y) (F n y) < ε

                      Expressing locally uniform convergence on a set using dist.

                      theorem Metric.tendstoUniformlyOn_iff {α : Type u} {β : Type v} {ι : Type u_2} [PseudoMetricSpace α] {F : ιβα} {f : βα} {p : Filter ι} {s : Set β} :
                      TendstoUniformlyOn F f p s ε > 0, ∀ᶠ (n : ι) in p, xs, dist (f x) (F n x) < ε

                      Expressing uniform convergence on a set using dist.

                      theorem Metric.tendstoLocallyUniformly_iff {α : Type u} {β : Type v} {ι : Type u_2} [PseudoMetricSpace α] [TopologicalSpace β] {F : ιβα} {f : βα} {p : Filter ι} :
                      TendstoLocallyUniformly F f p ε > 0, ∀ (x : β), ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, yt, dist (f y) (F n y) < ε

                      Expressing locally uniform convergence using dist.

                      theorem Metric.tendstoUniformly_iff {α : Type u} {β : Type v} {ι : Type u_2} [PseudoMetricSpace α] {F : ιβα} {f : βα} {p : Filter ι} :
                      TendstoUniformly F f p ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε

                      Expressing uniform convergence using dist.

                      theorem Metric.cauchy_iff {α : Type u} [PseudoMetricSpace α] {f : Filter α} :
                      Cauchy f Filter.NeBot f ε > 0, ∃ t ∈ f, xt, yt, dist x y < ε
                      theorem Metric.nhds_basis_ball {α : Type u} [PseudoMetricSpace α] {x : α} :
                      Filter.HasBasis (nhds x) (fun (x : ) => 0 < x) (Metric.ball x)
                      theorem Metric.mem_nhds_iff {α : Type u} [PseudoMetricSpace α] {x : α} {s : Set α} :
                      s nhds x ∃ ε > 0, Metric.ball x ε s
                      theorem Metric.eventually_nhds_iff {α : Type u} [PseudoMetricSpace α] {x : α} {p : αProp} :
                      (∀ᶠ (y : α) in nhds x, p y) ∃ ε > 0, ∀ ⦃y : α⦄, dist y x < εp y
                      theorem Metric.eventually_nhds_iff_ball {α : Type u} [PseudoMetricSpace α] {x : α} {p : αProp} :
                      (∀ᶠ (y : α) in nhds x, p y) ∃ ε > 0, yMetric.ball x ε, p y
                      theorem Metric.eventually_nhds_prod_iff {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f : Filter ι} {x₀ : α} {p : α × ιProp} :
                      (∀ᶠ (x : α × ι) in nhds x₀ ×ˢ f, p x) ∃ ε > 0, ∃ (pa : ιProp), (∀ᶠ (i : ι) in f, pa i) ∀ {x : α}, dist x x₀ < ε∀ {i : ι}, pa ip (x, i)

                      A version of Filter.eventually_prod_iff where the first filter consists of neighborhoods in a pseudo-metric space.

                      theorem Metric.eventually_prod_nhds_iff {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f : Filter ι} {x₀ : α} {p : ι × αProp} :
                      (∀ᶠ (x : ι × α) in f ×ˢ nhds x₀, p x) ∃ (pa : ιProp), (∀ᶠ (i : ι) in f, pa i) ∃ ε > 0, ∀ {i : ι}, pa i∀ {x : α}, dist x x₀ < εp (i, x)

                      A version of Filter.eventually_prod_iff where the second filter consists of neighborhoods in a pseudo-metric space.

                      theorem Metric.nhds_basis_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} :
                      Filter.HasBasis (nhds x) (fun (ε : ) => 0 < ε) (Metric.closedBall x)
                      theorem Metric.nhds_basis_ball_inv_nat_succ {α : Type u} [PseudoMetricSpace α] {x : α} :
                      Filter.HasBasis (nhds x) (fun (x : ) => True) fun (n : ) => Metric.ball x (1 / (n + 1))
                      theorem Metric.nhds_basis_ball_inv_nat_pos {α : Type u} [PseudoMetricSpace α] {x : α} :
                      Filter.HasBasis (nhds x) (fun (n : ) => 0 < n) fun (n : ) => Metric.ball x (1 / n)
                      theorem Metric.nhds_basis_ball_pow {α : Type u} [PseudoMetricSpace α] {x : α} {r : } (h0 : 0 < r) (h1 : r < 1) :
                      Filter.HasBasis (nhds x) (fun (x : ) => True) fun (n : ) => Metric.ball x (r ^ n)
                      theorem Metric.nhds_basis_closedBall_pow {α : Type u} [PseudoMetricSpace α] {x : α} {r : } (h0 : 0 < r) (h1 : r < 1) :
                      Filter.HasBasis (nhds x) (fun (x : ) => True) fun (n : ) => Metric.closedBall x (r ^ n)
                      theorem Metric.isOpen_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} :
                      IsOpen s xs, ∃ ε > 0, Metric.ball x ε s
                      theorem Metric.isOpen_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } :
                      theorem Metric.ball_mem_nhds {α : Type u} [PseudoMetricSpace α] (x : α) {ε : } (ε0 : 0 < ε) :
                      theorem Metric.closedBall_mem_nhds {α : Type u} [PseudoMetricSpace α] (x : α) {ε : } (ε0 : 0 < ε) :
                      theorem Metric.closedBall_mem_nhds_of_mem {α : Type u} [PseudoMetricSpace α] {x : α} {c : α} {ε : } (h : x Metric.ball c ε) :
                      theorem Metric.nhdsWithin_basis_ball {α : Type u} [PseudoMetricSpace α] {x : α} {s : Set α} :
                      Filter.HasBasis (nhdsWithin x s) (fun (ε : ) => 0 < ε) fun (ε : ) => Metric.ball x ε s
                      theorem Metric.mem_nhdsWithin_iff {α : Type u} [PseudoMetricSpace α] {x : α} {s : Set α} {t : Set α} :
                      s nhdsWithin x t ∃ ε > 0, Metric.ball x ε t s
                      theorem Metric.tendsto_nhdsWithin_nhdsWithin {α : Type u} {β : Type v} [PseudoMetricSpace α] {s : Set α} [PseudoMetricSpace β] {t : Set β} {f : αβ} {a : α} {b : β} :
                      Filter.Tendsto f (nhdsWithin a s) (nhdsWithin b t) ε > 0, ∃ δ > 0, ∀ {x : α}, x sdist x a < δf x t dist (f x) b < ε
                      theorem Metric.tendsto_nhdsWithin_nhds {α : Type u} {β : Type v} [PseudoMetricSpace α] {s : Set α} [PseudoMetricSpace β] {f : αβ} {a : α} {b : β} :
                      Filter.Tendsto f (nhdsWithin a s) (nhds b) ε > 0, ∃ δ > 0, ∀ {x : α}, x sdist x a < δdist (f x) b < ε
                      theorem Metric.tendsto_nhds_nhds {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : αβ} {a : α} {b : β} :
                      Filter.Tendsto f (nhds a) (nhds b) ε > 0, ∃ δ > 0, ∀ {x : α}, dist x a < δdist (f x) b < ε
                      theorem Metric.continuousAt_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : αβ} {a : α} :
                      ContinuousAt f a ε > 0, ∃ δ > 0, ∀ {x : α}, dist x a < δdist (f x) (f a) < ε
                      theorem Metric.continuousWithinAt_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : αβ} {a : α} {s : Set α} :
                      ContinuousWithinAt f s a ε > 0, ∃ δ > 0, ∀ {x : α}, x sdist x a < δdist (f x) (f a) < ε
                      theorem Metric.continuousOn_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : αβ} {s : Set α} :
                      ContinuousOn f s bs, ε > 0, ∃ δ > 0, as, dist a b < δdist (f a) (f b) < ε
                      theorem Metric.continuous_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : αβ} :
                      Continuous f ∀ (b : α), ε > 0, ∃ δ > 0, ∀ (a : α), dist a b < δdist (f a) (f b) < ε
                      theorem Metric.tendsto_nhds {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : Filter β} {u : βα} {a : α} :
                      Filter.Tendsto u f (nhds a) ε > 0, ∀ᶠ (x : β) in f, dist (u x) a < ε
                      theorem Metric.continuousAt_iff' {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : βα} {b : β} :
                      ContinuousAt f b ε > 0, ∀ᶠ (x : β) in nhds b, dist (f x) (f b) < ε
                      theorem Metric.continuousWithinAt_iff' {α : 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) < ε
                      theorem Metric.continuousOn_iff' {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : βα} {s : Set β} :
                      ContinuousOn f s bs, ε > 0, ∀ᶠ (x : β) in nhdsWithin b s, dist (f x) (f b) < ε
                      theorem Metric.continuous_iff' {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : βα} :
                      Continuous f ∀ (a : β), ε > 0, ∀ᶠ (x : β) in nhds a, dist (f x) (f a) < ε
                      theorem Metric.tendsto_atTop {α : Type u} {β : Type v} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : βα} {a : α} :
                      Filter.Tendsto u Filter.atTop (nhds a) ε > 0, ∃ (N : β), nN, dist (u n) a < ε
                      theorem Metric.tendsto_atTop' {α : Type u} {β : Type v} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] [NoMaxOrder β] {u : βα} {a : α} :
                      Filter.Tendsto u Filter.atTop (nhds a) ε > 0, ∃ (N : β), n > N, dist (u n) a < ε

                      A variant of tendsto_atTop that uses ∃ N, ∀ n > N, ... rather than ∃ N, ∀ n ≥ N, ...

                      theorem Metric.isOpen_singleton_iff {α : Type u_3} [PseudoMetricSpace α] {x : α} :
                      IsOpen {x} ∃ ε > 0, ∀ (y : α), dist y x < εy = x
                      theorem Metric.exists_ball_inter_eq_singleton_of_mem_discrete {α : Type u} [PseudoMetricSpace α] {s : Set α} [DiscreteTopology s] {x : α} (hx : x s) :
                      ∃ ε > 0, Metric.ball x ε s = {x}

                      Given a point x in a discrete subset s of a pseudometric space, there is an open ball centered at x and intersecting s only at x.

                      theorem Metric.exists_closedBall_inter_eq_singleton_of_discrete {α : Type u} [PseudoMetricSpace α] {s : Set α} [DiscreteTopology s] {x : α} (hx : x s) :
                      ∃ ε > 0, Metric.closedBall x ε s = {x}

                      Given a point x in a discrete subset s of a pseudometric space, there is a closed ball of positive radius centered at x and intersecting s only at x.

                      theorem Dense.exists_dist_lt {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : Dense s) (x : α) {ε : } (hε : 0 < ε) :
                      ∃ y ∈ s, dist x y < ε
                      theorem DenseRange.exists_dist_lt {α : Type u} [PseudoMetricSpace α] {β : Type u_3} {f : βα} (hf : DenseRange f) (x : α) {ε : } (hε : 0 < ε) :
                      ∃ (y : β), dist x (f y) < ε
                      theorem Metric.uniformity_edist_aux {α : Type u_3} (d : ααNNReal) :
                      ⨅ (ε : ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | (d p.1 p.2) < ε} = ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal {p : α × α | (d p.1 p.2) < ε}
                      theorem Metric.uniformity_edist {α : Type u} [PseudoMetricSpace α] :
                      uniformity α = ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal {p : α × α | edist p.1 p.2 < ε}

                      A pseudometric space induces a pseudoemetric space

                      Equations
                      • PseudoMetricSpace.toPseudoEMetricSpace = let __src := inst; PseudoEMetricSpace.mk PseudoMetricSpace.toUniformSpace
                      @[deprecated uniformity_basis_edist]
                      theorem Metric.uniformity_basis_edist {α : Type u} [PseudoMetricSpace α] :
                      Filter.HasBasis (uniformity α) (fun (ε : ENNReal) => 0 < ε) fun (ε : ENNReal) => {p : α × α | edist p.1 p.2 < ε}

                      Expressing the uniformity in terms of edist

                      theorem Metric.eball_top_eq_univ {α : Type u} [PseudoMetricSpace α] (x : α) :
                      EMetric.ball x = Set.univ

                      In a pseudometric space, an open ball of infinite radius is the whole space

                      @[simp]
                      theorem Metric.emetric_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } :

                      Balls defined using the distance or the edistance coincide

                      @[simp]
                      theorem Metric.emetric_ball_nnreal {α : Type u} [PseudoMetricSpace α] {x : α} {ε : NNReal} :
                      EMetric.ball x ε = Metric.ball x ε

                      Balls defined using the distance or the edistance coincide

                      theorem Metric.emetric_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } (h : 0 ε) :

                      Closed balls defined using the distance or the edistance coincide

                      @[simp]

                      Closed balls defined using the distance or the edistance coincide

                      @[simp]
                      theorem Metric.emetric_ball_top {α : Type u} [PseudoMetricSpace α] (x : α) :
                      EMetric.ball x = Set.univ
                      theorem Metric.inseparable_iff {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} :
                      Inseparable x y dist x y = 0
                      @[reducible]

                      Build a new pseudometric space from an old one where the bundled uniform structure is provably (but typically non-definitionaly) equal to some given uniform structure. See Note [forgetful inheritance].

                      Equations
                      Instances For
                        @[reducible]
                        def PseudoMetricSpace.replaceTopology {γ : Type u_3} [U : TopologicalSpace γ] (m : PseudoMetricSpace γ) (H : U = UniformSpace.toTopologicalSpace) :

                        Build a new pseudo metric space from an old one where the bundled topological structure is provably (but typically non-definitionaly) equal to some given topological structure. See Note [forgetful inheritance].

                        Equations
                        Instances For
                          theorem PseudoMetricSpace.replaceTopology_eq {γ : Type u_3} [U : TopologicalSpace γ] (m : PseudoMetricSpace γ) (H : U = UniformSpace.toTopologicalSpace) :
                          @[reducible]
                          def PseudoEMetricSpace.toPseudoMetricSpaceOfDist {α : Type u} [e : PseudoEMetricSpace α] (dist : αα) (edist_ne_top : ∀ (x y : α), edist x y ) (h : ∀ (x y : α), dist x y = (edist x y).toReal) :

                          One gets a pseudometric space from an emetric space if the edistance is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the uniformity are defeq in the pseudometric space and the pseudoemetric space. In this definition, the distance is given separately, to be able to prescribe some expression which is not defeq to the push-forward of the edistance to reals. See note [reducible non-instances].

                          Equations
                          Instances For
                            @[reducible]

                            One gets a pseudometric space from an emetric space if the edistance is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the uniformity are defeq in the pseudometric space and the emetric space.

                            Equations
                            Instances For
                              @[reducible]

                              Build a new pseudometric space from an old one where the bundled bornology structure is provably (but typically non-definitionaly) equal to some given bornology structure. See Note [forgetful inheritance].

                              Equations
                              Instances For

                                Instantiate the reals as a pseudometric space.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                theorem Real.dist_eq (x : ) (y : ) :
                                dist x y = |x - y|
                                theorem Real.nndist_eq (x : ) (y : ) :
                                nndist x y = Real.nnabs (x - y)
                                theorem Real.nndist_eq' (x : ) (y : ) :
                                nndist x y = Real.nnabs (y - x)
                                theorem Real.dist_0_eq_abs (x : ) :
                                dist x 0 = |x|
                                theorem Real.dist_left_le_of_mem_uIcc {x : } {y : } {z : } (h : y Set.uIcc x z) :
                                dist x y dist x z
                                theorem Real.dist_right_le_of_mem_uIcc {x : } {y : } {z : } (h : y Set.uIcc x z) :
                                dist y z dist x z
                                theorem Real.dist_le_of_mem_uIcc {x : } {y : } {x' : } {y' : } (hx : x Set.uIcc x' y') (hy : y Set.uIcc x' y') :
                                dist x y dist x' y'
                                theorem Real.dist_le_of_mem_Icc {x : } {y : } {x' : } {y' : } (hx : x Set.Icc x' y') (hy : y Set.Icc x' y') :
                                dist x y y' - x'
                                theorem Real.dist_le_of_mem_Icc_01 {x : } {y : } (hx : x Set.Icc 0 1) (hy : y Set.Icc 0 1) :
                                dist x y 1
                                theorem Real.ball_eq_Ioo (x : ) (r : ) :
                                Metric.ball x r = Set.Ioo (x - r) (x + r)
                                theorem Real.closedBall_eq_Icc {x : } {r : } :
                                Metric.closedBall x r = Set.Icc (x - r) (x + r)
                                theorem Real.Ioo_eq_ball (x : ) (y : ) :
                                Set.Ioo x y = Metric.ball ((x + y) / 2) ((y - x) / 2)
                                theorem Real.Icc_eq_closedBall (x : ) (y : ) :
                                Set.Icc x y = Metric.closedBall ((x + y) / 2) ((y - x) / 2)
                                theorem totallyBounded_Icc {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) :
                                theorem totallyBounded_Ico {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) :
                                theorem totallyBounded_Ioc {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) :
                                theorem totallyBounded_Ioo {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) :
                                theorem squeeze_zero' {α : Type u_3} {f : α} {g : α} {t₀ : Filter α} (hf : ∀ᶠ (t : α) in t₀, 0 f t) (hft : ∀ᶠ (t : α) in t₀, f t g t) (g0 : Filter.Tendsto g t₀ (nhds 0)) :
                                Filter.Tendsto f t₀ (nhds 0)

                                Special case of the sandwich theorem; see tendsto_of_tendsto_of_tendsto_of_le_of_le' for the general case.

                                theorem squeeze_zero {α : Type u_3} {f : α} {g : α} {t₀ : Filter α} (hf : ∀ (t : α), 0 f t) (hft : ∀ (t : α), f t g t) (g0 : Filter.Tendsto g t₀ (nhds 0)) :
                                Filter.Tendsto f t₀ (nhds 0)

                                Special case of the sandwich theorem; see tendsto_of_tendsto_of_tendsto_of_le_of_le and tendsto_of_tendsto_of_tendsto_of_le_of_le' for the general case.

                                theorem Metric.uniformity_eq_comap_nhds_zero {α : Type u} [PseudoMetricSpace α] :
                                uniformity α = Filter.comap (fun (p : α × α) => dist p.1 p.2) (nhds 0)
                                theorem cauchySeq_iff_tendsto_dist_atTop_0 {α : Type u} {β : Type v} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : βα} :
                                CauchySeq u Filter.Tendsto (fun (n : β × β) => dist (u n.1) (u n.2)) Filter.atTop (nhds 0)
                                theorem tendsto_uniformity_iff_dist_tendsto_zero {α : 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)
                                theorem Filter.Tendsto.congr_dist {α : 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)
                                theorem tendsto_of_tendsto_of_dist {α : 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)

                                Alias of Filter.Tendsto.congr_dist.

                                theorem tendsto_iff_of_dist {α : 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)
                                theorem eventually_closedBall_subset {α : Type u} [PseudoMetricSpace α] {x : α} {u : Set α} (hu : u nhds x) :
                                ∀ᶠ (r : ) in nhds 0, Metric.closedBall x r u

                                If u is a neighborhood of x, then for small enough r, the closed ball Metric.closedBall x r is contained in u.

                                @[reducible]
                                def PseudoMetricSpace.induced {α : Type u_3} {β : Type u_4} (f : αβ) (m : PseudoMetricSpace β) :

                                Pseudometric space structure pulled back by a function.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  def Inducing.comapPseudoMetricSpace {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [m : PseudoMetricSpace β] {f : αβ} (hf : Inducing f) :

                                  Pull back a pseudometric space structure by an inducing map. This is a version of PseudoMetricSpace.induced useful in case if the domain already has a TopologicalSpace structure.

                                  Equations
                                  Instances For
                                    def UniformInducing.comapPseudoMetricSpace {α : Type u_3} {β : Type u_4} [UniformSpace α] [m : PseudoMetricSpace β] (f : αβ) (h : UniformInducing f) :

                                    Pull back a pseudometric space structure by a uniform inducing map. This is a version of PseudoMetricSpace.induced useful in case if the domain already has a UniformSpace structure.

                                    Equations
                                    Instances For
                                      Equations
                                      theorem Subtype.dist_eq {α : Type u} [PseudoMetricSpace α] {p : αProp} (x : Subtype p) (y : Subtype p) :
                                      dist x y = dist x y
                                      theorem Subtype.nndist_eq {α : Type u} [PseudoMetricSpace α] {p : αProp} (x : Subtype p) (y : Subtype p) :
                                      nndist x y = nndist x y
                                      Equations
                                      Equations
                                      @[simp]
                                      theorem AddOpposite.dist_op {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) :
                                      @[simp]
                                      theorem MulOpposite.dist_op {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) :
                                      @[simp]
                                      theorem AddOpposite.nndist_op {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) :
                                      @[simp]
                                      theorem MulOpposite.nndist_op {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) :
                                      theorem NNReal.dist_eq (a : NNReal) (b : NNReal) :
                                      dist a b = |a - b|
                                      theorem NNReal.nndist_eq (a : NNReal) (b : NNReal) :
                                      nndist a b = max (a - b) (b - a)
                                      @[simp]
                                      @[simp]
                                      theorem NNReal.le_add_nndist (a : NNReal) (b : NNReal) :
                                      a b + nndist a b
                                      Equations
                                      theorem ULift.dist_eq {β : Type v} [PseudoMetricSpace β] (x : ULift.{u_3, v} β) (y : ULift.{u_3, v} β) :
                                      dist x y = dist x.down y.down
                                      theorem ULift.nndist_eq {β : Type v} [PseudoMetricSpace β] (x : ULift.{u_3, v} β) (y : ULift.{u_3, v} β) :
                                      nndist x y = nndist x.down y.down
                                      @[simp]
                                      theorem ULift.dist_up_up {β : Type v} [PseudoMetricSpace β] (x : β) (y : β) :
                                      dist { down := x } { down := y } = dist x y
                                      @[simp]
                                      theorem ULift.nndist_up_up {β : Type v} [PseudoMetricSpace β] (x : β) (y : β) :
                                      nndist { down := x } { down := y } = nndist x y
                                      Equations
                                      theorem Prod.dist_eq {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {x : α × β} {y : α × β} :
                                      dist x y = max (dist x.1 y.1) (dist x.2 y.2)
                                      @[simp]
                                      theorem dist_prod_same_left {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {x : α} {y₁ : β} {y₂ : β} :
                                      dist (x, y₁) (x, y₂) = dist y₁ y₂
                                      @[simp]
                                      theorem dist_prod_same_right {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {x₁ : α} {x₂ : α} {y : β} :
                                      dist (x₁, y) (x₂, y) = dist x₁ x₂
                                      theorem ball_prod_same {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (x : α) (y : β) (r : ) :
                                      theorem closedBall_prod_same {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (x : α) (y : β) (r : ) :
                                      theorem dist_dist_dist_le_left {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) :
                                      dist (dist x z) (dist y z) dist x y
                                      theorem dist_dist_dist_le_right {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) :
                                      dist (dist x y) (dist x z) dist y z
                                      theorem dist_dist_dist_le {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (x' : α) (y' : α) :
                                      dist (dist x y) (dist x' y') dist x x' + dist y y'
                                      theorem uniformContinuous_dist {α : Type u} [PseudoMetricSpace α] :
                                      UniformContinuous fun (p : α × α) => dist p.1 p.2
                                      theorem UniformContinuous.dist {α : Type u} {β : Type v} [PseudoMetricSpace α] [UniformSpace β] {f : βα} {g : βα} (hf : UniformContinuous f) (hg : UniformContinuous g) :
                                      UniformContinuous fun (b : β) => dist (f b) (g b)
                                      theorem continuous_dist {α : Type u} [PseudoMetricSpace α] :
                                      Continuous fun (p : α × α) => dist p.1 p.2
                                      theorem Continuous.dist {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : βα} {g : βα} (hf : Continuous f) (hg : Continuous g) :
                                      Continuous fun (b : β) => dist (f b) (g b)
                                      theorem Filter.Tendsto.dist {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : βα} {g : βα} {x : Filter β} {a : α} {b : α} (hf : Filter.Tendsto f x (nhds a)) (hg : Filter.Tendsto g x (nhds b)) :
                                      Filter.Tendsto (fun (x : β) => dist (f x) (g x)) x (nhds (dist a b))
                                      theorem nhds_comap_dist {α : Type u} [PseudoMetricSpace α] (a : α) :
                                      Filter.comap (fun (x : α) => dist x a) (nhds 0) = nhds a
                                      theorem tendsto_iff_dist_tendsto_zero {α : 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)
                                      theorem continuous_iff_continuous_dist {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : βα} :
                                      Continuous f Continuous fun (x : β × β) => dist (f x.1) (f x.2)
                                      theorem uniformContinuous_nndist {α : Type u} [PseudoMetricSpace α] :
                                      UniformContinuous fun (p : α × α) => nndist p.1 p.2
                                      theorem UniformContinuous.nndist {α : Type u} {β : Type v} [PseudoMetricSpace α] [UniformSpace β] {f : βα} {g : βα} (hf : UniformContinuous f) (hg : UniformContinuous g) :
                                      UniformContinuous fun (b : β) => nndist (f b) (g b)
                                      theorem continuous_nndist {α : Type u} [PseudoMetricSpace α] :
                                      Continuous fun (p : α × α) => nndist p.1 p.2
                                      theorem Continuous.nndist {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : βα} {g : βα} (hf : Continuous f) (hg : Continuous g) :
                                      Continuous fun (b : β) => nndist (f b) (g b)
                                      theorem Filter.Tendsto.nndist {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : βα} {g : βα} {x : Filter β} {a : α} {b : α} (hf : Filter.Tendsto f x (nhds a)) (hg : Filter.Tendsto g x (nhds b)) :
                                      Filter.Tendsto (fun (x : β) => nndist (f x) (g x)) x (nhds (nndist a b))
                                      theorem Metric.isClosed_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } :
                                      theorem Metric.isClosed_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } :
                                      @[simp]
                                      @[simp]
                                      theorem Metric.closure_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {ε : } :
                                      theorem Metric.mem_closure_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} {a : α} :
                                      a closure s ε > 0, ∃ b ∈ s, dist a b < ε

                                      ε-characterization of the closure in pseudometric spaces

                                      theorem Metric.mem_closure_range_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] {e : βα} {a : α} :
                                      a closure (Set.range e) ε > 0, ∃ (k : β), dist a (e k) < ε
                                      theorem Metric.mem_closure_range_iff_nat {α : Type u} {β : Type v} [PseudoMetricSpace α] {e : βα} {a : α} :
                                      a closure (Set.range e) ∀ (n : ), ∃ (k : β), dist a (e k) < 1 / (n + 1)
                                      theorem Metric.mem_of_closed' {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : IsClosed s) {a : α} :
                                      a s ε > 0, ∃ b ∈ s, dist a b < ε
                                      theorem Metric.dense_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} :
                                      Dense s ∀ (x : α), r > 0, Set.Nonempty (Metric.ball x r s)
                                      theorem Metric.denseRange_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : βα} :
                                      DenseRange f ∀ (x : α), r > 0, ∃ (y : β), dist x (f y) < r

                                      The preimage of a separable set by an inducing map is separable.

                                      theorem ContinuousOn.isSeparable_image {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : αβ} {s : Set α} (hf : ContinuousOn f s) (hs : TopologicalSpace.IsSeparable s) :

                                      If a map is continuous on a separable set s, then the image of s is also separable.

                                      A compact set is separable.

                                      instance pseudoMetricSpacePi {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] :
                                      PseudoMetricSpace ((b : β) → π b)

                                      A finite product of pseudometric spaces is a pseudometric space, with the sup distance.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      theorem nndist_pi_def {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (f : (b : β) → π b) (g : (b : β) → π b) :
                                      nndist f g = Finset.sup Finset.univ fun (b : β) => nndist (f b) (g b)
                                      theorem dist_pi_def {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (f : (b : β) → π b) (g : (b : β) → π b) :
                                      dist f g = (Finset.sup Finset.univ fun (b : β) => nndist (f b) (g b))
                                      theorem nndist_pi_le_iff {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : NNReal} :
                                      nndist f g r ∀ (b : β), nndist (f b) (g b) r
                                      theorem nndist_pi_lt_iff {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : NNReal} (hr : 0 < r) :
                                      nndist f g < r ∀ (b : β), nndist (f b) (g b) < r
                                      theorem nndist_pi_eq_iff {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : NNReal} (hr : 0 < r) :
                                      nndist f g = r (∃ (i : β), nndist (f i) (g i) = r) ∀ (b : β), nndist (f b) (g b) r
                                      theorem dist_pi_lt_iff {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : } (hr : 0 < r) :
                                      dist f g < r ∀ (b : β), dist (f b) (g b) < r
                                      theorem dist_pi_le_iff {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : } (hr : 0 r) :
                                      dist f g r ∀ (b : β), dist (f b) (g b) r
                                      theorem dist_pi_eq_iff {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : } (hr : 0 < r) :
                                      dist f g = r (∃ (i : β), dist (f i) (g i) = r) ∀ (b : β), dist (f b) (g b) r
                                      theorem dist_pi_le_iff' {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] [Nonempty β] {f : (b : β) → π b} {g : (b : β) → π b} {r : } :
                                      dist f g r ∀ (b : β), dist (f b) (g b) r
                                      theorem dist_pi_const_le {α : Type u} {β : Type v} [PseudoMetricSpace α] [Fintype β] (a : α) (b : α) :
                                      (dist (fun (x : β) => a) fun (x : β) => b) dist a b
                                      theorem nndist_pi_const_le {α : Type u} {β : Type v} [PseudoMetricSpace α] [Fintype β] (a : α) (b : α) :
                                      (nndist (fun (x : β) => a) fun (x : β) => b) nndist a b
                                      @[simp]
                                      theorem dist_pi_const {α : Type u} {β : Type v} [PseudoMetricSpace α] [Fintype β] [Nonempty β] (a : α) (b : α) :
                                      (dist (fun (x : β) => a) fun (x : β) => b) = dist a b
                                      @[simp]
                                      theorem nndist_pi_const {α : Type u} {β : Type v} [PseudoMetricSpace α] [Fintype β] [Nonempty β] (a : α) (b : α) :
                                      (nndist (fun (x : β) => a) fun (x : β) => b) = nndist a b
                                      theorem nndist_le_pi_nndist {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (f : (b : β) → π b) (g : (b : β) → π b) (b : β) :
                                      nndist (f b) (g b) nndist f g
                                      theorem dist_le_pi_dist {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (f : (b : β) → π b) (g : (b : β) → π b) (b : β) :
                                      dist (f b) (g b) dist f g
                                      theorem ball_pi {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (x : (b : β) → π b) {r : } (hr : 0 < r) :
                                      Metric.ball x r = Set.pi Set.univ fun (b : β) => Metric.ball (x b) r

                                      An open ball in a product space is a product of open balls. See also ball_pi' for a version assuming Nonempty β instead of 0 < r.

                                      theorem ball_pi' {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] [Nonempty β] (x : (b : β) → π b) (r : ) :
                                      Metric.ball x r = Set.pi Set.univ fun (b : β) => Metric.ball (x b) r

                                      An open ball in a product space is a product of open balls. See also ball_pi for a version assuming 0 < r instead of Nonempty β.

                                      theorem closedBall_pi {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (x : (b : β) → π b) {r : } (hr : 0 r) :
                                      Metric.closedBall x r = Set.pi Set.univ fun (b : β) => Metric.closedBall (x b) r

                                      A closed ball in a product space is a product of closed balls. See also closedBall_pi' for a version assuming Nonempty β instead of 0 ≤ r.

                                      theorem closedBall_pi' {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] [Nonempty β] (x : (b : β) → π b) (r : ) :
                                      Metric.closedBall x r = Set.pi Set.univ fun (b : β) => Metric.closedBall (x b) r

                                      A closed ball in a product space is a product of closed balls. See also closedBall_pi for a version assuming 0 ≤ r instead of Nonempty β.

                                      theorem sphere_pi {β : Type v} {π : βType u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (x : (b : β) → π b) {r : } (h : 0 < r Nonempty β) :

                                      A sphere in a product space is a union of spheres on each component restricted to the closed ball.

                                      @[simp]
                                      theorem Fin.nndist_insertNth_insertNth {n : } {α : Fin (n + 1)Type u_4} [(i : Fin (n + 1)) → PseudoMetricSpace (α i)] (i : Fin (n + 1)) (x : α i) (y : α i) (f : (j : Fin n) → α (Fin.succAbove i j)) (g : (j : Fin n) → α (Fin.succAbove i j)) :
                                      nndist (Fin.insertNth i x f) (Fin.insertNth i y g) = max (nndist x y) (nndist f g)
                                      @[simp]
                                      theorem Fin.dist_insertNth_insertNth {n : } {α : Fin (n + 1)Type u_4} [(i : Fin (n + 1)) → PseudoMetricSpace (α i)] (i : Fin (n + 1)) (x : α i) (y : α i) (f : (j : Fin n) → α (Fin.succAbove i j)) (g : (j : Fin n) → α (Fin.succAbove i j)) :
                                      dist (Fin.insertNth i x f) (Fin.insertNth i y g) = max (dist x y) (dist f g)
                                      theorem Real.dist_le_of_mem_pi_Icc {β : Type v} [Fintype β] {x : β} {y : β} {x' : β} {y' : β} (hx : x Set.Icc x' y') (hy : y Set.Icc x' y') :
                                      dist x y dist x' y'
                                      theorem finite_cover_balls_of_compact {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : IsCompact s) {e : } (he : 0 < e) :
                                      ∃ t ⊆ s, Set.Finite t s ⋃ x ∈ t, Metric.ball x e

                                      Any compact set in a pseudometric space can be covered by finitely many balls of a given positive radius

                                      theorem IsCompact.finite_cover_balls {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : IsCompact s) {e : } (he : 0 < e) :
                                      ∃ t ⊆ s, Set.Finite t s ⋃ x ∈ t, Metric.ball x e

                                      Alias of finite_cover_balls_of_compact.


                                      Any compact set in a pseudometric space can be covered by finitely many balls of a given positive radius

                                      theorem Metric.secondCountable_of_almost_dense_set {α : Type u} [PseudoMetricSpace α] (H : ε > 0, ∃ (s : Set α), Set.Countable s ∀ (x : α), ∃ y ∈ s, dist x y ε) :

                                      A pseudometric space is second countable if, for every ε > 0, there is a countable set which is ε-dense.

                                      theorem lebesgue_number_lemma_of_metric {α : Type u} [PseudoMetricSpace α] {s : Set α} {ι : Sort u_3} {c : ιSet α} (hs : IsCompact s) (hc₁ : ∀ (i : ι), IsOpen (c i)) (hc₂ : s ⋃ (i : ι), c i) :
                                      ∃ δ > 0, xs, ∃ (i : ι), Metric.ball x δ c i
                                      theorem lebesgue_number_lemma_of_metric_sUnion {α : Type u} [PseudoMetricSpace α] {s : Set α} {c : Set (Set α)} (hs : IsCompact s) (hc₁ : tc, IsOpen t) (hc₂ : s ⋃₀ c) :
                                      ∃ δ > 0, xs, ∃ t ∈ c, Metric.ball x δ t