measurable_inv_iff — Mathlib

English

If the group G has an involutive inverse, then inversion is measurable iff the original function is measurable.

Русский

Если у группы G есть инволютивное обращение, то обращение измеримо тогда и только тогда, когда исходная функция измерима.

LaTeX

$$$(\\text{Measurable}(f^{-1})) \\iff \\text{Measurable}(f)$$$

Lean4

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

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