lt_top

Mathlib.Order.SuccPred.Limit

URI: https://scilib.ai/kg/mathlib#Order.IsPredLimit.lt_top

English

If a is a pred-limit, then a < ⊤.

Русский

Если a является пред-лимитом, то a < ⊤.

LaTeX

$$IsPredLimit(a) \rightarrow a < \top$$

Lean4

theorem lt_top [OrderTop α] (h : IsPredLimit a) : a < ⊤ :=
  h.ne_top.lt_top

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

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

Разделы

Аффилиация

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