Thinness from a countable-ordinal rank

The standard route to thinness: equip the points with a rank below ω₁, know that each fixed-rank antichain is countable, and know that a Cantor antichain has bounded rank. Then a Cantor antichain would be a countable union of countable sets while being of size continuum.

ThinRankAnalysis bundles exactly that evidence. no_cantorAntichain and isThinOn are derived from it, not fields: a structure whose fields already asserted the conclusion would prove nothing.

The Cantor-antichain hypothesis is the refined one: the rank need only be bounded on a continuously and injectively embedded Cantor subcopy of the antichain, not on the whole of it. That is all the countability contradiction consumes, and it is markedly easier to supply. ThinRankAnalysis.of_bounded_on_cantor_antichains recovers the structure from a bound on the whole antichain, for producers that happen to have one.

Setoid.countable_antichain is the elementary quotient step, factored out because it is independent of any rank and useful on its own.

theorem Setoid.countable_antichain {X : Type u} (r : Setoid X) [Countable (Quotient r)] {B : Set X} (hB : ∀ x ∈ B, ∀ y ∈ B, r x y → x = y) : B.Countable

An antichain injects into the quotient, so a countable quotient forces a countable antichain. No topology and no rank.

structure ThinRankAnalysis {X : Type u} [TopologicalSpace X] (r : Setoid X) (A : Set X) : Type (max 1 u)

The evidence that a rank witnesses thinness of A for r.

• rank : X → Ordinal.{0}

  The rank function.

• rank_lt_omega1 (x : X) : x ∈ A → self.rank x < Ordinal.omega 1

  Ranks of points of A are countable ordinals.

• fixedRankAntichains_countable (α : Ordinal.{0}) : α < Ordinal.omega 1 → ∀ B ⊆ A, (∀ x ∈ B, self.rank x = α) → (∀ x ∈ B, ∀ y ∈ B, r x y → x = y) → B.Countable

  Each fixed-rank antichain inside A is countable.

• bounded_on_refined_cantor_antichains (f : (ℕ → Bool) → X) : Continuous f → (∀ (x : ℕ → Bool), f x ∈ A) → (∀ (x y : ℕ → Bool), x ≠ y → ¬r (f x) (f y)) → ∃ (e : (ℕ → Bool) → ℕ → Bool), Continuous e ∧ Function.Injective e ∧ ∃ β < Ordinal.omega 1, ∀ (x : ℕ → Bool), self.rank (f (e x)) < β

  Every Cantor antichain contains a Cantor subcopy on which the ranks are bounded below ω₁. The bound need not hold on the whole antichain.

  e is stored as continuous and injective: continuity certifies the intended Cantor subcopy, while injectivity is what the contradiction below consumes. No separate IsEmbedding witness is required.

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

No Cantor antichain. Pass to the Cantor subcopy the analysis supplies, on which the ranks are bounded; that subcopy is the union, over the countably many ordinals below the bound, of fixed-rank antichains — each countable — hence countable, while being a continuous injective image of Cantor space.

Continuity of e is not consumed here — only its injectivity is, to keep the composite an antichain. The field promises continuity because that is what makes the subcopy a genuine Cantor subcopy, which is what a producer must supply and other consumers may need.

theorem ThinRankAnalysis.isThinOn {α : Type u} [MetricSpace α] [CompleteSpace α] {r : Setoid α} {A : Set α} (T : ThinRankAnalysis r A) : IsThinOn r A

Thinness. Immediate from no_cantorAntichain, since a perfect antichain would give a Cantor antichain.

def ThinRankAnalysis.of_bounded_on_cantor_antichains {X : Type u} [TopologicalSpace X] {r : Setoid X} {A : Set X} (rank : X → Ordinal.{0}) (rank_lt_omega1 : ∀ x ∈ A, rank x < Ordinal.omega 1) (fixedRankAntichains_countable : ∀ α < Ordinal.omega 1, ∀ B ⊆ A, (∀ x ∈ B, rank x = α) → (∀ x ∈ B, ∀ y ∈ B, r x y → x = y) → B.Countable) (bounded : ∀ (f : (ℕ → Bool) → X), Continuous f → (∀ (x : ℕ → Bool), f x ∈ A) → (∀ (x y : ℕ → Bool), x ≠ y → ¬r (f x) (f y)) → ∃ β < Ordinal.omega 1, ∀ (x : ℕ → Bool), rank (f x) < β) : ThinRankAnalysis r A

Compatibility with a bound on the whole antichain. A producer that can bound the rank on every Cantor antichain — the stronger, older hypothesis — is a ranked thinness analysis: take the subcopy to be the identity.

Only this direction is supplied, and no converse is claimed: a bound on some subcopy does not recover one on the whole antichain, which is exactly why the field was weakened.

A def, not a theorem: ThinRankAnalysis is evidence, not a proposition.

Equations

• One or more equations did not get rendered due to their size.