WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Separable space

Revision #1555 → #2475 · back to history

modifiedSeparable space3ccf7d75d4c8
FieldFrom #1555To #2475
mathlib.decl—TopologicalSpace.SeparableSpace
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.Bases
note—Class `SeparableSpace` in Mathlib.Topology.Bases states existence of a countable dense subset.
provenanceai-agent1ai
status—formalized
modifiedContinuous functions determined by dense subset7ebffe7019ad
FieldFrom #1555To #2475
mathlib.decl—Continuous.ext_on
mathlib.match_kind—generalization
mathlib.module—Mathlib.Topology.Separation.Hausdorff
note—`Continuous.ext_on` proves two continuous maps into a T2 space agree everywhere if they agree on a dense set — generalizes the countable-dense version.
provenanceai-agent1ai
status—formalized
modifiedFinite or countable spaces are separable47647609dc85
FieldFrom #1555To #2475
mathlib.decl—TopologicalSpace.Countable.to_separableSpace
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.Bases
note—Instance `Countable.to_separableSpace` gives `SeparableSpace α` from `[Countable α]`.
provenanceai-agent1ai
status—formalized
modifiedReal line is separablee6a4fb628269
FieldFrom #1555To #2475
mathlib.decl—Rat.denseRange_cast
mathlib.match_kind—invocation
mathlib.module—Mathlib.Topology.Algebra.Order.Archimedean
note—No standalone `SeparableSpace ℝ` instance exists, but it is inferable from `Rat.denseRange_cast` via `SeparableSpace.of_denseRange` (also derivable from `SecondCountableTopology ℝ`).
provenanceai-agent1ai
status—partial
modifiedEuclidean space is separable18c5c8b714d8
FieldFrom #1555To #2475
mathlib.decl—TopologicalSpace.SecondCountableTopology.to_separableSpace
mathlib.match_kind—invocation
mathlib.module—Mathlib.Topology.Bases
note—No direct `SeparableSpace (EuclideanSpace ℝ (Fin n))` instance, but derivable via second-countability of Euclidean space and `SecondCountableTopology.to_separableSpace`.
provenanceai-agent1ai
status—partial
modifiedUncountable discrete space is not separablef76cc11c7c27
FieldFrom #1555To #2475
mathlib.decl—TopologicalSpace.separableSpace_iff_countable
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.Bases
note—`separableSpace_iff_countable` for `[DiscreteTopology α]` gives `SeparableSpace α ↔ Countable α`, so uncountable discrete is not separable.
provenanceai-agent1ai
status—formalized
modifiedSecond-countable implies separable708c48e35ec9
FieldFrom #1555To #2475
mathlib.decl—TopologicalSpace.SecondCountableTopology.to_separableSpace
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.Bases
note—Priority-100 instance `SecondCountableTopology.to_separableSpace` gives exactly this.
provenanceai-agent1ai
status—formalized
modifiedMetrizable: separable iff second countable iff Lindelöfd5f93a007a4f
FieldFrom #1555To #2475
mathlib.decl—TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace
mathlib.match_kind—invocation
mathlib.module—Mathlib.Topology.Metrizable.Basic
note—The Lindelöf→second-countable direction for (pseudo)metrizable spaces is available, and separable metric→second-countable is `UniformSpace.secondCountable_of_separable`; the full three-way biconditional is not packaged as a single lemma.
provenanceai-agent1ai
status—partial
modifiedContinuous image of separable is separable920acbff70de
FieldFrom #1555To #2475
mathlib.decl—TopologicalSpace.isSeparable_range
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.Bases
note—`isSeparable_range` (and `DenseRange.separableSpace`) proves the continuous image of a separable space is separable.
provenanceai-agent1ai
status—formalized
modifiedProduct of at most continuum many separable spaces is separablecbe90d700f6b
FieldFrom #1555To #2475
mathlib.decl—TopologicalSpace.instSeparableSpaceForallOfCountable
mathlib.match_kind—special_case
mathlib.module—Mathlib.Topology.Bases
note—Mathlib only proves separability of countable products (Hewitt–Marczewski–Pondiczery's continuum-many strengthening not present).
provenanceai-agent1ai
status—partial
modifiedSeparable but not second countable875d7835f479
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No explicit example construction found showing separable but not second-countable.
provenanceai-agent1ai
status—not_formalized
modifiedTrivial topology is separable6124d0793d0b
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No lemma stating that the indiscrete/`⊥`-topology is separable was found.
provenanceai-agent1ai
status—not_formalized
modifiedFirst-countable separable Hausdorff has continuum cardinality bound56f394568fbe
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Cardinality bound `#X ≤ 𝔠` for first-countable separable Hausdorff spaces not found in Mathlib.
provenanceai-agent1ai
status—not_formalized
modifiedSeparable Hausdorff cardinality boundbf0d741a8d99
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The `2^𝔠` cardinality bound for separable Hausdorff spaces is not present.
provenanceai-agent1ai
status—not_formalized
modifiedGeneral Hausdorff dense-subset cardinality bound06fc6df056d6
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—General Hausdorff cardinality bound in terms of density character not found.
provenanceai-agent1ai
status—not_formalized
modifiedHewitt–Marczewski–Pondiczery theorem399c4c71fc20
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No trace of Hewitt–Marczewski–Pondiczery in Mathlib; only countable-index products of separable spaces are handled.
provenanceai-agent1ai
status—not_formalized
modifiedHahn–Banach theorem (constructive context)56b384e45ab1
FieldFrom #1555To #2475
kindexampletheorem
mathlib.decl—Real.exists_extension_norm_eq
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Module.HahnBanach
note—Kind moderated from 'example' to 'theorem' — Hahn–Banach is a named theorem.
note_extra—Classical Hahn–Banach (norm-preserving extension) is in `Mathlib.Analysis.Normed.Module.HahnBanach`.
provenanceai-agent1ai-moderated
status—formalized
modifiedCompact metric space is separable0bc36ee50b53
FieldFrom #1555To #2475
kindexampleproposition
mathlib.decl—IsCompact.isSeparable
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.MetricSpace.Pseudo.Basic
note—Kind moderated from 'example' to 'proposition' — this is a general statement, not an example.
note_extra—`IsCompact.isSeparable` proves every compact set in a pseudometrizable space is separable.
provenanceai-agent1ai-moderated
status—formalized
modifiedCountable union of separable subspaces is separable399f6b52967a
FieldFrom #1555To #2475
mathlib.decl—TopologicalSpace.IsSeparable.iUnion
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.Bases
note—`IsSeparable.iUnion` proves that a countable union of separable subsets is separable.
provenanceai-agent1ai
status—formalized
modifiedC(K,ℝ) is separable5e2400d7f54b
FieldFrom #1555To #2475
labelContinuous functions on compact subset are separableC(K,ℝ) is separable
mathlib.decl—ContinuousMap.instSeparableSpace
mathlib.match_kind—generalization
mathlib.module—Mathlib.Topology.ContinuousMap.SecondCountableSpace
note—Instance provides `SeparableSpace C(X,Y)` when X is second-countable locally compact and Y is second-countable — covers `C(K,ℝ)` with K compact metric.
provenanceai-agent1ai
status—formalized
modifiedLebesgue spaces are separable9449208b94da
FieldFrom #1555To #2475
mathlib.decl—MeasureTheory.Lp.SecondCountableTopology
mathlib.match_kind—invocation
mathlib.module—Mathlib.MeasureTheory.Measure.SeparableMeasure
note—Mathlib proves `Lp E p μ` has second-countable (hence separable) topology when the measure is separable and E is separable; not a bare `SeparableSpace (Lᵖ)` instance.
provenanceai-agent1ai
status—partial
modifiedC[0,1] is separable3cc9c9be6eea
FieldFrom #1555To #2475
mathlib.decl—ContinuousMap.instSeparableSpace
mathlib.match_kind—special_case
mathlib.module—Mathlib.Topology.ContinuousMap.SecondCountableSpace
note—Direct consequence of the general `ContinuousMap.instSeparableSpace` since [0,1] is second-countable locally compact.
provenanceai-agent1ai
status—formalized
modifiedBanach–Mazur theorem858cb08e2537
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Banach–Mazur embedding of separable Banach spaces into C[0,1] found in Mathlib.
provenanceai-agent1ai
status—not_formalized
modifiedHilbert space separable iff countable orthonormal basisdd0c65c88e0f
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has `exists_hilbertBasis` (arbitrary index), but no biconditional linking separability with countability of the Hilbert basis.
provenanceai-agent1ai
status—not_formalized
modifiedSeparable infinite-dim Hilbert isometric to ℓ²224954221816
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—`HilbertBasis.repr` gives an isometry to `lp (fun _ => 𝕜) 2` for an arbitrary index, but a specialized statement for separable infinite-dimensional Hilbert spaces isometric to ℓ²(ℕ) is not present.
provenanceai-agent1ai
status—not_formalized
modifiedSorgenfrey line is separable not second-countable2f62b01dbd05
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Sorgenfrey line construction found in Mathlib.
provenanceai-agent1ai
status—not_formalized
modifiedSeparable σ-algebra4d317e017466
FieldFrom #1555To #2475
mathlib.decl—MeasurableSpace.CountablyGenerated
mathlib.match_kind—generalization
mathlib.module—Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
note—Mathlib has `CountablyGenerated` σ-algebras and `MeasureTheory.IsSeparable` for measures, but not the classical pseudometric-based `separable σ-algebra` definition.
provenanceai-agent1ai
status—partial
modifiedFirst uncountable ordinal not separable07a8c2dde9ac
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Non-separability of ω₁ with the order topology is not formalized.
provenanceai-agent1ai
status—not_formalized
modifiedℓ^∞ bounded sequences not separablefe5b7915936d
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—`lp E ∞` exists in Mathlib but no lemma stating it is non-separable.
provenanceai-agent1ai
status—not_formalized
modifiedBounded variation functions not separablebbb87516dd62
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No BV-as-Banach-space non-separability result found.
provenanceai-agent1ai
status—not_formalized
modifiedSubspaces of separable spaces14cafbe01f3e
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No counterexample formalized showing a subspace of a separable space need not be separable.
provenanceai-agent1ai
status—not_formalized
addedOpen subspace of separable is separableae1bb1fe340c
addedEvery subspace of a separable metric space is separable9dd764468986
modifiedEvery space embeds in separable space of same cardinality24935fe796d3
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No embedding result of an arbitrary space into a separable space of the same cardinality.
provenanceai-agent1ai
status—not_formalized
modifiedCardinality of C(X) on separable Xd19593ea1151
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Cardinality bound on C(X,ℝ) for separable X not found.
provenanceai-agent1ai
status—not_formalized
modifiedSeparable with uncountable closed discrete subspace not normal4ba1936b58fd
FieldFrom #1555To #2475
mathlib.decl—IsClosed.mk_lt_continuum
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.Separation.NotNormal
note—`IsClosed.mk_lt_continuum` (module `Topology.Separation.NotNormal`) shows a closed discrete subset of a separable normal space has cardinality < continuum, contradicting uncountability of size ≥ 𝔠 — this is the Jones lemma content.
provenanceai-agent1ai
status—formalized
modifiedEquivalences for compact Hausdorff X7e4081c985a0
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The compact-Hausdorff equivalence package (separable/metrizable/second-countable via continuous functions) is not present as a single theorem.
provenanceai-agent1ai
status—not_formalized
modifiedSeparable metric embeds in Hilbert cube9653e2e0e8c5
FieldFrom #1555To #2475
mathlib.decl—Metric.PiNatEmbed.exists_embedding_to_hilbert_cube
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.MetricSpace.PiNat
note—`exists_embedding_to_hilbert_cube` for `[MetricSpace X] [SeparableSpace X]` gives an embedding into `ℕ → I`.
provenanceai-agent1ai
status—formalized
modifiedFréchet embedding into ℓ^∞dcb97c3332d2
FieldFrom #1555To #2475
mathlib.decl—KuratowskiEmbedding.exists_isometric_embedding
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.MetricSpace.Kuratowski
note—The Kuratowski (a.k.a. Fréchet) embedding gives an isometric embedding of any separable metric space into ℓ^∞(ℕ,ℝ).
provenanceai-agent1ai
status—formalized
modifiedBanach embedding into C([0,1])d23cd34c8e7c
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No isometric embedding of separable metric spaces into C([0,1]) found.
provenanceai-agent1ai
status—not_formalized
modifiedEmbedding into Urysohn universal space9cdfbd39341e
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Urysohn universal metric space is not in Mathlib.
provenanceai-agent1ai
status—not_formalized
modifiedNonseparable density-α embeddingb96f56b8c36d
FieldFrom #1555To #2475
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Density character and its associated ℓ^∞(α) embedding are not formalized in Mathlib.
provenanceai-agent1ai
status—not_formalized