aemeasurable_inv_iff — Mathlib

English

AEMeasurable of inversion is equivalent to AEMeasurable of the original function when the inverse is involutive.

Русский

AЕ-мераемость обращения эквивалентна AЕМераемости исходной функции при инволютивной инверсии.

LaTeX

$$$AEMeasurable\\ (f^{-1})\\mu \\iff AEMeasurable\\ f\\mu$$$

Lean4

@[to_additive (attr := simp)]
theorem aemeasurable_inv_iff {G : Type*} [InvolutiveInv G] [MeasurableSpace G] [MeasurableInv G] {f : α → G} :
    AEMeasurable (fun x => (f x)⁻¹) μ ↔ AEMeasurable f μ :=
  ⟨fun h => by simpa only [inv_inv] using h.inv, fun h => h.inv⟩

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