Commit 2024-09-06 16:27 329f679f

View on Github →

feat(Order/Hom): denselyOrdered_iff_of_orderIsoClass (#16427) Also add a DenselyOrdered of subsingleton types And additional API for order isos: map_inv_le_map_inv_iff map_inv_lt_map_inv_iff

Estimated changes

Modified Mathlib/Order/Basic.lean

added theorem Subsingleton.instDenselyOrdered

Modified Mathlib/Order/Hom/Basic.lean

added theorem denselyOrdered_iff_of_orderIsoClass

added theorem map_inv_le_map_inv_iff

added theorem map_inv_lt_map_inv_iff