Perfect and Cantor antichains, and thinness

The vocabulary a dichotomy theorem is stated in, separated from any particular dichotomy.

• HasPerfectAntichainOn r A — a nonempty perfect subset of A of pairwise r-inequivalent points;
• HasCantorAntichainOn r A — a continuous Cantor-space parametrization of such an antichain, the constructive form the Cantor-scheme builders actually produce;
• IsThinOn r A — the negation of the first.

The two positive forms are related by HasPerfectAntichainOn.hasCantorAntichainOn, which is Perfect.exists_nat_bool_injection plus bookkeeping. Injectivity of a Cantor antichain is not an extra hypothesis: it follows from reflexivity of the setoid, since distinct arguments have inequivalent images and every point is equivalent to itself.

The file also carries the cardinal facts these statements are measured against: a nonempty perfect set in a complete metric space has size continuum (Perfect.mk_eq_continuum); a perfect transversal forces continuum-many classes (continuum_classes_of_perfect_transversal, with its two-sided companion); and a Polish space, hence any quotient of one, has at most continuum-many points (mk_le_continuum_of_polish, mk_quotient_le_continuum_of_polish). None of them mentions a dichotomy, an equivalence relation being closed, or a splitting hypothesis.

Hypotheses are kept minimal, and the ordering below is what makes that possible. Only three results need SecondCountableTopology: the two Polish cardinality bounds and the upper half of Perfect.mk_eq_continuum. Everything else needs at most MetricSpace + CompleteSpace (for the Cantor injection) or nothing beyond TopologicalSpace. In particular continuum_classes_of_perfect_transversal is proved through the Cantor antichain rather than through mk_eq_continuum, which is what lets it drop second countability — it only ever needed the lower bound.

The generic vocabulary

def HasPerfectAntichainOn {X : Type u} [TopologicalSpace X] (r : Setoid X) (A : Set X) : Prop

A carries a perfect antichain for r: a nonempty perfect subset of A whose points are pairwise r-inequivalent.

Equations

• HasPerfectAntichainOn r A = ∃ (P : Set X), Perfect P ∧ P.Nonempty ∧ P ⊆ A ∧ ∀ x ∈ P, ∀ y ∈ P, r x y → x = y

def HasCantorAntichainOn {X : Type u} [TopologicalSpace X] (r : Setoid X) (A : Set X) : Prop

A carries a Cantor antichain for r: a continuous map from Cantor space into A sending distinct points to r-inequivalent ones. This is what the Cantor-scheme builders produce directly, and it is the form a thinness proof must refute.

Equations

• HasCantorAntichainOn r A = ∃ (f : (ℕ → Bool) → X), Continuous f ∧ (∀ (x : ℕ → Bool), f x ∈ A) ∧ ∀ (x y : ℕ → Bool), x ≠ y → ¬r (f x) (f y)

def IsThinOn {X : Type u} [TopologicalSpace X] (r : Setoid X) (A : Set X) : Prop

A is thin for r: no perfect antichain.

Equations

• IsThinOn r A = ¬HasPerfectAntichainOn r A

Adapters that need no metric structure

theorem HasCantorAntichainOn.mono {X : Type u} [TopologicalSpace X] {r : Setoid X} {A B : Set X} (h : HasCantorAntichainOn r A) (hAB : A ⊆ B) : HasCantorAntichainOn r B

Enlarging the ambient set preserves a Cantor antichain. Keeping this separate is what lets the scheme wrappers below conclude at the scheme's own root rather than carrying a containment hypothesis.

theorem HasCantorAntichainOn.mono_relation {X : Type u} [TopologicalSpace X] {A : Set X} {r s : Setoid X} (hrs : ∀ (x y : X), r x y → s x y) (h : HasCantorAntichainOn s A) : HasCantorAntichainOn r A

A Cantor antichain for a coarser relation is one for a finer relation.

hrs says r refines s: being r-related implies being s-related, so r cuts the space into the finer classes. Separating points for the coarser s is therefore the stronger requirement, and it survives the passage to r.

The direction is easy to reverse mentally, so concretely: with r := isoSetoid φ and s := bfEquivSetoid φ α, isomorphic models are back-and-forth equivalent, so a family that is pairwise BF-inequivalent is in particular pairwise non-isomorphic.

