Lemmas about topology on ℝ≥0∞.

theorem ENNReal.tendsto_zero_of_le {α : Type u_1} {f g : α → ENNReal} {ι : Filter α} (hg : Filter.Tendsto g ι (nhds 0)) (h : f ≤ g) : Filter.Tendsto f ι (nhds 0)