Theorem NNReal.infᵢ_real_pos_eq_infᵢ_nnreal_pos

Modification history