Theorem Order.embedding_from_countable_to_dense

Modification history

2024-02-08 13:28

Mathlib/Order/CountableDenseLinearOrder.lean

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

Modified Order.embedding_from_countable_to_dense View on Github →

2023-02-03 10:21

Mathlib/Order/CountableDenseLinearOrder.lean

feat port : Order.CountableDenseLinearOrder (#2037)

Added Order.embedding_from_countable_to_dense View on Github →