inter_vsub_subset — Mathlib

English

For finite sets s1, s2 and t, the pointwise subtraction distributes over intersection in the sense of subset: (s1 ∩ s2) -ᵥ t ⊆ (s1 -ᵥ t) ∩ (s2 -ᵥ t).

Русский

Для конечных множеств s1, s2 и t точечное вычитание распределяется по пересечению в смысле подмножества: (s1 ∩ s2) -ᵥ t ⊆ (s1 -ᵥ t) ∩ (s2 -ᵥ t).

LaTeX

$$$(s_1 \\cap s_2) -ᵥ t \\subseteq (s_1 -ᵥ t) \\cap (s_2 -ᵥ t)$$$

Lean4

theorem inter_vsub_subset : s₁ ∩ s₂ -ᵥ t ⊆ (s₁ -ᵥ t) ∩ (s₂ -ᵥ t) :=
  image₂_inter_subset_left

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