map_coe_ennreal_restrict — Mathlib

English

Specializing to ENNReal, the restricted-simple-func map with ENNReal.ofNNReal coincides with restricting the mapped simple function.

Русский

Специализация на ENNReal: отображение ограничения через ENNReal.ofNNReal совпадает с ограничением отображаемой простой функции.

LaTeX

$$$(f\\restriction s).map(\\mathrm{ENNReal.ofNNReal}) = (f.map(\\mathrm{ENNReal.ofNNReal})).\\restrict s.$$$

Lean4

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

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