toMeasurableInv — Mathlib

English

There is a canonical MeasurableInv instance on any group with MeasurableDiv, i.e., the inverse operation is measurable.

Русский

Для любой группы с MeasurableDiv существует каноническая инстанция MeasurableInv: обращение измеримо.

LaTeX

$$$\\text{MeasurableInv}\\ α$$$

Lean4

instance (priority := 100) toMeasurableInv [MeasurableSpace α] [Group α] [MeasurableDiv α] : MeasurableInv α where
  measurable_inv := by simpa using measurable_const_div (1 : α)

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