isPredPrelimit_of_pred_ne

Mathlib.Order.SuccPred.Limit

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

English

There exists an a such that IsPredPrelimit(a) if h holds that ∀ b, pred b ≠ a.

Русский

Существуют такие a, что IsPredPrelimit(a) при условии ∀ b, pred b ≠ a.

LaTeX

$$∃ a, IsPredPrelimit(a)$$

Lean4

theorem isPredPrelimit_of_pred_ne (h : ∀ b, pred b ≠ a) : IsPredPrelimit a := fun b hba => h b (CovBy.pred_eq hba)

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

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

Разделы

Аффилиация

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