isSuccPrelimit_of_succ_ne — Mathlib

English

If every successor is different from a fixed element a, then a is a succ-prelimit.

Русский

Если для всех b выполняется succ(b) ≠ a, то a является succ-предпределом.

LaTeX

$$$\forall \alpha\, (\text{PartialOrder } \alpha) \land (\text{SuccOrder } \alpha) \Rightarrow (\forall a, (\forall b, succ(b) \neq a) \Rightarrow IsSuccPrelimit(a))$$$

Lean4

theorem isSuccPrelimit_of_succ_ne (h : ∀ b, succ b ≠ a) : IsSuccPrelimit a := fun b hba => h b (CovBy.succ_eq hba)

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