theorem ENNReal.limsup_mul_const_of_ne_top {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal} (ha_top : a ≠ ⊤) : Filter.limsup (fun (x : α) => u x * a) f = Filter.limsup u f * a

theorem ENNReal.limsup_mul_const {α : Type u_1} {f : Filter α} [CountableInterFilter f] {u : α → ENNReal} {a : ENNReal} : Filter.limsup (fun (x : α) => u x * a) f = Filter.limsup u f * a