mathlib3
b779513a - feat(order/conditionally_complete_lattice): add `cInf_le_cInf'` (#14719)

Commit

3 years ago

feat(order/conditionally_complete_lattice): add `cInf_le_cInf'` (#14719) A version of `cInf_le_cInf` for `conditionally_complete_linear_order_bot`

Author

user7230724

Parents