union_right — Mathlib

English

If s is μ-a.e. disjoint from t and μ-a.e. disjoint from u, then s is μ-a.e. disjoint from t ∪ u.

Русский

Если s диссоциален с t и с u почти во всём отношении по μ, то s диссоциален и с t ∪ u почти во всём отношении по μ.

LaTeX

$$$\\\\operatorname{AEDisjoint} \\\\mu s t \\\\land \\\\operatorname{AEDisjoint} \\\\mu s u \\\Rightarrow \\\\operatorname{AEDisjoint} \\\\mu s (t \\\\cup u)$$$

Lean4

theorem union_right (ht : AEDisjoint μ s t) (hu : AEDisjoint μ s u) : AEDisjoint μ s (t ∪ u) :=
  union_right_iff.2 ⟨ht, hu⟩

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