symm — Mathlib

English

If a measurable equivalence e is ergodic, then its inverse e.symm is ergodic as well.

Русский

Если измеримое эквивалентное отображение e является эргодическим, то и его обратное e.symm эргодично.

LaTeX

$$$\mathrm{Ergodic}(e, \mu) \Rightarrow \mathrm{Ergodic}(e^{-1}, \mu)$$$

Lean4

/-- If a measurable equivalence is ergodic, then so is the inverse map. -/
theorem symm {e : α ≃ᵐ α} (he : Ergodic e μ) : Ergodic e.symm μ
    where
  toMeasurePreserving := he.toMeasurePreserving.symm
  aeconst_set s hsm hs := he.aeconst_set hsm <| by conv_lhs => rw [← hs, ← e.image_eq_preimage, e.preimage_image]

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