Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-07 02:03 71953e0b

View on Github →

feat(order/basic): add extensionality for order structures

Estimated changes

Modified order/basic.lean

added theorem linear_order.ext

added theorem partial_order.ext

added theorem preorder.ext

Modified order/bounded_lattice.lean

added theorem lattice.bounded_lattice.ext

added theorem lattice.order_bot.ext

added theorem lattice.order_bot.ext_bot

added theorem lattice.order_top.ext

added theorem lattice.order_top.ext_top

added theorem with_bot.inf_eq_min

added theorem with_bot.lattice_eq_DLO

added theorem with_bot.sup_eq_max

added theorem with_top.inf_eq_min

added theorem with_top.lattice_eq_DLO

added theorem with_top.sup_eq_max

Modified order/lattice.lean

added theorem lattice.inf_eq_min

added theorem lattice.lattice.ext

added theorem lattice.semilattice_inf.ext

added theorem lattice.semilattice_inf.ext_inf

added theorem lattice.semilattice_sup.ext

added theorem lattice.semilattice_sup.ext_sup

added theorem lattice.sup_eq_max