Homogenous.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

13 declarations, 5 contain sorry, 0 declared as axioms

Conjectures around homogeneous topological spaces

This file formalizes the notions of a homogeneous topological space and of (ω-)monolithic topological spaces, and states some open problems about homogeneous and monolithic compact spaces.

References:

[Ar2013] Arhangeliski, Alexandr. "Selected old open problems in general topology." Buletinul Academiei de Ştiinţe a Republicii Moldova. Matematica 73.2-3 (2013): 37-46. https://www.math.md/files/basm/y2013-n2-3/y2013-n2-3-(pp37-46).pdf.pdf
[Ar1987] Arhangel'skii, A. V. "Topological homogeneity. Topological groups and their continuous images." Russian Mathematical Surveys 42.2 (1987): 83-131. https://doi.org/10.1070/RM1987v042n02ABEH001333

Imports (1)

FormalConjecturesUtil

class Homogeneous.HomogeneousSpace A topological space $X$ is called homogeneous if for all $x, y \in X$ there is homeomorphism $f : X \to X$ with $f(x) = y$ line 46 source
Source documentation
A topological space $X$ is called homogeneous if for all $x, y \in X$ there is homeomorphism $f : X \to X$ with $f(x) = y$.

standard axioms: Quot.sound what this means
Statement uses: TopologicalSpace
```
class HomogeneousSpace (X : Type*) [TopologicalSpace X] : Prop where
…
```
instance Homogeneous.DiscreteTopology.toHomogeneousSpace Every discrete space is homogeneous line 51 source
Source documentation
Every discrete space is homogeneous.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, DiscreteTopology, Homogeneous.HomogeneousSpace
Proof uses: Homogeneous.HomogeneousSpace.mk, Exists.intro, Homeomorph, Eq, IsHomeomorph.homeomorph, Equiv.Perm, Equiv.swap, Classical.propDecidable, IsHomeomorph.equiv_of_discreteTopology, Eq.mpr, id, congrArg, IsHomeomorph.homeomorph_apply, Equiv.swap_apply_left, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
instance DiscreteTopology.toHomogeneousSpace (X : Type*) [TopologicalSpace X] [DiscreteTopology X] :
    HomogeneousSpace X where
…
```
Mentions: Homogeneous.HomogeneousSpace
theorem Homogeneous.homogeneousSpace_exists_inj_tendsto Problem 13 in [Ar2013]: Is it true that every infinite homogeneous compact hausdorff space contains a non-trivial convergent sequence? sorry line 63 source
Source documentation
Problem 13 in [Ar2013]: Is it true that every infinite homogeneous compact hausdorff space contains a non-trivial convergent sequence?

depends on sorry what this means
Statement uses: Iff, True, TopologicalSpace, Not, Finite, T2Space, CompactSpace, Homogeneous.HomogeneousSpace, Exists, Nat, And, Function.Injective, Filter.Tendsto, Filter.atTop, nhds
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem homogeneousSpace_exists_inj_tendsto :
    answer(sorry) ↔ ∀ (X : Type) (_ : TopologicalSpace X), ¬ Finite X → T2Space X → CompactSpace X →
      HomogeneousSpace X → ∃ s : ℕ → X, s.Injective ∧ ∃ a : X, Tendsto s atTop (nhds a) := by
…
```
Mentions: Homogeneous.HomogeneousSpace
theorem Homogeneous.homogeneousSpace_exists_surjective Problem 14 in [Ar2013]: Is it possible to represent an arbitrary compact hausdorff space as an image of a homogeneous compact space under a continuous mapping? sorry line 72 source
Source documentation
Problem 14 in [Ar2013]: Is it possible to represent an arbitrary compact hausdorff space as an image of a homogeneous compact space under a continuous mapping?

