Mathlib v3 is deprecated. Go to Mathlib v4

Def continuous_map.coe_nnreal_real

Modification history

2022-07-18 12:17
src/topology/instances/nnreal.lean
feat(topology/instances/nnreal): add `can_lift C(X, ℝ) C(X, ℝ≥0)` (#15446)
Added continuous_map.coe_nnreal_realView on Github →