measurableSet_quotient — Mathlib

English

A subset t of the quotient is measurable iff its preimage under the quotient map mk'' is measurable upstairs.

Русский

Подмножество t в притяжении кортежа измеримо тогда и только тогда, когда его прообраз при отображении mk'' измерим наверху.

LaTeX

$$$MeasurableSet t \\iff MeasurableSet (Quotient.mk''^{-1} t)$$$

Lean4

theorem measurableSet_quotient {s : Setoid α} {t : Set (Quotient s)} :
    MeasurableSet t ↔ MeasurableSet (Quotient.mk'' ⁻¹' t) :=
  Iff.rfl

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