Theorem Order.exists_between_finsets

Modification history

2024-09-09 16:04
Mathlib/Order/CountableDenseLinearOrder.lean
feat(ModelTheory/Order): Countable dense linear orders are Fraïssé limits of the class of finite linear orders (#16538) …
Modified Order.exists_between_finsetsView on Github →
2023-08-10 19:52
Mathlib/Order/CountableDenseLinearOrder.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified Order.exists_between_finsetsView on Github →
2023-02-03 10:21
Mathlib/Order/CountableDenseLinearOrder.lean
feat port : Order.CountableDenseLinearOrder (#2037)
Added Order.exists_between_finsetsView on Github →