coe_inf

Mathlib.Order.LatticeIntervals

URI: https://scilib.ai/kg/mathlib#Set.Iio.coe_inf

English

The infimum in Iio(a) projects to the infimum in α.

Русский

Инфинум в Iio(a) проецируется на инфинум в α.

LaTeX

$$$[SemilatticeInf\\;α] {a:\\alpha} {x,y:\\mathrm{Iio}\\;a} : \\uparrow(x\\inf y) = \\uparrow x \\inf \\uparrow y$$$

Lean4

@[simp, norm_cast]
protected theorem coe_inf [SemilatticeInf α] {a : α} {x y : Iio a} : ↑(x ⊓ y) = (↑x ⊓ ↑y : α) :=
  rfl

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

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

Разделы

Аффилиация

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