diffs_union_left

Mathlib.Data.Finset.Sups

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

English

The difference of a union distributes over t: (s1 ∪ s2) \\ t = (s1 \\ t) ∪ (s2 \\ t).

Русский

Разности объединения распределяются по t: (s1 ∪ s2) \\ t = (s1 \\ t) ∪ (s2 \\ t).

LaTeX

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

Lean4

theorem diffs_union_left : (s₁ ∪ s₂) \\ t = s₁ \\ t ∪ s₂ \\ t :=
  image₂_union_left

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

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

Разделы

Аффилиация

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