Ici_sup

Mathlib.Order.UpperLower.Principal

URI: https://scilib.ai/kg/mathlib#UpperSet.Ici_sup

English

The principal upper set distributes over binary joins: Ici(a ⊔ b) = Ici(a) ⊔ Ici(b).

Русский

Главная верхняя множество распределяется по обобщению: Ici(a ⊔ b) = Ici(a) ⊔ Ici(b).

LaTeX

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

Lean4

@[simp]
theorem Ici_sup [SemilatticeSup α] (a b : α) : Ici (a ⊔ b) = Ici a ⊔ Ici b :=
  ext Ici_inter_Ici.symm

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

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

Разделы

Аффилиация

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