measurableSpace — Mathlib

English

The quotient G/S of a group G by a subgroup S carries a natural measurable space structure, and the quotient map is measurable.

Русский

Квартирация G/S группы G по подгруппе S оснащена естественной структурой измеримости, и проекция измерима.

LaTeX

$$QuotientGroup.measurableSpace(S) = Quotient.instMeasurableSpace$$

Lean4

@[to_additive]
instance measurableSpace {G} [Group G] [MeasurableSpace G] (S : Subgroup G) : MeasurableSpace (G ⧸ S) :=
  Quotient.instMeasurableSpace

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