mathlib
ba346d8b - feat(order/upper_lower): `Iic` is not bounded below (#16425)

Commit

3 years ago

feat(order/upper_lower): `Iic` is not bounded below (#16425) Nonempty lower sets are not bounded below in a `no_min_order`, and dual.

Author

YaelDillies

Parents