Theorem ENNReal.coe_lt_ofReal

Modification history

2026-02-09 07:29
Mathlib/Data/ENNReal/Real.lean
feat: real-valued Lᵖ norm (#23881)
Added ENNReal.coe_lt_ofRealView on Github →