measurable_quotient_mk''

Mathlib.MeasureTheory.MeasurableSpace.Constructions

URI: https://scilib.ai/kg/mathlib#measurable_quotient_mk''

English

The quotient map Quotient.mk'' : α → Quotient s is measurable.

Русский

Отображение Quotient.mk'' : α → Quotient s измеримо.

LaTeX

$$$\\\\operatorname{Measurable}(\\\\operatorname{Quotient.mk''} : \\\\alpha \\\\rightarrow \\\\operatorname{Quotient} s)$$$

Lean4

@[measurability]
theorem measurable_quotient_mk'' {s : Setoid α} : Measurable (Quotient.mk'' : α → Quotient s) := fun _ => id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru