Revision #2539 → #3740 · back to history
modifiedRationals are not complete (intuitive)779c8ab0626d
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib does not contain a direct statement that the rationals with the standard metric are not a CompleteSpace. The reals are constructed as the Cauchy completion of the rationals, which implicitly relies on this fact. | Mathlib does not contain a direct statement that the rationals with the standard metric are not a CompleteSpace; the reals are constructed as the Cauchy completion of the rationals, which implicitly relies on this fact. |
modifiedCauchy sequence in a metric spacec52a2f17aa3e
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib defines `CauchySeq u` for sequences in uniform spaces. The metric-space epsilon-N characterization is proved as `cauchySeq_iff` in `Mathlib.Topology.MetricSpace.Cauchy`. | Mathlib defines `CauchySeq u` for sequences in uniform spaces; the metric-space epsilon-N characterization is available as `Metric.cauchySeq_iff`. |
modifiedComplete space (equivalent conditions)c9b0cc637df5
| Field | From #2539 | To #3740 |
|---|
| note | The equivalence of the Cauchy-sequence and Cauchy-filter definitions follows from the general theory. `CompleteSpace` requires every Cauchy filter to converge. | The equivalence of the Cauchy-sequence and Cauchy-filter definitions follows from the general theory; `CompleteSpace` requires every Cauchy filter to converge. |
modifiedComplete space — Cauchy sequence conditionfd5ae84cfab3
| Field | From #2539 | To #3740 |
|---|
| note | The Cauchy sequence convergence condition is subsumed by the Cauchy filter formulation of `CompleteSpace`. The equivalence for metric spaces is available via `Metric.complete_of_cauchySeq_tendsto`. | The Cauchy sequence convergence condition is subsumed by the Cauchy filter formulation of `CompleteSpace`; the equivalence for metric spaces is available via `Metric.complete_of_cauchySeq_tendsto`. |
modifiedComplete space — nested closed sets condition (Cantor's intersection theorem)048878b76120
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib proves Cantor's intersection theorem for compact spaces. For complete metric spaces with diameter tending to zero, the result follows from completeness. The compact version is `IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed`. | Mathlib proves Cantor's intersection theorem for compact spaces; the compact version is `IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed`, and the diameter→0 version for complete metric spaces follows. |
modifiedRationals are not complete90c95cf2b9db
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib does not contain a direct statement that the rationals with the standard metric are not a CompleteSpace. The reals are constructed as the Cauchy completion of the rationals (`Data.Real.Basic`), which implicitly relies on this fact. | Mathlib does not contain a direct statement that the rationals with the standard metric are not a CompleteSpace; the reals are constructed as the Cauchy completion of the rationals in `Data.Real.Basic`, which implicitly relies on this fact. |
modifiedOpen interval (0,1) is not completea5521991fd51
| Field | From #2539 | To #3740 |
|---|
| note | There is no explicit Mathlib statement that the open interval (0,1) is not complete. This could be derived from facts about subspaces. | There is no explicit Mathlib statement that the open interval (0,1) is not complete; this could be derived from facts about subspaces. |
modifiedClosed interval [0,1] is complete2b4576241911
| Field | From #2539 | To #3740 |
|---|
| note | The closed interval `Set.Icc 0 1` is a closed subset of the complete space R, so it inherits completeness via `IsClosed.isComplete`. Also `isCompact_Icc` gives compactness, which implies completeness. | The closed interval `Set.Icc 0 1` is a closed subset of the complete space ℝ, so it inherits completeness via `IsClosed.isComplete`; equivalently `isCompact_Icc` gives compactness, which implies completeness. |
modifiedReal numbers and complex numbers are completeb4f67f28fe3a
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib provides `Real.instCompleteSpace : CompleteSpace R` directly. Complex completeness is in `Mathlib.Analysis.Complex.Basic`. | Mathlib provides `Real.instCompleteSpace : CompleteSpace ℝ` directly; complex completeness is in `Mathlib.Analysis.Complex.Basic`. |
modifiedEuclidean space is completebc54e14d1914
| Field | From #2539 | To #3740 |
|---|
| note | Euclidean space `EuclideanSpace R (Fin n)` is a `PiLp` type. Completeness follows from `Pi.complete` (products of complete spaces are complete) and `CompleteSpace R`. | Euclidean space `EuclideanSpace ℝ (Fin n)` is a `PiLp` type; completeness follows from `Pi.complete` (products of complete spaces are complete) and `CompleteSpace ℝ`. |
modifiedBanach space (complete normed vector space)5e1e49116aff
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib does not define a separate `BanachSpace` class. A Banach space is simply a `NormedSpace` that is also `CompleteSpace`. This convention is used throughout `Mathlib.Analysis.Normed`. | Mathlib does not define a separate `BanachSpace` class; a Banach space is simply a `NormedSpace` that is also `CompleteSpace`, a convention used throughout `Mathlib.Analysis.Normed`. |
modifiedC([a,b]) is a Banach space with supremum norm519d5e154ae4
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib proves that bounded continuous functions `a ->b beta` form a `CompleteSpace` when the target is complete. Since [a,b] is compact, every continuous function on it is bounded, so this covers C([a,b]). | Mathlib proves that bounded continuous functions `α →ᵇ β` form a `CompleteSpace` when the target is complete; since [a,b] is compact, every continuous function on it is bounded, so this covers C([a,b]). |
modifiedSupremum norm does not give a norm on C(R)538ee61ea566
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib does not contain an explicit statement that the supremum norm fails to be a norm on C(R) due to unbounded functions. The `BoundedContinuousFunction` type sidesteps this by restricting to bounded functions. | Mathlib does not contain an explicit statement that the supremum norm fails to be a norm on C(ℝ) due to unbounded functions; the `BoundedContinuousFunction` type sidesteps this by restricting to bounded functions. |
modifiedFrechet space14d47e851c6c
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib does not define Frechet spaces as a class. While locally convex spaces and topological vector spaces exist in Mathlib, there is no dedicated Frechet space typeclass. | Mathlib does not define Fréchet spaces as a class; while locally convex spaces and topological vector spaces exist, there is no dedicated Fréchet space typeclass. |
modifiedC(R) is a Frechet space with compact convergence topology591465a045c6
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib does not define Frechet spaces as a class. The topology of compact convergence on C(R) is not formalized in this specific way. | Mathlib does not define Fréchet spaces as a class; the topology of compact convergence on C(ℝ) is not formalized in this specific way. |
modifiedp-adic numbers are complete4c7138d758fb
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib proves `instance : CompleteSpace Q_[p]` in `Mathlib.NumberTheory.Padics.PadicNumbers`. | Mathlib proves `instance : CompleteSpace ℚ_[p]` in `Mathlib.NumberTheory.Padics.PadicNumbers`. |
modifiedSequence space over arbitrary set is completeee4f549aa721
| Field | From #2539 | To #3740 |
|---|
| note | The space of all sequences (functions N -> alpha, or more generally iota -> alpha) inherits completeness from `Pi.complete` when the target space is complete. | The space of all sequences (functions ℕ → α, or more generally ι → α) inherits completeness from `Pi.complete` when the target space is complete. |
modifiedGeodesic manifold (complete Riemannian manifold)310fa64b55a2
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib does not define geodesic manifolds or completeness for Riemannian manifolds. The differential geometry library does not yet reach this level. | Mathlib does not define geodesic manifolds or completeness for Riemannian manifolds; the differential geometry library does not yet reach this level. |
modifiedCompleteness of Riemannian manifolds follows from Hopf-Rinowa94d6db51fba
| Field | From #2539 | To #3740 |
|---|
| note | The Hopf-Rinow theorem is not formalized in Mathlib. | The Hopf–Rinow theorem is not formalized in Mathlib. |
modifiedEvery compact metric space is completebf02b39fcf19
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib proves `IsCompact.isComplete` for any uniform space: a compact set is complete. The global version follows via `isCompact_iff_totallyBounded_isComplete`. | Mathlib proves `IsCompact.isComplete` for any uniform space: a compact set is complete; the global version follows via `isCompact_iff_totallyBounded_isComplete`. |
modifiedA metric space is compact iff complete and totally boundede7e00f232588
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib proves this for general uniform spaces: `isCompact_iff_totallyBounded_isComplete : IsCompact s <-> TotallyBounded s /\ IsComplete s`. | Mathlib proves this for general uniform spaces: `isCompact_iff_totallyBounded_isComplete : IsCompact s ↔ TotallyBounded s ∧ IsComplete s`. |
modifiedHeine-Borel theorem: closed and bounded subspace of R^n is compact1928899d5c26
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib formalizes Heine-Borel via `ProperSpace`, where closed balls are compact. The instance for finite-dimensional normed spaces shows R^n is proper. | Mathlib formalizes Heine-Borel via `ProperSpace`, where closed balls are compact; the instance for finite-dimensional normed spaces shows ℝⁿ is proper. |
modifiedComplete subspace of a metric space is closed08699e137799
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib proves `IsComplete.isClosed` for T0 uniform spaces. Since metric spaces are T0, this gives that complete subspaces are closed. | Mathlib proves `IsComplete.isClosed` for T0 uniform spaces; since metric spaces are T0, this gives that complete subspaces are closed. |
modifiedBounded functions into complete space form a complete space3374fb3c9c19
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib proves that bounded continuous functions form a complete space when the target is complete. This is a special case (continuous bounded rather than all bounded), but the general result follows from `Pi.complete`. | Mathlib proves that bounded continuous functions form a complete space when the target is complete; this is a special case (continuous bounded rather than all bounded), but the general result follows from `Pi.complete`. |
modifiedContinuous bounded functions into complete space form closed subspace182a48201725
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib proves directly that bounded continuous functions `alpha ->b beta` form a `CompleteSpace` when the target is complete, which is equivalent to the continuous bounded functions being a closed subspace of bounded functions. | Mathlib proves directly that bounded continuous functions `α →ᵇ β` form a `CompleteSpace` when the target is complete, which is equivalent to the continuous bounded functions being a closed subspace of bounded functions. |
modifiedBaire category theorem: complete metric space is a Baire space36ca3415f4fa
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib proves that completely pseudometrizable spaces are Baire in `BaireSpace.of_completelyPseudoMetrizable`. This generalizes the result from complete metric spaces to completely (pseudo)metrizable spaces. | Mathlib proves that completely pseudometrizable spaces are Baire in `BaireSpace.of_completelyPseudoMetrizable`; this generalizes the result from complete metric spaces to completely (pseudo)metrizable spaces. |
addedBaire space (countable union of nowhere dense has empty interior)7313e1dfb91a
modifiedExistence of completion for any metric spaced96110ad9c75
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib constructs `UniformSpace.Completion alpha` for any uniform space and proves it is complete (`Completion.completeSpace`). For metric spaces, a compatible `MetricSpace` instance is given in `Mathlib.Topology.MetricSpace.Completion`. | Mathlib constructs `UniformSpace.Completion α` for any uniform space and proves it is complete (`Completion.completeSpace`); for metric spaces, a compatible `MetricSpace` instance is given in `Mathlib.Topology.MetricSpace.Completion`. |
modifiedCompletion is unique up to isometry90c30cfa64ff
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib proves uniqueness via `AbstractCompletion.compareEquiv` which gives a uniform equivalence between any two abstract completions. | Mathlib proves uniqueness via `AbstractCompletion.compareEquiv`, which gives a uniform equivalence between any two abstract completions. |
modifiedCompletion constructed via equivalence classes of Cauchy sequencesa5c0501de62f
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib constructs the completion as `SeparationQuotient (CauchyFilter alpha)`, using Cauchy filters rather than sequences. This is the generalization to uniform spaces of the equivalence-class-of-Cauchy-sequences construction. | Mathlib constructs the completion as `SeparationQuotient (CauchyFilter α)`, using Cauchy filters rather than sequences; this is the uniform-space generalization of the equivalence-classes-of-Cauchy-sequences construction. |
modifiedDistance on Cauchy sequences is a pseudometric40d9c63216ab
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib first equips the completion with a `PseudoMetricSpace` structure, then derives a `MetricSpace` via the separation quotient. | Mathlib first equips the completion with a `PseudoMetricSpace` structure and then derives a `MetricSpace` via the separation quotient. |
modifiedEmbedding into completion defines an isometry onto dense subspaced5ac04c39b7a
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib proves `Completion.coe_isometry : Isometry (coe : alpha -> Completion alpha)` and `Completion.denseRange_coe : DenseRange (coe : alpha -> Completion alpha)`. | Mathlib proves `Completion.coe_isometry : Isometry (coe : α → Completion α)` and `Completion.denseRange_coe : DenseRange (coe : α → Completion α)`. |
modifiedReal numbers are completion of rationals0012d6fba3ef
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib defines R as a structure wrapping `CauSeq.Completion.Cauchy` of Q with the absolute value, and `Real.equivCauchy` gives the equivalence. The construction is directly via Cauchy sequences of rationals. | Mathlib defines ℝ as a structure wrapping `CauSeq.Completion.Cauchy` of ℚ with the absolute value, and `Real.equivCauchy` gives the equivalence; the construction is directly via Cauchy sequences of rationals. |
modifiedp-adic numbers arise from completing rationals with different metric39e0c82d5cb0
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib defines Q_[p] as the Cauchy completion of Q with respect to the p-adic norm. | Mathlib defines ℚ_[p] as the Cauchy completion of ℚ with respect to the p-adic norm. |
modifiedCompleteness is a metric property, not topological9de5290fa986
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib distinguishes `CompleteSpace` (a property of the uniform structure) from `IsCompletelyMetrizableSpace` (a topological property: existence of some complete compatible metric). This distinction embodies the fact that completeness depends on the metric. | Mathlib distinguishes `CompleteSpace` (a property of the uniform structure) from `IsCompletelyMetrizableSpace` (a topological property: existence of some complete compatible metric); this distinction embodies the fact that completeness depends on the metric. |
modifiedReals are homeomorphic to (0,1) but complete vs not50cb65c20116
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib does not contain the explicit example that R is homeomorphic to (0,1) as a witness to completeness being metric-dependent. | Mathlib does not contain the explicit example that ℝ is homeomorphic to (0,1) as a witness to completeness being metric-dependent. |
modifiedCompletely uniformizable space67f7a7fab1cc
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib does not define 'completely uniformizable space' as a class. The file `Mathlib.Topology.UniformSpace.Uniformizable` discusses uniformizable spaces but not the complete variant. | Mathlib does not define 'completely uniformizable space' as a class; the file `Mathlib.Topology.UniformSpace.Uniformizable` discusses uniformizable spaces but not the complete variant. |
modifiedPolish space3610903ea45e
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib defines `PolishSpace alpha` as a typeclass for separable completely metrizable spaces. | Mathlib defines `PolishSpace α` as a typeclass for separable completely metrizable spaces. |
modifiedCompleteness via group structure (topological groups)6e65297bea14
| Field | From #2539 | To #3740 |
|---|
| mathlib.decl | IsTopologicalGroup.completeSpace_rightUniformSpace_iff_leftUniformSpace | IsUniformGroup |
| mathlib.match_kind | exact | generalization |
| note | Mathlib defines left and right uniform structures on topological groups and proves that completeness with respect to both agrees. This is the formalization of completeness via group structure. | Mathlib formalizes completeness for topological groups via the `IsUniformGroup` typeclass, which equips a topological group with a compatible uniform structure so `CompleteSpace` becomes meaningful. |
| provenance | ai | ai-moderated |
modifiedCompleteness via Cauchy nets or Cauchy filters6dcf6c58bc17
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib defines `Cauchy f` for a filter `f` in a uniform space. Filters generalize both nets and sequences; this is the primary formalization of the Cauchy concept in Mathlib. | Mathlib defines `Cauchy f` for a filter `f` in a uniform space; filters generalize both nets and sequences and are the primary formalization of the Cauchy concept in Mathlib. |
modifiedComplete space via Cauchy nets/filters0ba8d7704127
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib defines `CompleteSpace alpha` exactly as requiring every Cauchy filter to converge, which is the filter-based generalization described in this article section. | Mathlib defines `CompleteSpace α` exactly as requiring every Cauchy filter to converge, which is the filter-based generalization described in this section. |
modifiedCompletion exists for arbitrary uniform spaces065400d8d701
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib constructs `UniformSpace.Completion alpha` for any uniform space and proves it is a complete Hausdorff uniform space with a dense uniform embedding from alpha. | Mathlib constructs `UniformSpace.Completion α` for any uniform space and proves it is a complete Hausdorff uniform space with a dense uniform embedding from α. |
modifiedCauchy spaces as most general setting for Cauchy nets94650ff887f2
| Field | From #2539 | To #3740 |
|---|
| note | Mathlib does not define Cauchy spaces (in the sense of axiomatic Cauchy structures). This is a concept from general topology not yet formalized. | Mathlib does not define Cauchy spaces (in the sense of axiomatic Cauchy structures); this general-topology concept is not yet formalized. |