IsPredLimit — Mathlib

English

A predecessor limit is a value that is not maximal and is a predecessor-prelimit.

Русский

Предпределенный предел — величина, которая не максимальна и является предпредлимитом.

LaTeX

$$$IsPredLimit(a) \equiv (\neg IsMax(a)) \land IsPredPrelimit(a)$$$

Lean4

/-- A predecessor limit is a value that isn't maximal and doesn't cover any other.

It's so named because in a predecessor order, a predecessor limit can't be the predecessor of
anything larger.

This previously allowed the element to be maximal. This usage is now covered by `IsPredPreLimit`. -/
def IsPredLimit (a : α) : Prop :=
  ¬IsMax a ∧ IsPredPrelimit a

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