isSuccPrelimit_iff_of_noMax

Mathlib.Order.SuccPred.Limit

URI: https://scilib.ai/kg/mathlib#Order.isSuccPrelimit_iff_of_noMax

English

IsSuccPrelimit a iff IsMin a under suitable hypotheses.

Русский

При некоторых условиях IsSuccPrelimit a эквивалентно IsMin a.

LaTeX

$$$IsSuccPrelimit(a) \leftrightarrow IsMin(a)$$$

Lean4

@[simp]
theorem isSuccPrelimit_iff_of_noMax : IsSuccPrelimit a ↔ IsMin a :=
  ⟨IsSuccPrelimit.isMin_of_noMax, IsMin.isSuccPrelimit⟩

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

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

Разделы

Аффилиация

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