not_isPredLimit_of_noMin

Mathlib.Order.SuccPred.Limit

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

English

If there is no Min, then IsPredLimit a is false.

Русский

Если нет минимума, IsPredLimit a ложно.

LaTeX

$$¬ IsPredLimit(a)$$

Lean4

@[simp]
theorem not_isPredLimit_of_noMin : ¬IsPredLimit a := fun h ↦ h.not_isMax h.isPredPrelimit.isMax_of_noMin

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

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

Разделы

Аффилиация

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