Theorem EReal.liminf_const_mul_of_nonneg_of_ne_top

Modification history

2026-03-10 15:17
Mathlib/Topology/Instances/EReal/Lemmas.lean
feat(Topology/Instances/EReal): limsup of multiplication by a constant (#35272) …
Added EReal.liminf_const_mul_of_nonneg_of_ne_topView on Github →