inv_apply — Mathlib

English

For μ on G with InvolutiveInv and MeasurableInv, Inv.inv is a measurable equivalence and map-invariant.

Русский

Инверсия является измеримым биекцияm и сохраняет меру.

LaTeX

$$$(\text{MeasurableInv } G) \land (\text{InvolutiveInv } G) \Rightarrow \text{MeasurePreserving}(Inv.inv,\mu,\mu)$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_apply (μ : Measure G) (s : Set G) : μ.inv s = μ s⁻¹ :=
  (MeasurableEquiv.inv G).map_apply s

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