vsub_union — Mathlib

English

Let s, t1, t2 be finite sets in β. Then the pointwise subtraction distributes over union: s -ᵥ (t1 ∪ t2) = (s -ᵥ t1) ∪ (s -ᵥ t2).

Русский

Пусть s, t1, t2 — конечные множества в β. Тогда точечное вычитание распределяется по объединению: s -ᵥ (t1 ∪ t2) = (s -ᵥ t1) ∪ (s -ᵥ t2).

LaTeX

$$$s -ᵥ (t_1 ∪ t_2) = (s -ᵥ t_1) ∪ (s -ᵥ t_2)$$$

Lean4

theorem vsub_union : s -ᵥ (t₁ ∪ t₂) = s -ᵥ t₁ ∪ (s -ᵥ t₂) :=
  image₂_union_right

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