Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-14 12:37 7f60a62d

View on Github →

chore(order/basic): move unbundled order classes to rel_classes ([#3066](https://github.com/leanprover-community/mathlib/pull/3066)) Reason: these classes are rarely used in mathlib, we don't need to mix them with classes extending has_le`.

Estimated changes

deleted theorem antisymm_of_asymm
deleted def bounded
deleted theorem is_antisymm.swap
deleted theorem is_asymm.swap
deleted theorem is_irrefl.swap
deleted theorem is_irrefl_of_is_asymm
deleted theorem is_linear_order.swap
deleted theorem is_partial_order.swap
deleted theorem is_preorder.swap
deleted theorem is_refl.swap
deleted theorem is_strict_order.swap
deleted theorem is_total.swap
deleted theorem is_total_preorder.swap
deleted theorem is_trans.swap
deleted theorem is_trichotomous.swap
deleted theorem not_bounded_iff
deleted theorem not_unbounded_iff
deleted def partial_order_of_SO
deleted theorem trans_trichotomous_left
deleted theorem trans_trichotomous_right
deleted def unbounded
deleted theorem well_founded.has_min
deleted theorem well_founded.min_mem
deleted theorem well_founded.not_lt_min
added def bounded
added theorem is_antisymm.swap
added theorem is_asymm.swap
added theorem is_irrefl.swap
added theorem is_linear_order.swap
added theorem is_partial_order.swap
added theorem is_preorder.swap
added theorem is_refl.swap
added theorem is_strict_order.swap
added theorem is_total.swap
added theorem is_total_preorder.swap
added theorem is_trans.swap
added theorem is_trichotomous.swap
added theorem not_bounded_iff
added theorem not_unbounded_iff
added def unbounded
added theorem well_founded.has_min
added theorem well_founded.min_mem