isSuccLimit

Mathlib.Order.SuccPred.Limit

URI: https://scilib.ai/kg/mathlib#Order.IsSuccPrelimit.isSuccLimit

English

If there is no minimum in the order, then IsSuccPrelimit a implies IsSuccLimit a.

Русский

Если в порядке отсутствует минимум, то IsSuccPrelimit a влечёт IsSuccLimit a.

LaTeX

$$$IsSuccPrelimit(a) \rightarrow IsSuccLimit(a)$$$

Lean4

theorem isSuccLimit [NoMinOrder α] (h : IsSuccPrelimit a) : IsSuccLimit a :=
  h.isSuccLimit_of_not_isMin (not_isMin a)

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

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

Разделы

Аффилиация

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