sups_sups_sups_comm

Mathlib.Data.Finset.Sups

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

English

For Finsets s, t, u, v in a semilattice, s ⊻ t ⊻ (u ⊻ v) = s ⊻ u ⊻ (t ⊻ v).

Русский

Для Finset s, t, u, v в полуприсоединённой решётке: s ⊻ t ⊻ (u ⊻ v) = s ⊻ u ⊻ (t ⊻ v).

LaTeX

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

Lean4

theorem sups_sups_sups_comm : s ⊻ t ⊻ (u ⊻ v) = s ⊻ u ⊻ (t ⊻ v) :=
  image₂_image₂_image₂_comm sup_sup_sup_comm

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

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

Разделы

Аффилиация

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