not_isSuccPrelimit_of_noMax — Mathlib

English

In a preorder with a successor operation, if there is no minimal element, then no element can be a succ-prelimit. In particular, IsSuccPrelimit a is false for every a.

Русский

В предпорядке с операции successor, если отсутствует минимальный элемент, то не существует предела предшествующего элемента; для каждого a выполняется ¬IsSuccPrelimit a.

LaTeX

$$$\forall \alpha\, (\text{Preorder } \alpha) \land (\text{SuccOrder } \alpha) \land (\text{IsSuccArchimedean } \alpha) \land (\text{NoMinOrder } \alpha) \Rightarrow \forall a:\alpha, \neg IsSuccPrelimit(a)$$$

Lean4

theorem not_isSuccPrelimit_of_noMax [NoMinOrder α] : ¬IsSuccPrelimit a := by simp

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