isPredLimit_of_not_isMax

Mathlib.Order.SuccPred.Limit

URI: https://scilib.ai/kg/mathlib#Order.IsPredPrelimit.isPredLimit_of_not_isMax

English

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

Русский

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

LaTeX

$$$IsPredPrelimit(a) \rightarrow (\neg IsMax(a) \rightarrow IsPredLimit(a))$$$

Lean4

theorem isPredLimit_of_not_isMax (h : IsPredPrelimit a) (ha : ¬IsMax a) : IsPredLimit a :=
  ⟨ha, h⟩

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

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

Разделы

Аффилиация

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