ae_restrict_union_eq — Mathlib

English

For two sets s and t, the a.e. restrictions to their union equal the supremum of a.e. restrictions to each: ae(μ.restrict (s ∪ t)) = ae(μ.restrict s) ⊔ ae(μ.restrict t).

Русский

Для двух множеств выполняется равенство a.e. ограничений по их объединению и максимум ограничений по каждому из них.

LaTeX

$$$\\operatorname{ae}(\\mu\\restrict (s\\cup t)) = \\operatorname{ae}(\\mu\\restrict s) \\sqcup \\operatorname{ae}(\\mu\\restrict t).$$$

Lean4

@[simp]
theorem ae_restrict_union_eq (s t : Set α) : ae (μ.restrict (s ∪ t)) = ae (μ.restrict s) ⊔ ae (μ.restrict t) := by
  simp [union_eq_iUnion, iSup_bool_eq]

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