Theorem OrderIso.map_pred

Modification history

2026-03-21 08:07
Mathlib/Order/SuccPred/Basic.lean
chore(Order/SuccPred/Basic): use `to_dual` more (#36612) …
Deleted OrderIso.map_predView on Github →
2024-08-29 12:34
Mathlib/Order/SuccPred/Basic.lean
feat(Order/*): `CovBy` and `OrderIso` (#16222) …
Added OrderIso.map_predView on Github →