Theorem Real.smul_infᵢ_of_nonneg

Modification history