union_union_distrib_left

Mathlib.Data.Set.Basic

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

English

Let s, t, u be sets. Then s ∪ (t ∪ u) = s ∪ t ∪ (s ∪ u).

Русский

Пусть S, T, U — множества. Тогда S ∪ (T ∪ U) = S ∪ T ∪ (S ∪ U).

LaTeX

$$$s \cup (t \cup u) = s \cup t \cup (s \cup u)$$$

Lean4

theorem union_union_distrib_left (s t u : Set α) : s ∪ (t ∪ u) = s ∪ t ∪ (s ∪ u) :=
  sup_sup_distrib_left _ _ _

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

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

Разделы

Аффилиация

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