Commit 2022-05-13 02:53 c4c279e6
View on Github →feat(data/real/nnreal): add nnreal.le_infi_add_infi and other lemmas (#14048)
- add
nnreal.coe_two,nnreal.le_infi_add_infi,nnreal.half_le_self; - generalize
le_cinfi_mul_cinfi,csupr_mul_csupr_le, and their additive versions to allow two different index types.