Mathlib v3 is deprecated. Go to Mathlib v4

Theorem with_top.inf_eq_min

Modification history

2021-09-15 02:43
src/order/bounded_lattice.lean
chore(*): upgrade to Lean 3.33.0c (#9165) …
Deleted with_top.inf_eq_minView on Github →
2020-10-27 11:55
src/order/bounded_lattice.lean
refactor(*): drop `decidable_linear_order`, switch to Lean 3.22.0 (#4762) …
Modified with_top.inf_eq_minView on Github →
2018-07-07 02:03
order/bounded_lattice.lean
feat(order/basic): add extensionality for order structures
Added with_top.inf_eq_minView on Github →