Theorem Order.PartialIso.exists_across

Modification history

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