theorem HasCantorAntichainOn.of_subtype {X : Type u} [TopologicalSpace X] {r : Setoid X} {A : Set X} (h : HasCantorAntichainOn (Setoid.comap Subtype.val r) Set.univ) : HasCantorAntichainOn r A

A Cantor antichain on a subtype is one on the underlying set.

The subtype carries r pulled back along the inclusion, and it is the ambient set seen from inside, so the containment clause is vacuous there and becomes membership in A here. Only continuity has to move, and it moves by composing with the inclusion.

This is the return leg for anything proved on the model subtype — where a Polish structure is available — when the statement to be established is about the ambient space.

theorem HasCantorAntichainOn.mono_topology {X : Type u} {r : Setoid X} {A : Set X} {t t' : TopologicalSpace X} (hle : t' ≤ t) (h : HasCantorAntichainOn r A) : HasCantorAntichainOn r A

A Cantor antichain survives coarsening the topology.

Of the three clauses only continuity is topological, and continuity into a coarser topology is just composition with the identity. This is the direction needed to carry a witness built in a Polish refinement — the kind PolishSpace.IsClopenable supplies — back to the ambient space.

It is also why no theorem about perfectness surviving coarsening is required: coarsening is applied to the Cantor antichain, where it is cheap, and perfectness is recovered afterwards in the ambient space by HasCantorAntichainOn.hasPerfectAntichainOn.

theorem HasCantorAntichainOn.injective {X : Type u} [TopologicalSpace X] {r : Setoid X} {A : Set X} (h : HasCantorAntichainOn r A) : ∃ (f : (ℕ → Bool) → X), Continuous f ∧ Set.range f ⊆ A ∧ Function.Injective f

A Cantor antichain is injective.

The inequivalence clause is deliberately not restated in the conclusion: it is already the content of h, and a consumer needing it should unpack h. One job per adapter.

theorem HasCantorAntichainOn.continuum_le_quotient {X : Type u} [TopologicalSpace X] {r : Setoid X} {A : Set X} (h : HasCantorAntichainOn r A) : Cardinal.continuum ≤ Cardinal.mk (Quotient r)

A Cantor antichain forces continuum-many classes. No metric or completeness assumption: the argument is the quotient-map injection, and only Continuous f mentions the topology.

Cantor antichain → perfect antichain

The converse direction to HasPerfectAntichainOn.hasCantorAntichainOn below, and the one that needs no metric or completeness assumption — only that the ambient space is Hausdorff.

theorem HasCantorAntichainOn.hasPerfectAntichainOn {X : Type u} [TopologicalSpace X] {r : Setoid X} {A : Set X} [T2Space X] (h : HasCantorAntichainOn r A) : HasPerfectAntichainOn r A

A Cantor antichain is a perfect antichain.

The range is closed because a continuous injection out of a compact space into a Hausdorff one is a closed embedding; and it inherits Cantor space's lack of isolated points by transporting accumulation points along that injection. No metric, completeness, or second-countability assumption is needed — only T2Space.

theorem IsThinOn.no_cantorAntichain {X : Type u} [TopologicalSpace X] {r : Setoid X} {A : Set X} [T2Space X] (h : IsThinOn r A) : ¬HasCantorAntichainOn r A

Thinness rules out a Cantor antichain. The converse of IsThinOn.of_no_cantorAntichain below, and much cheaper: that direction needs a complete metric space, this one only T2Space.

Adapters needing the Cantor injection

Perfect.exists_nat_bool_injection needs a complete metric space, but not second countability.

theorem HasPerfectAntichainOn.hasCantorAntichainOn {α : Type u} [MetricSpace α] [CompleteSpace α] {r : Setoid α} {A : Set α} (h : HasPerfectAntichainOn r A) : HasCantorAntichainOn r A

A perfect antichain yields a Cantor antichain: Perfect.exists_nat_bool_injection together with the observation that the injection's range lies in the perfect set, hence in A.

theorem IsThinOn.of_no_cantorAntichain {α : Type u} [MetricSpace α] [CompleteSpace α] {r : Setoid α} {A : Set α} (h : ¬HasCantorAntichainOn r A) : IsThinOn r A

