Commit 2024-02-08 13:28 71b03a20

View on Github →

chore(CountableDenseLinearOrder): Encodable -> Countable (#10308)

Estimated changes

Modified Mathlib/Order/CountableDenseLinearOrder.lean

modified theorem Order.embedding_from_countable_to_dense

modified theorem Order.iso_of_countable_dense