isSuccPrelimit

Mathlib.Order.SuccPred.Limit

URI: https://scilib.ai/kg/mathlib#IsMin.isSuccPrelimit

English

If IsMin a then IsSuccPrelimit a.

Русский

Если a минимален, то он является предлимитом.

LaTeX

$$IsMin(a) \rightarrow IsSuccPrelimit(a)$$

Lean4

protected theorem _root_.IsMin.isSuccPrelimit : IsMin a → IsSuccPrelimit a := fun h _ hab => not_isMin_of_lt hab.lt h

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

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

Разделы

Аффилиация

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