ne_top

Mathlib.Order.SuccPred.Limit

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

English

If a is a pred-limit, then a is not equal to ⊤.

Русский

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

LaTeX

$$$a \neq \top$$$

Lean4

theorem ne_top [OrderTop α] (h : IsPredLimit a) : a ≠ ⊤ :=
  h.dual.ne_bot

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

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

Разделы

Аффилиация

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