inter_vsub_subset — Mathlib

English

The vsub of an intersection is contained in the intersection of vsubs: s1 ∩ s2 −ᵥ t ⊆ (s1 −ᵥ t) ∩ (s2 −ᵥ t).

Русский

Разность по векторному вычитанию пересечения содержится в пересечении соответствующих разностей: s1 ∩ s2 −ᵥ t ⊆ (s1 −ᵥ t) ∩ (s2 −ᵥ t).

LaTeX

$$$ s1 \cap s2 -ᵥ t \subseteq (s1 -ᵥ t) \cap (s2 -ᵥ t) $$$

Lean4

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

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