not_isPredLimit

Mathlib.Order.SuccPred.Limit

URI: https://scilib.ai/kg/mathlib#IsMax.not_isPredLimit

English

If a is maximal, then a is not a predecessor-limit.

Русский

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

LaTeX

$$$IsMax(a) \Rightarrow \neg IsPredLimit(a)$$$

Lean4

protected theorem _root_.IsMax.not_isPredLimit (h : IsMax a) : ¬IsPredLimit a := fun ha ↦ ha.not_isMax h

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

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

Разделы

Аффилиация

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