measurableSet_sum_iff — Mathlib

English

A set s ⊆ α ⊕ β is measurable if and only if its preimages under Sum.inl and Sum.inr are measurable.

Русский

Множество s ⊆ α ⊕ β измеримо тогда, когда измеримы его предобраза при Sum.inl и Sum.inr.

LaTeX

$$$\\mathrm{MeasurableSet}(s) \\iff \\mathrm{MeasurableSet}(\\mathrm{Sum.inl}^{-1}(s)) \\land \\mathrm{MeasurableSet}(\\mathrm{Sum.inr}^{-1}(s))$$$

Lean4

theorem measurableSet_sum_iff {s : Set (α ⊕ β)} :
    MeasurableSet s ↔ MeasurableSet (Sum.inl ⁻¹' s) ∧ MeasurableSet (Sum.inr ⁻¹' s) :=
  Iff.rfl

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