union_vsub_inter_subset_union

Mathlib.Algebra.Group.Pointwise.Set.Scalar

URI: https://scilib.ai/kg/mathlib#Set.union_vsub_inter_subset_union

English

s1 ∪ s2 −ᵥ (t1 ∩ t2) ⊆ s1 −ᵥ t1 ∪ (s2 −ᵥ t2).

Русский

Объединение слева и пересечение справа: s1 ∪ s2 −ᵥ (t1 ∩ t2) ⊆ s1 −ᵥ t1 ∪ (s2 −ᵥ t2).

LaTeX

$$$ (s1 \cup s2) -ᵥ (t1 \cap t2) \subseteq (s1 -ᵥ t1) \cup (s2 -ᵥ t2) $$$

Lean4

theorem union_vsub_inter_subset_union : s₁ ∪ s₂ -ᵥ t₁ ∩ t₂ ⊆ s₁ -ᵥ t₁ ∪ (s₂ -ᵥ t₂) :=
  image2_union_inter_subset_union

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru