not_isTop

Mathlib.Order.Max

URI: https://scilib.ai/kg/mathlib#not_isTop

English

In a type with NoTopOrder, no element is top; i.e., for every a, there exists y with a < y.

Русский

В типе с NoTopOrder нет верхнего элемента; для каждого a существует y такой, что a < y.

LaTeX

$$$\forall a \in \alpha:\, \neg \mathrm{IsTop}(a)$$$

Lean4

@[simp]
theorem not_isTop [NoTopOrder α] (a : α) : ¬IsTop a := fun h =>
  let ⟨_, hb⟩ := exists_not_le a
  hb <| h _

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

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

Разделы

Аффилиация

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