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 #

source

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)

Instances For

Adapters that need no metric structure #

source

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.

source

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.

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.