isPredLimit — Mathlib

English

In a linear order, a is not a predecessor-prelimit iff there exists b with a ⋖ b.

Русский

В линейном порядке a не является пред-предлимитом тогда и только тогда, когда существует b, такой что a ⋖ b.

LaTeX

$$$\neg IsPredPrelimit(a) \iff \exists b, a \⋖ b$$$

Lean4

theorem isPredLimit [NoMaxOrder α] (h : IsPredPrelimit a) : IsPredLimit a :=
  h.isPredLimit_of_not_isMax (not_isMax a)

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