ite — Mathlib

English

If t, s1, s2 are subsets of α with t measurable, and s1, s2 measurable, then t.ite s1 s2 is measurable.

Русский

Если t, s1, s2 — подмножества α с t измеримым, и s1, s2 измеримы, то t.ite s1 s2 измеримо.

LaTeX

$$$\\mathrm{MeasurableSet}(t) \\rightarrow \\mathrm{MeasurableSet}(s_1) \\rightarrow \\mathrm{MeasurableSet}(s_2) \\rightarrow \\mathrm{MeasurableSet}(t.\\mathrm{ite}\\ s_1\ \\, s_2)$$$

Lean4

@[simp, measurability]
protected theorem ite {t s₁ s₂ : Set α} (ht : MeasurableSet t) (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) :
    MeasurableSet (t.ite s₁ s₂) :=
  (h₁.inter ht).union (h₂.diff ht)

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