lt_of_ne

Mathlib.Order.Max

URI: https://scilib.ai/kg/mathlib#IsTop.lt_of_ne

English

If a is top and b ≠ a, then b < a.

Русский

Если a является топ, и b ≠ a, тогда b < a.

LaTeX

$$$\\forall {\\alpha : Type*} [inst : PartialOrder \\alpha] {a b : \\alpha}, IsTop a \\rightarrow Ne b a \\rightarrow b < a$$$

Lean4

protected theorem lt_of_ne (ha : IsTop a) (h : b ≠ a) : b < a :=
  (ha b).lt_of_ne h

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

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

Разделы

Аффилиация

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