Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2018-08-14 16:11
add16e97
View on Github →
feat(order): add order_dual (similar to with_top/with_bot) and dual order instances
Estimated changes
Modified
order/basic.lean
deleted
theorem
le_dual_eq_le
added
def
order_dual
deleted
def
partial_order.dual
deleted
def
preorder.dual
Modified
order/bounded_lattice.lean
Modified
order/complete_lattice.lean
added
theorem
lattice.Inf_eq_top
added
theorem
lattice.Sup_eq_bot
modified
theorem
lattice.infi_const
added
theorem
lattice.infi_eq_bot
added
theorem
lattice.infi_eq_top
modified
theorem
lattice.infi_top
added
def
lattice.ord_continuous
added
theorem
lattice.ord_continuous_mono
added
theorem
lattice.ord_continuous_sup
modified
theorem
lattice.supr_bot
modified
theorem
lattice.supr_const
deleted
def
ord_continuous
deleted
theorem
ord_continuous_mono
deleted
theorem
ord_continuous_sup
Modified
order/galois_connection.lean
Modified
order/lattice.lean