Refuting Cantor antichains suffices for thinness.

Perfect set cardinality

This is where second countability genuinely enters, and only for the upper bound.

theorem Perfect.mk_eq_continuum {α : Type u} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] {C : Set α} (hperf : Perfect C) (hne : C.Nonempty) : Cardinal.mk ↑C = Cardinal.continuum

A nonempty perfect subset of a Polish space has cardinality = continuum. Lower bound via Perfect.exists_nat_bool_injection; upper bound via second-countability of Polish spaces.

Perfect transversal → continuum classes

theorem continuum_classes_of_perfect_transversal {α : Type u} [MetricSpace α] [CompleteSpace α] (r : Setoid α) {C : Set α} (hperf : Perfect C) (hne : C.Nonempty) (hinequiv : ∀ x ∈ C, ∀ y ∈ C, r x y → x = y) : Cardinal.continuum ≤ Cardinal.mk (Quotient r)

If an equivalence relation has a perfect set of pairwise inequivalent elements, it has at least continuum classes.

No second countability: the route is the Cantor antichain, i.e. only the lower bound of Perfect.mk_eq_continuum, which is exactly the half that does not need it.

theorem eq_continuum_classes_of_perfect_transversal {α : Type u} [MetricSpace α] [CompleteSpace α] (r : Setoid α) {C : Set α} (hperf : Perfect C) (hne : C.Nonempty) (hinequiv : ∀ x ∈ C, ∀ y ∈ C, r x y → x = y) (hle : Cardinal.mk α ≤ Cardinal.continuum) : Cardinal.mk (Quotient r) = Cardinal.continuum

If an equivalence relation has a perfect set of pairwise inequivalent elements, it has exactly continuum classes (assuming the ambient space has cardinality ≤ continuum).

No second countability: the upper bound arrives explicitly as hle.

Polish space cardinality upper bound

theorem mk_le_continuum_of_polish {α : Type u} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [Nonempty α] : Cardinal.mk α ≤ Cardinal.continuum

A Polish space has cardinality ≤ continuum.

theorem mk_quotient_le_continuum_of_polish {α : Type u} [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [Nonempty α] (r : Setoid α) : Cardinal.mk (Quotient r) ≤ Cardinal.continuum

The quotient of a Polish space has cardinality ≤ continuum.

Packaging the Cantor-scheme builders

Wrappers only: the existential content is CantorAntichain.lean's, restated in the vocabulary above so that consumers need not unpack it. Each concludes at the scheme's own root; use HasCantorAntichainOn.mono to enlarge to an ambient set.

theorem CantorScheme.hasCantorAntichainOn {α : Type u} [PseudoMetricSpace α] (r : Setoid α) {A : List Bool → Set α} (hlim : ∀ (x : ℕ → Bool), (⋂ (n : ℕ), A (PiNat.res x n)).Nonempty) (hdiam : VanishingDiam A) (hcross : ∀ (l : List Bool), ∀ x ∈ A (false :: l), ∀ y ∈ A (true :: l), ¬r x y) : HasCantorAntichainOn r (A [])

CantorScheme.exists_antichain_map in antichain vocabulary, concluding at the scheme root A [] via branch membership at level zero.

theorem CantorScheme.hasCantorAntichainOn_of_splitting {α : Type u} [MetricSpace α] [CompleteSpace α] (r : Setoid α) (P : Set α → Prop) (hcl : ∀ (F : Set α), P F → IsClosed F) (hne : ∀ (F : Set α), P F → F.Nonempty) {E : Set α} (hE : P E) (hsplit : ∀ (F : Set α), P F → ∀ (ε : ENNReal), 0 < ε → ∃ (F₀ : Set α) (F₁ : Set α), P F₀ ∧ P F₁ ∧ F₀ ⊆ F ∧ F₁ ⊆ F ∧ Metric.ediam F₀ ≤ ε ∧ Metric.ediam F₁ ≤ ε ∧ ∀ x ∈ F₀, ∀ y ∈ F₁, ¬r x y) : HasCantorAntichainOn r E

CantorScheme.exists_antichain_map_of_splitting in antichain vocabulary.