not_isMin

Mathlib.Order.Max

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

English

If there is no minimal element, then no element is minimal.

Русский

Если минимального элемента не существует, то никакой элемент не минимален.

LaTeX

$$$[NoMinOrder\\\\,\\\\alpha] \\\\Rightarrow \\\\lnot \\\\mathrm{IsMin}(a)$$$

Lean4

@[simp]
theorem not_isMin [NoMinOrder α] (a : α) : ¬IsMin a :=
  not_isMin_iff.2 <| exists_lt a

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

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

Разделы

Аффилиация

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