sup_sup_distrib_right

Mathlib.Order.Lattice

URI: https://scilib.ai/kg/mathlib#sup_sup_distrib_right

English

a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c).

Русский

Правая дистрибутивность над объединением: a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c).

LaTeX

$$$a \sqcup b \sqcup c = a \sqcup c \sqcup (b \sqcup c)$$$

Lean4

theorem sup_sup_distrib_right (a b c : α) : a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c) := by rw [sup_sup_sup_comm, sup_idem]

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

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

Разделы

Аффилиация

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