isSuccLimit_iff — Mathlib

English

If the order has a bottom element, then IsSuccLimit a holds exactly when a is not the bottom and a is a succ-prelimit.

Русский

Если в порядке есть нулевой элемент, то IsSuccLimit a выполняется тогда и только тогда, когда a не равен нижнему пределу и a является succ-предпределом.

LaTeX

$$$\forall \alpha\, (\text{PartialOrder } \alpha) \land (\text{OrderBot } \alpha) \Rightarrow IsSuccLimit(a) \leftrightarrow (a \neq \bot) \land IsSuccPrelimit(a)$$$

Lean4

theorem isSuccLimit_iff [OrderBot α] : IsSuccLimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a := by rw [IsSuccLimit, isMin_iff_eq_bot]

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