union_right_iff — Mathlib

English

Let μ be a measure on α and s, t, u subsets of α. Then s is μ-almost everywhere disjoint from t ∪ u if and only if s is μ-a.e. disjoint from both t and u.

Русский

Пусть μ — мера на α, и s, t, u — подмножества α. Тогда s μ-близко к μ-несовместности с t ∪ u тогда и только тогда, когда s μ-близко к μ-несовместности как с t, так и с u.

LaTeX

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

Lean4

@[simp]
theorem union_right_iff : AEDisjoint μ s (t ∪ u) ↔ AEDisjoint μ s t ∧ AEDisjoint μ s u := by
  simp [union_eq_iUnion, and_comm]

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