union_vsub

Mathlib.Algebra.Group.Pointwise.Set.Scalar

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

English

The vsub distributes over union on the left: (s1 ∪ s2) −ᵥ t = (s1 −ᵥ t) ∪ (s2 −ᵥ t).

Русский

Разность по векторному вычитанию распределяется по объединению слева: (s1 ∪ s2) −ᵥ t = (s1 −ᵥ t) ∪ (s2 −ᵥ t).

LaTeX

$$$ (s1 \cup s2) -ᵥ t = (s1 -ᵥ t) \cup (s2 -ᵥ t) $$$

Lean4

theorem union_vsub : s₁ ∪ s₂ -ᵥ t = s₁ -ᵥ t ∪ (s₂ -ᵥ t) :=
  image2_union_left

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

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

Разделы

Аффилиация

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