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 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 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.