instDiscreteMeasurableSpace — Mathlib

English

There is a discrete measurable space structure on the quotient G ⧸ S.

Русский

На факторном пространстве G ⧸ S задана дискретная измеримая структура.

LaTeX

$$$\\text{DiscreteMeasurableSpace}(G \\nobreakdash/ S)$$$

Lean4

instance instDiscreteMeasurableSpace {α} {s : Setoid α} [MeasurableSpace α] [DiscreteMeasurableSpace α] :
    DiscreteMeasurableSpace (Quotient s) where forall_measurableSet _ := measurableSet_quotient.2 .of_discrete

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