cond — Mathlib

English

If s1 and s2 are measurable, then for any i ∈ Bool, cond i s1 s2 is measurable.

Русский

Если s1 и s2 измеримы, то для любого i ∈ Bool множество cond i s1 s2 измеримо.

LaTeX

$$$\\mathrm{MeasurableSet}(s_1) \\rightarrow \\mathrm{MeasurableSet}(s_2) \\rightarrow \\forall i \\in \\{\\text{true},\\text{false}\\}, \\mathrm{MeasurableSet}(\\mathrm{cond}\ i\ s_1\ s_2)$$$

Lean4

@[simp, measurability]
protected theorem cond {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) {i : Bool} :
    MeasurableSet (cond i s₁ s₂) := by
  cases i
  exacts [h₂, h₁]

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