Theorems · Inductive type · order theory

Order.IsSuccLimit

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

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

Defined in

Mathlib.Order.SuccPred.Limit

Cited by

255 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

Preorder