mathlib3
6c247315 - feat(order/bounded_lattice): `ne_(bot|top)_iff_exists` (#8960)

Commit

4 years ago

feat(order/bounded_lattice): `ne_(bot|top)_iff_exists` (#8960) Like `ne_zero_iff_exists`

Author

pechersky

Parents