coe_inf

Mathlib.Order.LatticeIntervals

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

English

The infimum is preserved by the inclusion: the infimum of x and y in Ici a maps to the infimum of their images in α.

Русский

Сохранение инфа: инфimum x и y в Ici a отображается в α как их инфimum.

LaTeX

$$$$\\uparrow (x \\wedge y) = \\uparrow x \\wedge \\uparrow y.$$$$

Lean4

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

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

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

Разделы

Аффилиация

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