Mathlib v3 is deprecated. Go to Mathlib v4

Def is_strict_weak_order_of_is_order_connected

Modification history

2018-01-11 23:22
order/basic.lean
doc(*): blurbs galore …
Deleted is_strict_weak_order_of_is_order_connectedView on Github →
2017-12-20 23:25
data/ordinal.lean
refactor(data/ordinal): rearrange files, more cofinality
Modified is_strict_weak_order_of_is_order_connectedView on Github →
2017-12-10 08:36
data/ordinal.lean
feat(data/ordinal): ordinal numbers
Added is_strict_weak_order_of_is_order_connectedView on Github →