Metric spaces

ClassMetric space#

A metric space is a type endowed with a ℝ-valued distance dist satisfying dist x y = 0 ↔ x = y, commutativity dist x y = dist y x, and the triangle inequality dist x z ≤ dist x y + dist y z.

See pseudometric spaces (PseudoMetricSpace) for the similar class with the dist x y = 0 ↔ x = y assumption weakened to dist x x = 0.

Any metric space is a T1 topological space and a uniform space (see TopologicalSpace, T1Space, UniformSpace), where the topology and uniformity come from the metric.

We make the uniformity/topology part of the data instead of deriving it from the metric. This e.g. ensures that we do not get a diamond when doing [MetricSpace α] [MetricSpace β] : TopologicalSpace (α × β): The product metric and product topology agree, but not definitionally so. See Note [forgetful inheritance].

MetricSpace.{u} (α : Type u) : Type u
Sources
MathlibMetricSpace
Uses 2 · Used by 45
Statement usesBornology · Order
Used byDivergence of the Harmonic Series · Sum of kth powers · Divergence of the Prime Reciprocal Series · Differentiable function between normed vector spaces · Fatou's lemma · \(L^p\) space · Uniform integrability · Absolutely convergent series in Banach spaces · Equivalence of norms in finite dimension · Finite-dimensional normed spaces over complete normed fields are complete · Normed vector space over a normed field · \(p\)-adic number · Riemannian/bundle metric · Kolmogorov's \(0\)-\(1\) law · Stone-Weierstrass theorem · Gromov-Hausdorff space · Heine-Borel theorem (proper metric space version) · Gershgorin circle theorem · Abel's theorem · Besicovitch covering theorem · Dini's theorem · Vitali convergence theorem · Gelfand–Mazur theorem · Krein–Milman theorem · Lebesgue's density theorem · Tietze extension theorem · Dirichlet's approximation theorem · Dirichlet's unit theorem · Ostrowski's theorem · Pentagonal number theorem · Norm · Differentials (linear tangent functions) · Cos (power series expansion of elementary functions) · Log · Sin (power series expansion of elementary functions) · Holomorphic functions · Derivative at a point · Convergence of \(p\)-series for \(p>1\) · Geometric series · Continuity of the sum of a series of functions · Weierstrass trigonometric approximation theorem · Metric structure · Completeness of \(l^2\) · Riesz' lemma (unit-ball characterization of finite dimension) · Finite product of metric spaces

DefinitionBall#

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

Metric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α
Sources
MathlibMetric.ball
Uses 2 · Used by 14
Statement usesBornology · Order
Used byCauchy integral formula · Schwarz lemma · Approximation by convolution · Local existence of integral curves · Stone-Weierstrass theorem · Heine-Borel theorem (proper metric space version) · Borel–Carathéodory theorem · Continuity (Complex-valued series) · Cauchy formulas · Holomorphic stability under uniform convergence · Differentiability of the limit of a sequence of functions · Completeness of R · Limits of sequences · Topology of a metric space

TheoremSequential compactness is equivalent to compactness (Bolzano-Weierstrass)#

A version of Bolzano-Weierstrass: in a (pseudo)metrizable space, a set is compact if and only if it is sequentially compact.

isCompact_iff_isSeqCompact.{u_1} {X : Type u_1} [TopologicalSpace X]
  [TopologicalSpace.PseudoMetrizableSpace X] {s : Set X} : IsCompact s ↔ IsSeqCompact s
Sources
MathlibisCompact_iff_isSeqCompact
Uses 5
Statement usesCompactness in terms of filters · Natural number · Uniform space
Proof usesCauchy sequence · Limit point

TheoremHeine-Borel theorem (proper metric space version)#

The Heine–Borel theorem: In a proper metric space, a set is compact if and only if it is closed and bounded.

Metric.isCompact_iff_isClosed_bounded.{u_2} {α : Type u_2} {s : Set α} [MetricSpace α]
  [ProperSpace α] : IsCompact s ↔ IsClosed s ∧ Bornology.IsBounded s

The 1000+ list (Q253214) also cites FiniteDimensional.proper.

Sources
MathlibMetric.isCompact_iff_isClosed_bounded
Uses 4 · Used by 2
Statement usesCompactness in terms of filters · Metric space
Proof usesBall · Hausdorff space
Used byHeine-Borel theorem (finite-dimensional normed spaces are proper) · Prokhorov's theorem

