eventuallyConst_inv_set_ae — Mathlib

English

For a subset s of G, the property that s is eventually constant with respect to the a.e. measure is equivalent to the same property for the inverse set s⁻¹.

Русский

Для множества s подействие почти всей меры ae μ сохраняется под взятием обратно, то есть свойство EV Const для s равно свойству EV Const для s⁻¹.

LaTeX

$$$\mathrm{EvConst}(s^{-1}, \mathrm{ae}\,\mu) \iff \mathrm{EvConst}(s, \mathrm{ae}\,\mu)$$$

Lean4

@[to_additive (attr := simp)]
theorem eventuallyConst_inv_set_ae : EventuallyConst (s⁻¹ : Set G) (ae μ) ↔ EventuallyConst s (ae μ) := by
  rw [← inv_preimage, eventuallyConst_preimage, Filter.map_inv, inv_ae]

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