Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-23 09:33 ceb13bad

View on Github →

chore(order/basic): add monotone.order_dual, strict_mono.order_dual (#2778) Also split long lines and lint.

Estimated changes

modified theorem is_strict_total_order'.swap
modified theorem le_of_forall_ge_of_dense
modified theorem le_of_forall_le_of_dense
added theorem monotone.order_dual
added theorem strict_mono.order_dual