DefinitionLipschitz continuity#

A function f is Lipschitz continuous with constant K ≥ 0 if for all x, y we have dist (f x) (f y) ≤ K * dist x y.

LipschitzWith.{u, v} {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β]
  (K : NNReal) (f : α → β) : Prop
Sources
MathlibLipschitzWith
Uses 1 · Used by 14
Statement usesReal number
Used byFourier Series · Maximum modulus principle · Schwarz lemma · Conditional expectation · Arzela-Ascoli theorem · Contraction mapping theorem · Monotone convergence theorem (1000+ theorems) · Rademacher's theorem · Tietze extension theorem · Lévy continuity theorem · Slutsky's theorem · Cauchy-Lipschitz Theorem · Completeness of \(l^2\) · Example, the Hilbert basis of trigonometric polynomials

DefinitionHölder continuity#

A function f : X → Y between two PseudoEMetricSpaces is Hölder continuous with constant C : ℝ≥0 and exponent r : ℝ≥0, if edist (f x) (f y) ≤ C * edist x y ^ r for all x y : X.

HolderWith.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y]
  (C r : NNReal) (f : X → Y) : Prop
Sources
MathlibHolderWith
Uses 1
Statement usesReal number

TheoremContraction mapping theorem#

Banach fixed-point theorem, contraction mapping theorem, EMetricSpace version. A contracting map on a complete metric space has a fixed point. We include more conclusions in this theorem to avoid proving them again later.

The main API for this theorem are the functions efixedPoint and fixedPoint, and lemmas about these functions.

ContractingWith.exists_fixedPoint.{u_1} {α : Type u_1} [EMetricSpace α] {K : NNReal} {f : α → α}
  [CompleteSpace α] (hf : ContractingWith K f) (x : α) (hx : edist x (f x) ≠ ⊤) :
  ∃ y,
    Function.IsFixedPt f y ∧
      Filter.Tendsto (fun n => f^[n] x) Filter.atTop (nhds y) ∧
        ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
Sources
MathlibContractingWith.exists_fixedPoint
Uses 4
Statement usesCompleteness · Lipschitz continuity
Proof usesHausdorff space · Sum of a Geometric Series

TheoremBaire theorem#

First Baire theorem: a completely pseudometrizable topological space has Baire property.

BaireSpace.of_completelyPseudoMetrizable.{u_1} {X : Type u_1} [TopologicalSpace X]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace X] : BaireSpace X

The 1000+ list (Q1052678) also cites BaireSpace.of_t2Space_locallyCompactSpace.

Sources
MathlibBaireSpace.of_completelyPseudoMetrizable
Uses 5 · Used by 2
Statement usesBornology · Closure · Completeness · Order
Proof usesSum of a Geometric Series
Used byBanach open mapping theorem · Banach-Steinhaus theorem

TheoremArzela-Ascoli theorem#

Third \(main\) version, with pointwise equicontinuity and range in a compact subset, but without closedness. The closure is then compact.

BoundedContinuousFunction.arzela_ascoli.{u, v} {α : Type u} {β : Type v} [TopologicalSpace α]
  [CompactSpace α] [PseudoMetricSpace β] [T2Space β] (s : Set β) (hs : IsCompact s)
  (A : Set (BoundedContinuousFunction α β))
  (in_s : ∀ (f : BoundedContinuousFunction α β) (x : α), f ∈ A → f x ∈ s)
  (H : Equicontinuous fun x => ⇑↑x) : IsCompact (closure A)
Sources
MathlibBoundedContinuousFunction.arzela_ascoli
Uses 10
Statement usesBornology · Closure · Compactness in terms of filters · Continuous function · Hausdorff space · Order
Proof usesCharacteristic zero · Completeness of spaces of bounded continuous functions · Finite set · Lipschitz continuity

DefinitionHausdorff distance#

The Hausdorff edistance between two sets is the smallest r such that each set is contained in the r-neighborhood of the other one

Metric.hausdorffEDist.{u} {α : Type u} [PseudoEMetricSpace α] (s t : Set α) : ENNReal
Sources
MathlibMetric.hausdorffEDist
Uses 1
Statement usesReal number

DefinitionGromov-Hausdorff space#

The Gromov-Hausdorff space

GromovHausdorff.GHSpace : Type
Sources
MathlibGromovHausdorff.GHSpace
Uses 3
Statement usesCompactness in terms of filters · Infinite sum · Metric space

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.