map_coe_nnreal_restrict — Mathlib

English

Analogous to ENNReal specialization, but for NNReal: the map of restrict via NNReal corresponds to restricting the map.

Русский

Аналогично для NNReal: отображение через NNReal согласуется с ограничением функции.

LaTeX

$$$(f\\restriction s).map (\\mathrm{NNReal.toReal}) = (f.map(\\mathrm{NNReal.toReal})).restrict s.$$$

Lean4

theorem map_coe_nnreal_restrict (f : α →ₛ ℝ≥0) (s : Set α) :
    (f.restrict s).map ((↑) : ℝ≥0 → ℝ) = (f.map (↑)).restrict s :=
  map_restrict_of_zero NNReal.coe_zero _ _

Похожие утверждения