vsub_inter_subset — Mathlib

English

For finite sets s, t1, t2, the subtraction over the intersection is contained in the intersection of the subtractions: s -ᵥ (t1 ∩ t2) ⊆ (s -ᵥ t1) ∩ (s -ᵥ t2).

Русский

Для конечных множеств s, t1, t2 вычитание по пересечению включено в пересечение вычитаний: s -ᵥ (t1 ∩ t2) ⊆ (s -ᵥ t1) ∩ (s -ᵥ t2).

LaTeX

$$$s -ᵥ (t_1 \\cap t_2) \\subseteq (s -ᵥ t_1) \\cap (s -ᵥ t_2)$$$

Lean4

theorem vsub_inter_subset : s -ᵥ t₁ ∩ t₂ ⊆ (s -ᵥ t₁) ∩ (s -ᵥ t₂) :=
  image₂_inter_subset_right

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