Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-04 08:30 85fffda8

View on Github →

feat(order/conditionally_complete_lattice,data/real/nnreal): add 2 lemmas (#14545) Add cInf_univ and nnreal.Inf_empty.

Estimated changes

added theorem nnreal.Inf_empty
added theorem cInf_univ