coe_bot

Mathlib.Order.LatticeIntervals

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

English

The bottom element of Ico(a,b) coerces to a in α.

Русский

Нижняя граница Ico(a,b) при коэрции равна a в α.

LaTeX

$$$[PartialOrder\\;α](a

Lean4

@[simp, norm_cast]
protected theorem coe_bot [PartialOrder α] (a b : α) [Fact (a < b)] : ↑(⊥ : Ico a b) = a :=
  rfl

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

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

Разделы

Аффилиация

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