Thinness transport through canonical expansions

The expansion code morleyCode Φ is a measurable embedding (measurableEmbedding_morleyCode) that preserves and reflects isomorphism (morleyCode_iso_iff), so antichain transport applies: a class of base codes is thin for isomorphism iff its class of canonical expansion codes is (isThinOn_morleyCode_image_iff), and likewise for Cantor antichains. The class need not be Borel. Nothing about continuity of the expansion code, the logic topology, or spectra is used.

theorem FirstOrder.Language.hasCantorAntichainOn_morleyCode_image_iff {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} [Countable ↑Φ] (C : Set L.StructureSpace) : HasCantorAntichainOn (L.morleyize Φ).structureIsoSetoid (morleyCode Φ '' C) ↔ HasCantorAntichainOn L.structureIsoSetoid C

Cantor antichains transport through the expansion code, in both directions.

theorem FirstOrder.Language.isThinOn_morleyCode_image_iff {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {Φ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} [Countable ↑Φ] (C : Set L.StructureSpace) : IsThinOn (L.morleyize Φ).structureIsoSetoid (morleyCode Φ '' C) ↔ IsThinOn L.structureIsoSetoid C

Thinness transport: a class of base codes is thin iff its class of canonical expansion codes is. No Borelness of the class is assumed.