Theorem inf_eq_bot_iff_le_compl
Modification history
2022-05-24 10:24
src/order/bounded_order.lean
chore(order/bounded_order): Golf `disjoint` API (#14194) …
Deleted inf_eq_bot_iff_le_complView on Github →2021-11-29 17:49
src/order/bounded_order.lean
chore(order): fix-ups after #9891 (#10538)
Modified inf_eq_bot_iff_le_complView on Github →2021-11-23 13:11
src/order/bounded_order.lean
refactor(*): split `order_{top,bot}` from `lattice` hierarchy (#9891) …
Added inf_eq_bot_iff_le_complView on Github →2021-10-28 17:00
src/order/bounded_lattice.lean
feat(order/bounded_lattice): add `is_compl.le_sup_right_iff_inf_left_le` (#10014) …
Deleted inf_eq_bot_iff_le_complView on Github →2020-03-19 15:12
src/order/bounded_lattice.lean
refactor(*): drop `lattice` namespace (#2166) …
Added inf_eq_bot_iff_le_complView on Github →2017-08-11 17:57
algebra/lattice/filter.lean
algebra/lattice/filter: cleanup move theorems to appropriate places
Deleted inf_eq_bot_iff_le_complView on Github →2017-08-10 16:36
algebra/lattice/filter.lean
construct reals as complete, linear ordered field
Modified inf_eq_bot_iff_le_complView on Github →