coe_inf

Mathlib.Order.LatticeIntervals

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

English

The infimum in Ico(a,b) projects to the infimum in α.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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