ne_top_of_le_ne_top

Mathlib.Order.BoundedOrder.Basic

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

English

If b ≠ ⊤ and a ≤ b, then a ≠ ⊤ in any ordered set with top.

Русский

Если b ≠ ⊤ и a ≤ b, то a ≠ ⊤ в любом упорядоченном множестве с верхним элементом.

LaTeX

$$$\forall a,b:\\alpha,\ (a \le b) \land (b \neq \top) \rightarrow a \neq \top$$$

Lean4

theorem ne_top_of_le_ne_top (hb : b ≠ ⊤) (hab : a ≤ b) : a ≠ ⊤ :=
  (hab.trans_lt hb.lt_top).ne

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

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

Разделы

Аффилиация

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