Commit 2020-12-30 15:51 38ba6ba2

chore(data/real/{e,}nnreal): a few lemmas (#5530)

• Rename nnreal.le_of_forall_lt_one_mul_lt to nnreal.le_of_forall_lt_one_mul_le, and similarly for ennreal.
• Move the proof of the latter lemma to topology/instances/ennreal, prove it using continuity of multiplication.
• Add ennreal.le_of_forall_nnreal_lt, nnreal.lt_div_iff, and nnreal.mul_lt_of_lt_div.