depends on sorry what this means
Statement uses: Iff, True, TopologicalSpace, T2Space, CompactSpace, Exists, And, Homogeneous.HomogeneousSpace, Continuous, Function.Surjective
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem homogeneousSpace_exists_surjective :
    answer(sorry) ↔ ∀ (X : Type) (_ : TopologicalSpace X), T2Space X → CompactSpace X →
      ∃ (Y : Type) (_ : TopologicalSpace Y), T2Space Y ∧ CompactSpace Y ∧ HomogeneousSpace Y ∧
        ∃ f : Y → X, Continuous f ∧ f.Surjective := by
…
```
Mentions: Homogeneous.HomogeneousSpace
class Homogeneous.CountablyMonolithicSpace A topological space is called ω-monolithic if the closure of every countable subspace is metrizable line 80 source
Source documentation
A topological space is called ω-monolithic if the closure of every countable subspace is metrizable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace
```
class CountablyMonolithicSpace (X : Type*) [TopologicalSpace X] : Prop where
…
```
instance Homogeneous.MetrizableSpace.countablyMonolithicSpace Every Metrizable space is ω-monolithic line 85 source
Source documentation
Every Metrizable space is ω-monolithic.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, TopologicalSpace.MetrizableSpace, Homogeneous.CountablyMonolithicSpace
Proof uses: Homogeneous.CountablyMonolithicSpace.mk, Set, Set.Countable, inferInstance, closure, Membership.mem
4 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
instance MetrizableSpace.countablyMonolithicSpace
    (X : Type*) [TopologicalSpace X] [MetrizableSpace X] : CountablyMonolithicSpace X := by
…
```
Mentions: Homogeneous.CountablyMonolithicSpace
theorem Homogeneous.firstCountableTopology_of_countablyMonolithicSpace Problem 15 in [Ar2013]: Is every homogeneous ω-monolithic compact hausdorff space first countable? sorry line 94 source
Source documentation
Problem 15 in [Ar2013]: Is every homogeneous ω-monolithic compact hausdorff space first countable?

depends on sorry what this means
Statement uses: Iff, True, TopologicalSpace, T2Space, CompactSpace, Homogeneous.HomogeneousSpace, Homogeneous.CountablyMonolithicSpace, FirstCountableTopology
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem firstCountableTopology_of_countablyMonolithicSpace :
    answer(sorry) ↔ ∀ (X : Type) (_ : TopologicalSpace X), T2Space X → CompactSpace X →
      HomogeneousSpace X → CountablyMonolithicSpace X → FirstCountableTopology X := by
…
```
Mentions: Homogeneous.HomogeneousSpace, Homogeneous.CountablyMonolithicSpace
theorem Homogeneous.countablyMonolithicSpace_card_lt Problem 16 in [Ar2013]: Is the cardinality of every homogeneous ω-monolithic compact hausdorff space not greater than 𝔠? sorry line 102 source
Source documentation
Problem 16 in [Ar2013]: Is the cardinality of every homogeneous ω-monolithic compact hausdorff space not greater than 𝔠?

depends on sorry what this means
Statement uses: Iff, True, TopologicalSpace, T2Space, CompactSpace, Homogeneous.HomogeneousSpace, Homogeneous.CountablyMonolithicSpace, LE.le, Cardinal, Cardinal.mk, Cardinal.continuum
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem countablyMonolithicSpace_card_lt :
    answer(sorry) ↔ ∀ (X : Type) (_ : TopologicalSpace X), T2Space X → CompactSpace X →
      HomogeneousSpace X → CountablyMonolithicSpace X → #X ≤ 𝔠 := by
…
```
Mentions: Homogeneous.HomogeneousSpace, Homogeneous.CountablyMonolithicSpace
class Homogeneous.MonolithicSpace A topological space is monolithic (see [Ar1987]; [Ar2013] uses the term without defining it) if every subspace has network weight at most its density line 109 source
Source documentation
A topological space is monolithic (see [Ar1987]; [Ar2013] uses the term without defining it) if every subspace has network weight at most its density.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace
```
class MonolithicSpace (X : Type*) [TopologicalSpace X] : Prop where
…
```
theorem Homogeneous.monolithicSpace_iff_networkWeight_closure_le Monolithicity in the form nw(cl A) ≤ |A| + ω for every subset A line 114 source
Source documentation
Monolithicity in the form nw(cl A) ≤ |A| + ω for every subset A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, Iff, Homogeneous.MonolithicSpace, Set, LE.le, Cardinal, TopologicalSpace.networkWeight, closure, Membership.mem, HAdd.hAdd, Cardinal.mk, Cardinal.aleph0
Proof uses: Iff.intro, LE.le.trans, TopologicalSpace.density, Homogeneous.MonolithicSpace.networkWeight_le_density, Dense, Set.preimage, Eq.mpr, Set.image, id, Eq, congrArg, propext, Subtype.dense_iff, Inter.inter, Subtype, Subtype.image_preimage_coe, Iff.mpr, Set.inter_eq_right, subset_closure, le_refl and 16 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
theorem monolithicSpace_iff_networkWeight_closure_le (X : Type*) [TopologicalSpace X] :
    MonolithicSpace X ↔ ∀ s : Set X, networkWeight (closure s) ≤ #s + ℵ₀ := by
