Theorems · Definition · order theory

Order.IsSuccPrelimit

{α : Type u_1} → [LT α] → α → Prop

A successor pre-limit is a value that doesn't cover any other. It's so named because in a successor order, a successor pre-limit can't be the successor of anything smaller. Use IsSuccLimit if you want to exclude the case of a minimal element.

Defined in

Mathlib.Order.SuccPred.Limit

Cited by

157 results in Mathlib

Foundations

Depth 3 from the axioms, rests on 7 definitions · uses no axioms

Assumes

LT