not_isSuccLimit

Mathlib.Order.SuccPred.Limit

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

English

If IsMin a, then not IsSuccLimit a.

Русский

Если a минимален, то он не является пределом следующего элемента.

LaTeX

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

Lean4

protected theorem _root_.IsMin.not_isSuccLimit (h : IsMin a) : ¬IsSuccLimit a := fun ha ↦ ha.not_isMin h

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

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

Разделы

Аффилиация

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