union_union_union_comm

Mathlib.Data.Set.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem union_union_union_comm (s t u v : Set α) : s ∪ t ∪ (u ∪ v) = s ∪ u ∪ (t ∪ v) :=
  sup_sup_sup_comm _ _ _ _

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

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

Разделы

Аффилиация

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