Def Order.PartialIso

Modification history

2023-02-03 10:21
Mathlib/Order/CountableDenseLinearOrder.lean
feat port : Order.CountableDenseLinearOrder (#2037)
Added Order.PartialIsoView on Github →