not_isPredLimit_iff

Mathlib.Order.SuccPred.Limit

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

English

¬IsPredLimit a iff IsMax a or ¬IsPredPrelimit a.

Русский

Не является пред-лимитом тогда и только тогда, когда либо максимум, либо не пред-предлимит.

LaTeX

$$$\neg IsPredLimit(a) \iff IsMax(a) \lor \neg IsPredPrelimit(a)$$$

Lean4

theorem not_isPredLimit_iff : ¬IsPredLimit a ↔ IsMax a ∨ ¬IsPredPrelimit a := by rw [IsPredLimit, not_and_or, not_not]

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

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

Разделы

Аффилиация

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