disjSups_union_right — Mathlib

English

DisjSups distributes over union on the right: disjSups(s, t1 ∪ t2) = disjSups(s, t1) ∪ disjSups(s, t2).

Русский

DisjSups распределяется по объединению справа: disjSups(s, t1 ∪ t2) = disjSups(s, t1) ∪ disjSups(s, t2).

LaTeX

$$$ s \disjSups (t_{1} \cup t_{2}) = s \disjSups t_{1} \cup s \disjSups t_{2} $$$

Lean4

theorem disjSups_union_right : s ○ (t₁ ∪ t₂) = s ○ t₁ ∪ s ○ t₂ := by simp [disjSups, filter_union, image_union]

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