union_left — Mathlib

English

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

Русский

Если множества s и t по отношению к μ являются μ-почти что несопоставимыми с u, то s ∪ t также μ-почти что несопоставимо с u.

LaTeX

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

Lean4

theorem union_left (hs : AEDisjoint μ s u) (ht : AEDisjoint μ t u) : AEDisjoint μ (s ∪ t) u :=
  union_left_iff.mpr ⟨hs, ht⟩

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