Transporting antichains across a measurable embedding

A measurable embedding g : X → Y between Polish spaces that preserves and reflects two equivalence relations (r' (g x) (g y) ↔ r x y) transports Cantor antichains in both directions (hasCantorAntichainOn_image_iff), hence thinness (isThinOn_image_iff). The ambient class A need not be Borel, and neither relation need be Borel: only the witnesses are Borel.

The argument transports a Borel witness and then extracts a new Cantor copy; it does not claim that any composed map is continuous. Forward: the image under g of the range of a Cantor antichain is an uncountable Borel set (Lusin–Souslin, through the measurable embedding) of pairwise inequivalent points, so it contains a Cantor copy (MeasurableSet.exists_nat_bool_injection_of_not_countable), which is a Cantor antichain in the image class. Backward: the preimage under g of the range of a Cantor antichain in the image is an uncountable Borel subset of A of pairwise inequivalent points, and the same extraction applies.

Ambient Polish spaces and Cantor-copy extraction are used; no logic topology and no spectrum characterization.

theorem hasCantorAntichainOn_image_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {r : Setoid X} {r' : Setoid Y} {g : X → Y} (hg : MeasurableEmbedding g) (hrel : ∀ (x y : X), r' (g x) (g y) ↔ r x y) (A : Set X) : HasCantorAntichainOn r' (g '' A) ↔ HasCantorAntichainOn r A

Antichain transport, both directions. For a measurable embedding preserving and reflecting the relations, the image class carries a Cantor antichain iff the class does.

theorem isThinOn_image_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {r : Setoid X} {r' : Setoid Y} {g : X → Y} (hg : MeasurableEmbedding g) (hrel : ∀ (x y : X), r' (g x) (g y) ↔ r x y) (A : Set X) : IsThinOn r' (g '' A) ↔ IsThinOn r A

Thinness transport. In Polish ambient spaces perfect and Cantor antichains coincide, so the image class is thin iff the class is.