not_isMin_iff

Mathlib.Order.Max

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

English

Not IsMin a iff there exists b with b < a.

Русский

Не IsMin a эквивалентно существованию b, такого что b < a.

LaTeX

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

Lean4

@[simp]
theorem not_isMin_iff : ¬IsMin a ↔ ∃ b, b < a := by simp [lt_iff_le_not_ge, IsMin, not_forall]

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

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

Разделы

Аффилиация

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