English
If α is countably generated and separates points, it is measure-equivalent to a subset of the Cantor space ℕ → Bool.
Русский
Если α счетно порождено и разделяет точки, то α эквивалентно по мере подмножеству канторова пространства ℕ → Bool.
LaTeX
$$$\\exists s: Set (\\mathbb{N} \\to Bool), Nonempty (\\alpha \\simeq^\\mathrm{m} s)$$$
Lean4
/-- If a measurable space is countably generated and separates points, it is measure equivalent
to some subset of the Cantor space `ℕ → Bool` (equipped with the product sigma algebra).
Note: `s` need not be measurable, so this map need not be a `MeasurableEmbedding` to
the Cantor Space. -/
theorem measurableEquiv_nat_bool_of_countablyGenerated [MeasurableSpace α] [CountablyGenerated α] [SeparatesPoints α] :
∃ s : Set (ℕ → Bool), Nonempty (α ≃ᵐ s) :=
by
use range (mapNatBool α), Equiv.ofInjective _ <| injective_mapNatBool _,
Measurable.subtype_mk <| measurable_mapNatBool _
simp_rw [← generateFrom_natGeneratingSequence α]
apply measurable_generateFrom
rintro _ ⟨n, rfl⟩
rw [← Equiv.image_eq_preimage _ _]
refine ⟨{y | y n}, by measurability, ?_⟩
rw [← Equiv.preimage_eq_iff_eq_image]
simp [mapNatBool]