…
```
Mentions: Homogeneous.MonolithicSpace
instance Homogeneous.DiscreteTopology.toMonolithicSpace Every discrete space is monolithic line 135 source
Source documentation
Every discrete space is monolithic.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, DiscreteTopology, Homogeneous.MonolithicSpace
Proof uses: Homogeneous.MonolithicSpace.mk, Set, Eq.mpr, LE.le, Cardinal, TopologicalSpace.networkWeight, Membership.mem, TopologicalSpace.density, HAdd.hAdd, Cardinal.mk, Cardinal.aleph0, id, Eq, congrArg, TopologicalSpace.networkWeight_discrete, TopologicalSpace.density_discrete, le_refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
instance DiscreteTopology.toMonolithicSpace (X : Type*) [TopologicalSpace X] [DiscreteTopology X] :
    MonolithicSpace X where
…
```
Mentions: Homogeneous.MonolithicSpace
instance Homogeneous.SecondCountableTopology.toMonolithicSpace Every second countable space is monolithic line 141 source
Source documentation
Every second countable space is monolithic.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: TopologicalSpace, SecondCountableTopology, Homogeneous.MonolithicSpace
Proof uses: Homogeneous.MonolithicSpace.mk, Set, LE.le.trans, Cardinal, TopologicalSpace.networkWeight, Membership.mem, Cardinal.aleph0, TopologicalSpace.density, TopologicalSpace.networkWeight_le_aleph0, TopologicalSpace.aleph0_le_density
6 instances, coercions and auxiliary constants left out.
```
instance SecondCountableTopology.toMonolithicSpace (X : Type*) [TopologicalSpace X]
    [SecondCountableTopology X] : MonolithicSpace X where
…
```
Mentions: Homogeneous.MonolithicSpace
theorem Homogeneous.monolithicSpace_exists_nhds_generated_countable Problem 17 in [Ar2013]: Is it true that every nonempty monolithic compact hausdorff space contains a point with a first countable neighborhood basis? sorry line 152 source
Source documentation
Problem 17 in [Ar2013]: Is it true that every nonempty monolithic compact hausdorff space contains a point with a first countable neighborhood basis?
Note: Nonempty X is required since the conclusion asserts the existence of a point.

depends on sorry what this means
Statement uses: Iff, True, TopologicalSpace, T2Space, CompactSpace, Nonempty, Homogeneous.MonolithicSpace, Exists, Filter.IsCountablyGenerated, nhds
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem monolithicSpace_exists_nhds_generated_countable :
    answer(sorry) ↔ ∀ (X : Type) (_ : TopologicalSpace X), T2Space X → CompactSpace X →
      Nonempty X → MonolithicSpace X → ∃ x : X, (𝓝 x).IsCountablyGenerated := by
…
```
Mentions: Homogeneous.MonolithicSpace