inv — Mathlib

English

If f is AEStronglyMeasurable and the target is a group with inversion, then the inverse function x ↦ f(x)⁻¹ is AEStronglyMeasurable.

Русский

Если f является AEStronglyMeasurable и целевое пространство образовано группой с инверсией, то функция x ↦ f(x)⁻¹ тоже AEStronglyMeasurable.

LaTeX

$$$AEStronglyMeasurable\ f\ μ \rightarrow AEStronglyMeasurable\left(f^{-1}\right) μ$$$

Lean4

@[to_additive (attr := fun_prop, measurability)]
protected theorem inv [Inv β] [ContinuousInv β] (hf : AEStronglyMeasurable[m] f μ) : AEStronglyMeasurable[m] f⁻¹ μ :=
  ⟨(hf.mk f)⁻¹, hf.stronglyMeasurable_mk.inv, hf.ae_eq_mk.inv⟩

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