measurableEquiv — Mathlib

English

There exists a measurable equivalence in the non-countable case extending to Cantor-like representations.

Русский

Существование измеримого эквивалента в не счётном случае в Кантороподобном представлении.

LaTeX

$$MeasurableEquiv α β$$

Lean4

/-- The **Borel Isomorphism Theorem**: If two standard Borel spaces have the same cardinality,
they are Borel isomorphic. -/
noncomputable def measurableEquiv (e : α ≃ β) : α ≃ᵐ β :=
  by
  by_cases h : Countable α
  · letI := Countable.of_equiv α e
    refine ⟨e, ?_, ?_⟩ <;> apply measurable_of_countable
  refine measurableEquivOfNotCountable h ?_
  rwa [e.countable_iff] at h

Похожие утверждения