toMeasurableEquiv — Mathlib

English

A homeomorphism between two Borel spaces induces a measurable equivalence.

Русский

Гомеоморфизм между двумя борелевскими пространствами порождает измеримое эквивалентное отображение.

LaTeX

$$$\\text{toMeasurableEquiv}(h):\\gamma\\to^\\sim\\gamma_2$ является измеримым эквивалентом.$$

Lean4

/-- A homeomorphism between two Borel spaces is a measurable equivalence. -/
def toMeasurableEquiv (h : γ ≃ₜ γ₂) : γ ≃ᵐ γ₂
    where
  measurable_toFun := h.measurable
  measurable_invFun := h.symm.measurable
  toEquiv := h.toEquiv

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