theorem ENNReal.sum_geometric_two_le (n : ℕ) : ∑ i ∈ Finset.range n, 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 ENNReal.div_le_one_of_le {x y : ENNReal} (h : x ≤ y) : x / y ≤ 1

theorem ENNReal.one_le_toReal {p : ENNReal} (hp1 : 1 ≤ p) (hp2 : p ≠ ⊤) : 1 ≤ p.toReal

theorem ENNReal.toReal_pos_of_one_le {p : ENNReal} (hp1 : 1 ≤ p) (hp2 : p ≠ ⊤) : 0 < p.toReal

theorem ENNReal.rpow_iSup {ι : Type u_1} (f : ι → ENNReal) {x : ℝ} (hx : 0 < x) : (⨆ (i : ι), f i) ^ x = ⨆ (i : ι), f i ^ x

theorem ENNReal.div_pow (a b : ENNReal) (n : ℕ) : (a / b) ^ n = a ^ n / b ^ n

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

Alias of the reverse direction of ENat.toENNReal_le.