measurable_quotient_mk' — Mathlib

English

Let α be a type equipped with a Setoid s. The natural quotient map from α to α ⧸ s is measurable.

Русский

Пусть α — множество с заданным отношением эквивалентности через множества s. Естественное отображение α → α ⧸ 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

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