diffs_union_right

Mathlib.Data.Finset.Sups

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

English

The difference of a right-hand union distributes over s: s \\ (t1 ∪ t2) = (s \\ t1) ∪ (s \\ t2).

Русский

Разность по правому объединению распределяется: s \\ (t1 ∪ t2) = (s \\ t1) ∪ (s \\ t2).

LaTeX

$$$ s \\ (t_1 \\cup t_2) = (s \\ t_1) \\cup (s \\ t_2) $$$

Lean4

theorem diffs_union_right : s \\ (t₁ ∪ t₂) = s \\ t₁ ∪ s \\ t₂ :=
  image₂_union_right

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

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

Разделы

Аффилиация

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