inv — Mathlib

English

If f is strongly measurable and β has a continuous inverse, then f⁻¹ is strongly measurable.

Русский

Если f сильно измерима и в β есть непрерывное обратное, тогда f⁻¹ сильно измерима.

LaTeX

$$$\text{StronglyMeasurable}(f) \Rightarrow \text{StronglyMeasurable}(f^{-1})$$$

Lean4

@[to_additive (attr := fun_prop, measurability)]
protected theorem inv [Inv β] [ContinuousInv β] (hf : StronglyMeasurable f) : StronglyMeasurable f⁻¹ :=
  ⟨fun n => (hf.approx n)⁻¹, fun x => (hf.tendsto_approx x).inv⟩

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