Commit 2023-02-03 10:21 d2943ca8

View on Github →

feat port : Order.CountableDenseLinearOrder (#2037)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/CountableDenseLinearOrder.lean

added def Order.PartialIso.definedAtLeft

added def Order.PartialIso.definedAtRight

added theorem Order.PartialIso.exists_across

added def Order.PartialIso.funOfIdeal

added def Order.PartialIso.invOfIdeal

added def Order.PartialIso

added theorem Order.embedding_from_countable_to_dense

added theorem Order.exists_between_finsets

added theorem Order.iso_of_countable_dense