not_isMin

Mathlib.Order.Max

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

English

In a nontrivial preorder, a top element cannot be a bottom element.

Русский

В неtrивиальном порядке верхний элемент не может быть нижним.

LaTeX

$$$\\forall {\\alpha : Type*} [PartialOrder \\alpha] [Nontrivial \\alpha], IsTop a \\rightarrow \\neg IsMin a$$$

Lean4

protected theorem not_isMin [Nontrivial α] (ha : IsTop a) : ¬IsMin a :=
  ha.toDual.not_isMax

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

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

Разделы

Аффилиация

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