Revision #1403 → #1843 · back to history
modifiedMetric spacea87c2baa0cba
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Definition","snippet":"Formally, a metric space is an ordered pair"},{"type":"math_alttext","value":"{\\displaystyle d\\,\\colon M\\times M\\to \\mathbb {R} }"}] | — |
modifiedDistance from a point to itself is zeroed668fd3b419
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Definition","snippet":"The distance from a point to itself is zero"},{"type":"math_alttext","value":"{\\displaystyle d(x,x)=0}"}] | — |
| label | Identity of indiscernibles axiom | Distance from a point to itself is zero |
| mathlib.decl | eq_of_dist_eq_zero | dist_self |
| mathlib.module | Mathlib.Topology.MetricSpace.Defs | Mathlib.Topology.MetricSpace.Pseudo.Defs |
| note | The field/theorem `eq_of_dist_eq_zero` and `dist_eq_zero` give exactly this axiom (combined with `dist_self`). | `dist_self : dist x x = 0` is exactly this axiom. |
| provenance | ai | ai-moderated |
modifiedPositivity axiom4d007cf87e1e
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Definition","snippet":"(Positivity) The distance between two distinct points is always positive"},{"type":"math_alttext","value":"{\\displaystyle {\\text{If }}x\\neq y{\\text{, then }}d(x,y)>0}"}] | — |
modifiedSymmetry axiom9d3c68ab3a6e
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Definition","snippet":"the distance from x to y is always the same as the distance from y to x"},{"type":"math_alttext","value":"{\\displaystyle d(x,y)=d(y,x)}"}] | — |
modifiedTriangle inequality axiomd2646e3667c8
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Definition","snippet":"The triangle inequality holds"},{"type":"math_alttext","value":"{\\displaystyle d(x,z)\\leq d(x,y)+d(y,z)}"}] | — |
addedHamming distancec3e5776c359d
modifiedEuclidean distancee116daef0ec8
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Metrics on Euclidean spaces","snippet":"The Euclidean distance familiar from school mathematics"},{"type":"math_alttext","value":"{\\displaystyle d_{2}((x_{1},y_{1}),(x_{2},y_{2}))={\\sqrt {(x_{2}-x_{1})^{2}+(y_{2}-y_{1})^{2}}}.}"}] | — |
| note | `EuclideanSpace 𝕜 n := PiLp 2 (n → 𝕜)` with `dist x y = √(∑ i, dist (x i) (y i) ^ 2)` formalizes the Euclidean distance. | `EuclideanSpace 𝕜 n` with `dist x y = √(∑ i, dist (x i) (y i) ^ 2)` formalizes the Euclidean distance. |
modifiedTaxicab/Manhattan distance81939607b1d8
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Metrics on Euclidean spaces","snippet":"The taxicab or Manhattan distance is defined by"},{"type":"math_alttext","value":"{\\displaystyle d_{1}((x_{1},y_{1}),(x_{2},y_{2}))=|x_{2}-x_{1}|+|y_{2}-y_{1}|}"}] | — |
| mathlib.decl | PiLp.prod_dist_eq_of_L1 | WithLp.prod_dist_eq_of_L1 |
| note | `WithLp 1 (α × β)` and `PiLp 1` give the L¹/Manhattan distance via `prod_dist_eq_of_L1` and its `PiLp` analogues. | `WithLp 1 (α × β)` carries the L¹/Manhattan distance with `WithLp.prod_dist_eq_of_L1 : dist x y = dist x.fst y.fst + dist x.snd y.snd`. |
modifiedChebyshev distance761b1b285cb4
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Metrics on Euclidean spaces","snippet":"or Chebyshev distance is defined by"},{"type":"math_alttext","value":"{\\displaystyle d_{\\infty }((x_{1},y_{1}),(x_{2},y_{2}))=\\max\\{|x_{2}-x_{1}|,|y_{2}-y_{1}|\\}.}"}] | — |
modifiedEquivalence of Euclidean, taxicab, Chebyshev metrics52377bac7858
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Metrics on Euclidean spaces","snippet":"This observation can be quantified with the formula"},{"type":"math_alttext","value":"{\\displaystyle d_{\\infty }(p,q)\\leq d_{2}(p,q)\\leq d_{1}(p,q)\\leq 2d_{\\infty }(p,q),}"},{"type":"math_alttext","value":"{\\displaystyle d_{\\alpha }((x_{1},y_{1}),(x_{2},y_{2}))=\\left(\\vert x_{2}-x_{1}\\vert ^{\\alpha }+\\vert y_{2}-y_{1}\\vert ^{\\alpha }\\right)^{1/\\alpha }.}"}] | — |
| note | Mathlib has individual `PiLp.norm_eq_*` and `Pi.norm_def` lemmas relating L^p norms, but no single statement quantifying the equivalence as in the article. | Mathlib has individual `PiLp.norm_eq_*` lemmas relating L^p norms but no single statement quantifying the Lᵖ equivalence as in the article. |
modifiedDiscrete metric84b723d003c8
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Metrics on Euclidean spaces","snippet":"In this discrete metric , all distinct points are 1 unit apart"},{"type":"math_alttext","value":"{\\displaystyle d(p,q)={\\begin{cases}0,&{\\text{if }}p=q,\\\\1,&{\\text{otherwise.}}\\end{cases}}}"}] | — |
| note | Mathlib has `DiscreteTopology` and `DiscreteTopology.of_forall_le_dist`, but no canonical `MetricSpace` instance defining the 0/1 discrete metric on an arbitrary type. | Mathlib has `DiscreteTopology` but no canonical `MetricSpace` instance providing the 0/1 discrete metric on an arbitrary type. |
modifiedInduced metric on a subspaceb956c2633d72
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Subspaces","snippet":"the induced metric on A is a function"},{"type":"math_alttext","value":"{\\displaystyle d_{A}(x,y)=d(x,y).}"}] | — |
| note | `MetricSpace.induced` (and `Subtype.metricSpace`) pulls back a metric along an injection, giving the induced subspace metric. | `MetricSpace.induced` pulls back a metric along an injection, giving the induced subspace metric. |
modifiedOpen ballbf5d737bc3f8
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"The topology of a metric space","snippet":"the open ball of radius r around x is defined to be the set of points that are strictly less than distance r from x"},{"type":"math_alttext","value":"{\\displaystyle B_{r}(x)=\\{y\\in M:d(x,y)<r\\}.}"}] | — |
modifiedNeighborhood06ae0d4402b7
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"The topology of a metric space","snippet":"is a neighborhood of x (informally, it contains all points \"close enough\" to x )"},{"type":"math_alttext","value":"{\\displaystyle B_{r}(x)=\\{y\\in M:d(x,y)<r\\}.}"}] | — |
modifiedMetrizable spacee78719d21751
| Field | From #1403 | To #1843 |
|---|
| note | `MetrizableSpace` (and `PseudoMetrizableSpace`) classes encode metrizability of a topological space. | `MetrizableSpace` encodes metrizability of a topological space. |
modifiedConvergence in Euclidean space7eada1accc86
| Field | From #1403 | To #1843 |
|---|
| note | Convergence is characterized via `Metric.tendsto_atTop` / `Metric.tendsto_nhds` (ε–N form). | Convergence is characterized via `Metric.tendsto_atTop` in ε–N form. |
modifiedConvergence in a topological space8716903a4c2b
| Field | From #1403 | To #1843 |
|---|
| mathlib.module | Mathlib.Order.Filter.Tendsto | Mathlib.Order.Filter.Defs |
modifiedConvergent sequences are Cauchyfce8f50633a5
| Field | From #1403 | To #1843 |
|---|
| note | `Tendsto.cauchySeq` (referenced as `tendsto_const_nhds.cauchySeq` etc.) shows convergent sequences are Cauchy. | `Filter.Tendsto.cauchySeq` shows a convergent sequence is Cauchy. |
modifiedCompletion6588adbaf4ee
| Field | From #1403 | To #1843 |
|---|
| mathlib.module | Mathlib.Topology.MetricSpace.Completion | Mathlib.Topology.UniformSpace.Completion |
addedp-adic numbers as completion of the rationals92521dc16018
modifiedBounded metric spacee0a98643ab18
| Field | From #1403 | To #1843 |
|---|
| note | `Bornology.IsBounded` together with `Metric.isBounded_iff_subset_closedBall` characterizes bounded sets in metric spaces. | `Bornology.IsBounded` with `Metric.isBounded_iff_subset_closedBall` characterizes bounded sets in metric spaces. |
modifiedCompact metric space (equivalent definitions)8f6e0a82266d
| Field | From #1403 | To #1843 |
|---|
| mathlib.decl | Metric.isCompact_iff_totallyBounded_isComplete | isCompact_iff_totallyBounded_isComplete |
| mathlib.module | Mathlib.Topology.MetricSpace.Cauchy | Mathlib.Topology.UniformSpace.Cauchy |
| note | `isCompact_iff_totallyBounded_isComplete` and `Metric.isSeqCompact_iff_isCompact` give the standard equivalences. | `isCompact_iff_totallyBounded_isComplete` gives the standard equivalence; sequential-compactness equivalences also exist for metric spaces. |
modifiedClosed interval is compact184c7c1f8f46
| Field | From #1403 | To #1843 |
|---|
| note | `isCompact_Icc` shows closed intervals in linearly-ordered topological spaces are compact. | `isCompact_Icc` (exported from `CompactIccSpace`) shows closed intervals in linearly-ordered topological spaces are compact. |
modifiedLebesgue's number lemmacccbee0ab432
| Field | From #1403 | To #1843 |
|---|
| note | `lebesgue_number_lemma` (and `lebesgue_number_lemma_of_metric`) state exactly this result. | `lebesgue_number_lemma` states exactly this result. |
modifiedDistance-preserving function43906c6b74d4
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Isometries","snippet":"is distance-preserving"},{"type":"math_alttext","value":"{\\displaystyle d_{2}(f(x),f(y))=d_{1}(x,y).}"}] | — |
modifiedDistance-preserving functions are injectivea7fb2e8aac0e
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Isometries","snippet":"It follows from the metric space axioms that a distance-preserving function is injective"},{"type":"math_alttext","value":"{\\displaystyle f(x,y)=(x+y,x-y).}"}] | — |
| note | `Isometry.injective` directly proves this (on emetric spaces). | `Isometry.injective` directly proves this on emetric spaces. |
modifiedIsometry2ec20186ae6b
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Isometries","snippet":"A bijective distance-preserving function is called an isometry"},{"type":"math_alttext","value":"{\\displaystyle f(x,y)=(x+y,x-y).}"}] | — |
| note | `IsometryEquiv` (denoted `α ≃ᵢ β`) is the bundled bijective isometry. | `IsometryEquiv` (`α ≃ᵢ β`) is the bundled bijective isometry. |
modifiedIsometric spaces2a3fcbcde46b
| Field | From #1403 | To #1843 |
|---|
| note | The existence of an `IsometryEquiv` between spaces is Mathlib's way of saying they are isometric. | Existence of an `IsometryEquiv` between spaces is Mathlib's way of saying they are isometric. |
modifiedUniformly continuous mapda24d2c8178c
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Uniformly continuous maps","snippet":"is uniformly continuous if for every real number ε > 0 there exists δ > 0"},{"type":"math_alttext","value":"{\\displaystyle d_{2}(f(x),f(y))<\\varepsilon .}"}] | — |
modifiedLipschitz map84e3b76a4051
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Lipschitz maps and contractions","snippet":"A Lipschitz map is one that stretches distances by at most a bounded factor"},{"type":"math_alttext","value":"{\\displaystyle d_{2}(f(x),f(y))\\leq Kd_{1}(x,y)\\quad {\\text{for all}}\\quad x,y\\in M_{1}.}"}] | — |
| note | `LipschitzWith K f` and `lipschitzWith_iff_dist_le_mul` formalize Lipschitz maps. | `LipschitzWith K f` (with `lipschitzWith_iff_dist_le_mul`) formalizes Lipschitz maps. |
modifiedRectifiable iff has Lipschitz reparametrizationd70a87e68481
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Lipschitz maps and contractions","snippet":"a curve in a metric space is rectifiable (has finite length) if and only if it has a Lipschitz reparametrization"},{"type":"math_alttext","value":"{\\displaystyle d_{2}(f(x),f(y))\\leq Kd_{1}(x,y)\\quad {\\text{for all}}\\quad x,y\\in M_{1}.}"}] | — |
| note | Mathlib has `eVariationOn`/`BoundedVariationOn`, but I found no statement equating finite length with admitting a Lipschitz reparametrization. | Mathlib has `eVariationOn`/`BoundedVariationOn`, but no statement equating finite length with admitting a Lipschitz reparametrization. |
modifiedMetric map (nonexpanding)4d3098d99cf3
| Field | From #1403 | To #1843 |
|---|
| note | Nonexpanding maps are `LipschitzWith 1 f` (no dedicated `NonexpandingMap` notion exists). | Nonexpanding maps are `LipschitzWith 1 f`; no dedicated `NonexpandingMap` notion exists. |
modifiedContractionbf31aa1a3fa0
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Lipschitz maps and contractions","snippet":"A K -Lipschitz map for K < 1 is called a contraction"},{"type":"math_alttext","value":"{\\displaystyle d(f(x),f(y))<d(x,y)\\quad {\\mbox{for all}}\\quad x\\neq y\\in M_{1}.}"}] | — |
modifiedBanach fixed-point theorem1f62862b0d3c
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Lipschitz maps and contractions","snippet":"The Banach fixed-point theorem states that if M is a complete metric space"},{"type":"math_alttext","value":"{\\displaystyle d(f(x),f(y))<d(x,y)\\quad {\\mbox{for all}}\\quad x\\neq y\\in M_{1}.}"}] | — |
modifiedQuasi-isometric embeddingf81c9019484c
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Quasi-isometries","snippet":"is a quasi-isometric embedding if there exist constants A ≥ 1 and B ≥ 0"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {1}{A}}d_{2}(f(x),f(y))-B\\leq d_{1}(x,y)\\leq Ad_{2}(f(x),f(y))+B\\quad {\\text{ for all }}\\quad x,y\\in M_{1}.}"}] | — |
| note | Grep for `QuasiIsometry`/`quasiIsometry` returns no matches in Mathlib. | Grep for `QuasiIsometry` returns no matches in Mathlib. |
modifiedQuasi-isometry9b99efd589c8
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Quasi-isometries","snippet":"It is a quasi-isometry if in addition it is quasi-surjective"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {1}{A}}d_{2}(f(x),f(y))-B\\leq d_{1}(x,y)\\leq Ad_{2}(f(x),f(y))+B\\quad {\\text{ for all }}\\quad x,y\\in M_{1}.}"}] | — |
modifiedŠvarc–Milnor lemmaf709a09a6c54
| Field | From #1403 | To #1843 |
|---|
| note | No file mentions Švarc–Milnor; the prerequisite quasi-isometry notion is also absent. | No file mentions Švarc–Milnor; the prerequisite quasi-isometry notion is absent. |
modifiedBilipschitz homeomorphic0dba681bec51
| Field | From #1403 | To #1843 |
|---|
| note | Mathlib expresses bilipschitz equivalence via `LipschitzWith` on both directions, but there is no dedicated bundled `Bilipschitz` structure. | Mathlib expresses bilipschitz equivalence via `LipschitzWith` on both directions; no dedicated bundled `Bilipschitz` structure. |
modifiedMetric induced by a normc6baa2d346ff
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Normed vector spaces","snippet":"Any normed vector space can be equipped with a metric in which the distance between two vectors x and y is given by"},{"type":"math_alttext","value":"{\\displaystyle d(x,y):=\\lVert x-y\\rVert .}"}] | — |
| mathlib.module | Mathlib.Analysis.Normed.Group.Defs | Mathlib.Analysis.Normed.Group.Basic |
modifiedTranslation-invariant and homogeneous metric comes from a norm3604c7e6f7ea
| Field | From #1403 | To #1843 |
|---|
| note | I found no Mathlib statement constructing a norm from a translation-invariant, homogeneous metric on a vector space. | No Mathlib statement constructs a norm from a translation-invariant, homogeneous metric on a vector space. |
addedKuratowski embeddinge22c81f5b36b
modifiedLinear maps continuous iff Lipschitzfac4f2e0d436
| Field | From #1403 | To #1843 |
|---|
| mathlib.decl | LinearMap.continuous_of_bound | continuous_of_linear_of_bound |
| note | `continuous_of_linear_of_bound` and `ContinuousLinearMap.lipschitz` together formalize that a linear map is continuous iff Lipschitz. | `continuous_of_linear_of_bound` together with `ContinuousLinearMap.lipschitz` formalize that a linear map is continuous iff Lipschitz. |
modifiedCurve and its lengtha2b9b048fe8b
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Length spaces","snippet":"A curve in a metric space ( M , d ) is a continuous function"},{"type":"math_alttext","value":"{\\displaystyle L(\\gamma )=\\sup _{0=x_{0}<x_{1}<\\cdots <x_{n}=T}\\left\\{\\sum _{k=1}^{n}d(\\gamma (x_{k-1}),\\gamma (x_{k}))\\right\\}.}"}] | — |
| mathlib.module | Mathlib.Analysis.BoundedVariation | Mathlib.Topology.EMetricSpace.BoundedVariation |
modifiedRectifiable curvea85bb65d4818
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Length spaces","snippet":"a curve of finite length is called rectifiable"},{"type":"math_alttext","value":"{\\displaystyle L(\\gamma )=\\sup _{0=x_{0}<x_{1}<\\cdots <x_{n}=T}\\left\\{\\sum _{k=1}^{n}d(\\gamma (x_{k-1}),\\gamma (x_{k}))\\right\\}.}"}] | — |
| mathlib.module | Mathlib.Analysis.BoundedVariation | Mathlib.Topology.EMetricSpace.BoundedVariation |
modifiedGeodesic31b417f3247c
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Length spaces","snippet":"After reparametrization by arc length"},{"type":"math_alttext","value":"{\\displaystyle L(\\gamma )=\\sup _{0=x_{0}<x_{1}<\\cdots <x_{n}=T}\\left\\{\\sum _{k=1}^{n}d(\\gamma (x_{k-1}),\\gamma (x_{k}))\\right\\}.}"}] | — |
| note | Riemannian-manifold geodesics appear in Mathlib (e.g. `PathELength`), but no general metric-space `Geodesic` definition exists. | Riemannian-manifold geodesics appear in Mathlib, but no general metric-space `Geodesic` definition exists. |
modifiedGeodesic metric space737c29270f63
| Field | From #1403 | To #1843 |
|---|
| note | No `GeodesicSpace`/`geodesic_space` class found in Mathlib. | No `GeodesicSpace` class found in Mathlib. |
modifiedRiemannian manifold and length of a pathcb66d77c1e2a
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Riemannian manifolds","snippet":"A Riemannian manifold is a space equipped with a Riemannian metric tensor"},{"type":"math_alttext","value":"{\\displaystyle L(\\gamma )=\\int _{0}^{T}|{\\dot {\\gamma }}(t)|dt.}"}] | — |
| mathlib.match_kind | exact | invocation |
| mathlib.module | Mathlib.Geometry.Manifold.Riemannian.Basic | Mathlib.Geometry.Manifold.IsManifold.Basic |
| note | Mathlib's `Mathlib.Geometry.Manifold.Riemannian` develops Riemannian manifolds with a Riemannian metric and `PathELength` for path length. | Mathlib's `Mathlib.Geometry.Manifold.Riemannian` develops Riemannian manifolds (built on `IsManifold`) with a Riemannian metric and `PathELength` for path length. |
modifiedWord metricc238cf6888f1
| Field | From #1403 | To #1843 |
|---|
| note | Grep finds no `wordMetric`/`word_metric` and no Cayley-graph metric construction in Mathlib. | No `wordMetric` and no Cayley-graph metric construction in Mathlib. |
modifiedUniform (supremum) metric on bounded functionsdf681d385546
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Distances between mathematical objects","snippet":"This metric is called the uniform metric or supremum metric"},{"type":"math_alttext","value":"{\\displaystyle d(f,g)=\\sup _{x\\in X}d(f(x),g(x)).}"}] | — |
modifiedCompleteness of bounded function spacec349834d4231
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Distances between mathematical objects","snippet":"If M is complete, then this function space is complete as well"},{"type":"math_alttext","value":"{\\displaystyle d(f,g)=\\sup _{x\\in X}d(f(x),g(x)).}"}] | — |
addedLevenshtein distance6f2012bf2fef
modifiedDistance from a point to a setccf16b38c8c6
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Hausdorff and Gromov–Hausdorff distance","snippet":"The distance from S to a point x of M is, informally, the distance from x to the closest point of S"},{"type":"math_alttext","value":"{\\displaystyle d(x,S)=\\inf\\{d(x,s):s\\in S\\}.}"},{"type":"math_alttext","value":"{\\displaystyle d(x,S)\\leq d(x,y)+d(y,S),}"}] | — |
modifiedDistance zero iff in closure4f02fa066a13
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Hausdorff and Gromov–Hausdorff distance","snippet":"if and only if x belongs to the closure of S"},{"type":"math_alttext","value":"{\\displaystyle d(x,S)=\\inf\\{d(x,s):s\\in S\\}.}"},{"type":"math_alttext","value":"{\\displaystyle d(x,S)\\leq d(x,y)+d(y,S),}"}] | — |
modifiedContinuity of distance-to-setbf5942ad5938
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Hausdorff and Gromov–Hausdorff distance","snippet":"and therefore the map"},{"type":"math_alttext","value":"{\\displaystyle d(x,S)=\\inf\\{d(x,s):s\\in S\\}.}"},{"type":"math_alttext","value":"{\\displaystyle d(x,S)\\leq d(x,y)+d(y,S),}"}] | — |
| note | `continuous_infDist_pt` and `uniformContinuous_infDist_pt` show `x ↦ infDist x s` is (uniformly) continuous. | `continuous_infDist_pt` shows `x ↦ infDist x s` is continuous. |
modifiedMetric spaces are completely regularf2618b6f243a
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Hausdorff and Gromov–Hausdorff distance","snippet":"Incidentally, this shows that metric spaces are completely regular"},{"type":"math_alttext","value":"{\\displaystyle d(x,S)=\\inf\\{d(x,s):s\\in S\\}.}"},{"type":"math_alttext","value":"{\\displaystyle d(x,S)\\leq d(x,y)+d(y,S),}"}] | — |
| note | `CompletelyRegularSpace` exists, and metric spaces being T3.5 follows from being `NormalSpace`, but I did not find an explicit `instance CompletelyRegularSpace` for metric spaces. | `CompletelyRegularSpace` exists, and metric spaces being T3.5 follows from being normal, but no explicit `instance CompletelyRegularSpace` for metric spaces was found. |
modifiedHausdorff distancee65f89f9e977
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Hausdorff and Gromov–Hausdorff distance","snippet":"Given two subsets S and T of M , their Hausdorff distance is"},{"type":"math_alttext","value":"{\\displaystyle d_{H}(S,T)=\\max\\{\\sup\\{d(s,T):s\\in S\\},\\sup\\{d(t,S):t\\in T\\}\\}.}"}] | — |
modifiedHausdorff distance is a metric on compact subsets0cedd3e46c10
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Hausdorff and Gromov–Hausdorff distance","snippet":"Thus the Hausdorff distance defines a metric on the set of compact subsets of M"},{"type":"math_alttext","value":"{\\displaystyle d_{H}(S,T)=\\max\\{\\sup\\{d(s,T):s\\in S\\},\\sup\\{d(t,S):t\\in T\\}\\}.}"}] | — |
| mathlib.decl | Metric.NonemptyCompacts.metricSpace | NonemptyCompacts.instMetricSpace |
| note | Mathlib endows `NonemptyCompacts` (and `Closeds`) with a metric/emetric via `hausdorffEDist`. | `NonemptyCompacts.instMetricSpace` endows nonempty compact subsets with the Hausdorff metric. |
modifiedSnowflake of a metric1b57c218abe6
| Field | From #1403 | To #1843 |
|---|
| note | `Mathlib.Topology.MetricSpace.Snowflaking` handles the power-of-d snowflake; the general concave-f version is not stated. | `Snowflaking` formalizes the power-of-d snowflake; the general concave-f version is not stated. |
modifiedTight span52730a1a481c
| Field | From #1403 | To #1843 |
|---|
| note | Grep finds no tight-span / injective-hull construction in Mathlib. | No tight-span / injective-hull construction in Mathlib. |
modifiedProduct metric8ce67cf7c1ad
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Product metric spaces","snippet":"the product metric is defined by"},{"type":"math_alttext","value":"{\\displaystyle d_{\\times }{\\bigl (}(x_{1},\\ldots ,x_{n}),(y_{1},\\ldots ,y_{n}){\\bigr )}=N{\\bigl (}d_{1}(x_{1},y_{1}),\\ldots ,d_{n}(x_{n},y_{n}){\\bigr )},}"}] | — |
modifiedCountable product metric59fc886a3aff
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Product metric spaces","snippet":"a metric on the topological product of countably many metric spaces can be obtained"},{"type":"math_alttext","value":"{\\displaystyle d(x,y)=\\sum _{i=1}^{\\infty }{\\frac {1}{2^{i}}}{\\frac {d_{i}(x_{i},y_{i})}{1+d_{i}(x_{i},y_{i})}}.}"}] | — |
| mathlib.decl | PiNat | PiCountable.metricSpace |
| note | `Mathlib.Topology.MetricSpace.PiNat` constructs a metric on countable products `∀ n, E n` generating the product topology. | `PiCountable.metricSpace` constructs a (non-instance) metric on countable products `∀ i, F i` of metric spaces. |
modifiedUncountable products need not be metrizablef5c79dcd0b5b
| Field | From #1403 | To #1843 |
|---|
| note | I found no explicit non-metrizability result for uncountable products in Mathlib. | No explicit non-metrizability result for uncountable products in Mathlib. |
modifiedQuotient pseudometricc6452752cd44
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Quotient metric spaces","snippet":"then we can endow the quotient set"},{"type":"math_alttext","value":"{\\displaystyle d'([x],[y])=\\inf\\{d(p_{1},q_{1})+d(p_{2},q_{2})+\\dotsb +d(p_{n},q_{n})\\},}"}] | — |
| mathlib.decl | Metric.gluingSpace | — |
| mathlib.match_kind | special_case | — |
| note | Mathlib's `Gluing.lean` constructs quotient (pseudo)metric spaces in the gluing context but no general `Quotient.pseudoMetric` of a setoid. | `Mathlib.Topology.MetricSpace.Gluing` constructs quotient (pseudo)metric spaces in the gluing context, but no general `Quotient.pseudoMetric` of a setoid is defined. |
modifiedExtended metric replaceable by topologically equivalent real-valued metric9b761a713d04
| Field | From #1403 | To #1843 |
|---|
| note | I found no general lemma in Mathlib converting an `EMetricSpace` to a topologically equivalent `MetricSpace`. | No general lemma in Mathlib converts an `EMetricSpace` to a topologically equivalent `MetricSpace`. |
modifiedQuasimetric on the reals19677bcc0e25
| Field | From #1403 | To #1843 |
|---|
| anchors | [{"section":"Quasimetrics","snippet":"A quasimetric on the reals can be defined by setting"},{"type":"math_alttext","value":"{\\displaystyle d(x,y)={\\begin{cases}x-y&{\\text{if }}x\\geq y,\\\\1&{\\text{otherwise.}}\\end{cases}}}"}] | — |