Theorem OrderIso.map_succ

Modification history

2024-11-29 04:10
Mathlib/Order/SuccPred/Basic.lean
feat(Order/InitialSeg): initial segments preserve successor limits (#19053) …
Modified OrderIso.map_succView on Github →
2024-08-29 12:34
Mathlib/Order/SuccPred/Basic.lean
feat(Order/*): `CovBy` and `OrderIso` (#16222) …
Added OrderIso.map_succView on Github →