sups_union_right

Mathlib.Data.Finset.Sups

URI: https://scilib.ai/kg/mathlib#Finset.sups_union_right

English

Sups distribute over union on the left: (s₁ ∪ s₂) ⊻ t = (s₁ ⊻ t) ∪ (s₂ ⊻ t).

Русский

Распределение сумм по левой объединению: (s₁ ∪ s₂) ⊻ t = (s₁ ⊻ t) ∪ (s₂ ⊻ t).

LaTeX

$$$ (s_1 \cup s_2) \oplus t = (s_1 \oplus t) \cup (s_2 \oplus t) $$$

Lean4

theorem sups_union_right : s ⊻ (t₁ ∪ t₂) = s ⊻ t₁ ∪ s ⊻ t₂ :=
  image₂_union_right

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

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

Разделы

Аффилиация

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