Cantor antichains from Cantor schemes

A Bool-indexed Cantor scheme A : List Bool → Set α with vanishing diameter whose branch intersections are all nonempty induces a continuous map of Cantor space into α, sending each branch to a chosen point of its intersection; in a pseudometric space the intersection need not be a single point. If moreover any point of A (false :: l) is E-inequivalent to any point of A (true :: l), the images of distinct branches are E-inequivalent: two branches first differ at some position, and their images lie in the two sibling pieces below their common prefix. So the scheme carries a Cantor antichain for E on its root A [].

No closedness of the pieces, completeness of the space or disjointness of siblings is assumed; the nonempty branch intersections are a hypothesis. Injectivity follows from the antichain property by reflexivity of E. For closure-antitone schemes of nonempty sets in a complete space the hypothesis can be discharged by Mathlib's CantorScheme.ClosureAntitone.map_of_vanishingDiam, while fusion arguments can supply it for schemes of non-closed sets.

For equality, E = ⊥, this recovers under these extra hypotheses the injectivity given by Mathlib's CantorScheme.Disjoint.map_injective, which needs neither vanishing diameter nor nonempty branch intersections and gives injectivity on the domain of inducedMap.

Main results

• CantorScheme.VanishingDiam.exists_antichain_map: the scheme induces a continuous injection of Cantor space along the scheme with pairwise E-inequivalent images.
• CantorScheme.VanishingDiam.hasCantorAntichainOn: the root of the scheme carries a Cantor antichain for E.

References

• Ported from cameronfreer/infinitary-logic at commit 518a366cba97b1ae8c4dc64a297a396939bc3e0b, InfinitaryLogic/Descriptive/CantorAntichain.lean (CantorScheme.exists_antichain_map).
• Divergences from that source: the results are stated on the vanishing-diameter hypothesis, for dot notation; the conclusion is also packaged as Setoid.HasCantorAntichainOn; the recursive splitting construction of the source is not included.

theorem CantorScheme.VanishingDiam.exists_antichain_map {α : Type u} [PseudoMetricSpace α] {A : List Bool → Set α} (hdiam : VanishingDiam A) (E : Setoid α) (hlim : ∀ (x : ℕ → Bool), (⋂ (n : ℕ), A (PiNat.res x n)).Nonempty) (hcross : ∀ (l : List Bool), ∀ x ∈ A (false :: l), ∀ y ∈ A (true :: l), ¬E x y) : ∃ (f : (ℕ → Bool) → α), Continuous f ∧ Function.Injective f ∧ (∀ (a : ℕ → Bool) (n : ℕ), f a ∈ A (PiNat.res a n)) ∧ ∀ (a b : ℕ → Bool), a ≠ b → ¬E (f a) (f b)

Cantor antichains from a scheme. A Bool-scheme with vanishing diameter, nonempty branch intersections and E-inequivalent siblings induces a continuous injection of Cantor space whose image of each branch lies along it, and whose images of distinct branches are E-inequivalent.

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

The root of the scheme carries a Cantor antichain. A Bool-scheme with vanishing diameter, nonempty branch intersections and E-inequivalent siblings gives a Cantor antichain for E on A [].