mathlib3
85fffda8 - feat(order/conditionally_complete_lattice,data/real/nnreal): add 2 lemmas (#14545)

Commit
3 years ago
feat(order/conditionally_complete_lattice,data/real/nnreal): add 2 lemmas (#14545) Add `cInf_univ` and `nnreal.Inf_empty`.
Author
Parents
Loading