WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Well-order

Revision #2669 → #3198 · back to history

modifiedCofinal subset7e07ac34e185
FieldFrom #2669To #3198
mathlib.moduleMathlib.Order.CofinalMathlib.Order.Bounds.Defs
note`IsCofinal` defines a cofinal set in any ordered type as one with elements ≥ every element (i.e. unbounded).`IsCofinal` (in Mathlib.Order.Bounds.Defs) defines a cofinal set in any ordered type as one with elements ≥ every element (i.e. unbounded).
addedTransfinite recursion theorem4c3e616cb278