Theorem EReal.liminf_const_mul_of_nonpos_of_ne_bot

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_nonpos_of_ne_botView on Github →