theorem NNReal.neq_zero_imp_gt {x : NNReal} (h : x ≠ 0) : 0 < x

theorem NNReal.pos_imp_add_pos (x y : NNReal) (h : x ≠ 0) : x + y ≠ 0

def NNReal.toPReal (x : NNReal) (h : 0 < x) : ℝ>0

Equations

• x.toPReal h = ⟨↑x, h⟩

def NNReal.toPReal' (x : NNReal) (h : x ≠ 0) : ℝ>0

Equations

• x.toPReal' h = ⟨↑x, ⋯⟩

@[simp]

theorem NNReal_toPReal_toNNReal_eq_self (x : NNReal) (h : 0 < x) : ↑(x.toPReal h) = x