union — Mathlib

English

If S1 and S2 are measurable subsets of α, then their union is measurable.

Русский

Если A и B — измеримые подмножества α, то их объединение измеримо.

LaTeX

$$$\mathrm{MeasurableSet}(s_1) \rightarrow \mathrm{MeasurableSet}(s_2) \rightarrow \mathrm{MeasurableSet}(s_1 \cup s_2)$$$

Lean4

@[simp, measurability]
protected theorem union {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) : MeasurableSet (s₁ ∪ s₂) :=
  by
  rw [union_eq_iUnion]
  exact .iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)

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