measurableInv — Mathlib

English

If γ has a continuous inverse, then the inversion map x ↦ x^{-1} is measurable.

Русский

Если в γ имеется непрерывное обращение, то отображение инверсии x ↦ x^{-1} измеримо.

LaTeX

$$$\\mathrm{MeasurableInv}(\\gamma)\\quad\\text{from }[Inv\\,\\gamma][ContinuousInv\\gamma],\\ \\mathrm{Measurable}(\\lambda x:\\gamma, x^{-1}).$$$

Lean4

@[to_additive]
instance (priority := 100) measurableInv [Inv γ] [ContinuousInv γ] : MeasurableInv γ :=
  ⟨continuous_inv.measurable⟩

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