isMin_iff_forall_not_lt

Mathlib.Order.Max

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

English

IsMin a iff for all b, not a < b.

Русский

IsMin a эквивалентно тому, что для всех b выполняется ¬(a < b).

LaTeX

$$$\\\\mathrm{IsMin}(a) \\\\leftrightarrow \\\\forall b, \\\\lnot (a < b)$$$

Lean4

theorem isMin_iff_forall_not_lt : IsMin a ↔ ∀ b, ¬b < a :=
  ⟨fun h _ => h.not_lt, fun h _ hba => of_not_not fun hab => h _ <| hba.lt_of_not_ge hab⟩

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

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

Разделы

Аффилиация

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