instMeasurableSpace — Mathlib

English

The group of units Mˣ carries a canonical measurable space structure given by pulling back along the valuation map val: Mˣ → M.

Русский

Группа единиц Mˣ несет каноническую структуру измеримого пространства, получаемую посредством вытягивания через отображение значения val: Mˣ → M.

LaTeX

$$$\\text{MeasurableSpace}(M^{\\times}) := \\text{MeasurableSpace.comap}(\\mathrm{val},\\, \\text{MeasurableSpace}(M))$$$

Lean4

@[to_additive]
instance instMeasurableSpace : MeasurableSpace Mˣ :=
  .comap Units.val ‹_›

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