IsPredPrelimit

Mathlib.Order.SuccPred.Limit

URI: https://scilib.ai/kg/mathlib#Order.IsPredPrelimit

Lean4

/-- A predecessor pre-limit is a value that isn't covered by any other.

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

Use `IsPredLimit` to exclude the case of a maximal element. -/
def IsPredPrelimit (a : α) : Prop :=
  ∀ b, ¬a ⋖ b

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru