symm_iff — Mathlib

English

Symmetry: ergodicity of a measurable equivalence is equivalent to ergodicity of its inverse.

Русский

Симметрия: эргодичность измеримого эквивалентного отображения эквивалентна эргодичности его обратного отображения.

LaTeX

$$$\mathrm{Ergodic}(e^{-1}) \;\Leftrightarrow\; \mathrm{Ergodic}(e)$$$

Lean4

@[simp]
theorem symm_iff {e : α ≃ᵐ α} : Ergodic e.symm μ ↔ Ergodic e μ :=
  ⟨.symm, .symm⟩

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