Theorem OrderIso.isMin_apply

Modification history

2025-12-18 18:46
Mathlib/Order/Hom/Basic.lean
feat(Order/Hom/Basic): use `to_dual` (#33036) …
Deleted OrderIso.isMin_applyView on Github →
2024-08-29 12:34
Mathlib/Order/Hom/Basic.lean
feat(Order/*): `CovBy` and `OrderIso` (#16222) …
Added OrderIso.isMin_applyView on Github →