coe_sup

Mathlib.Order.LatticeIntervals

URI: https://scilib.ai/kg/mathlib#Set.Iic.coe_sup

English

The supremum in Iic(a) projects to the supremum in α.

Русский

Супремум в Iic(a) проецируется на супремум в α.

LaTeX

$$$[SemilatticeSup\\alpha] {a:\\alpha} {x,y:\\mathrm{Iic}\\;a} : \\uparrow(x\\sqcup y) = \\uparrow x \\sqcup \\uparrow y$$$

Lean4

@[simp, norm_cast]
protected theorem coe_sup [SemilatticeSup α] {x y : Iic a} : ↑(x ⊔ y) = (↑x ⊔ ↑y : α) :=
  rfl

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

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

Разделы

Аффилиация

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