Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-26 19:45 a71628aa

View on Github →

feat(algebra/order,...): material on orders (#554)

Estimated changes

Modified algebra/order.lean

added theorem le_of_forall_le'

added theorem le_of_forall_lt'

Modified algebra/order_functions.lean

modified theorem le_max_iff

modified theorem le_min_iff

modified theorem lt_max_iff

modified theorem lt_min_iff

modified theorem max_le_iff

modified theorem max_lt_iff

modified theorem min_le_iff

modified theorem min_lt_iff

Modified algebra/ordered_group.lean

added theorem with_top.add_lt_add_iff_right

added theorem with_top.add_lt_top

Modified algebra/ordered_ring.lean

added theorem with_top.mul_eq_top_iff

Modified data/finset.lean

Modified order/bounded_lattice.lean

added theorem lattice.ne_bot_of_gt

added theorem lattice.ne_top_of_lt

Modified order/lattice.lean

added theorem lattice.lt_inf_iff

added theorem lattice.sup_lt_iff