theorem ENNReal.sum_geometric_two_le (n : ℕ) : ∑ i ∈ Finset.range n, (1 / 2) ^ i ≤ 2

theorem ENNReal.ofReal_one_div {x : ℝ} (hx : 0 < x) : ENNReal.ofReal (1 / x) = 1 / ENNReal.ofReal x

theorem ENNReal.le_one_div_iff {x y : ENNReal} : x ≤ 1 / y ↔ y ≤ 1 / x

theorem ENat.toENNReal_iSup {ι : Sort u_1} (f : ι → ℕ∞) : ↑(⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)

theorem ENat.toENNReal_le' {m n : ℕ∞} : m ≤ n → ↑m ≤ ↑n

Alias of the reverse direction of ENat.toENNReal_le.