union_left_comm

Mathlib.Data.Finset.Lattice.Basic

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

English

Left-commutativity of union: S ∪ (T ∪ U) = T ∪ (S ∪ U).

Русский

Лево-центрическая перестановка объединения: S ∪ (T ∪ U) = T ∪ (S ∪ U).

LaTeX

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

Lean4

theorem union_left_comm (s t u : Finset α) : s ∪ (t ∪ u) = t ∪ (s ∪ u) :=
  ext fun _ => by simp only [mem_union, or_left_comm]

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

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

Разделы

Аффилиация

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