lt_top'

Mathlib.Order.BoundedOrder.Basic

URI: https://scilib.ai/kg/mathlib#Ne.lt_top'

English

Let α be a type with a partial order and a top element ⊤. If ⊤ ≠ a, then a < ⊤.

Русский

Пусть имеется множества с частичным порядком и верхним элементом ⊤. Если ⊤ ≠ a, то a < ⊤.

LaTeX

$$$\forall a:\\alpha,\ top \neq a \rightarrow a < \top$$$

Lean4

theorem lt_top' (h : ⊤ ≠ a) : a < ⊤ :=
  h.symm.lt_top

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

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

Разделы

Аффилиация

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