isSuccPrelimit_iff_isSuccLimit_of_not_isMin

Mathlib.Order.SuccPred.Limit

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

← MathLib Explorer

English

If a is not minimal, then IsSuccPrelimit a iff IsSuccLimit a.

Русский

Если a не минимален, то IsSuccPrelimit a эквивалентно IsSuccLimit a.

LaTeX

$$$(\neg IsMin(a)) \rightarrow (IsSuccPrelimit(a) \leftrightarrow IsSuccLimit(a))$$$

Lean4

theorem isSuccPrelimit_iff_isSuccLimit_of_not_isMin (h : ¬IsMin a) : IsSuccPrelimit a ↔ IsSuccLimit a :=
  ⟨fun ha ↦ ha.isSuccLimit_of_not_isMin h, IsSuccLimit.isSuccPrelimit⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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