Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nonempty_of_is_glb

Modification history

2020-02-25 14:16
src/order/bounds.lean
refactor(order/bounds): use dot notation, reorder, prove more properties (#2028) …
Deleted nonempty_of_is_glbView on Github →
2020-02-05 06:25
src/order/bounds.lean
refactor(*): migrate from `≠ ∅` to `set.nonempty` (#1954) …
Added nonempty_of_is_glbView on Github →