coe_indicator — Mathlib

English

The embedding of NNReal into ENNReal commutes with the indicator function: ENNReal.ofNNReal(s.indicator f a) = s.indicator (fun x => ENNReal.ofNNReal(f x)) a.

Русский

Встраивание NNReal в ENNReal commute с индикаторной функцией: ENNReal.ofNNReal( s.indicator f a ) = s.indicator( x ↦ ENNReal.ofNNReal(f x) ) a.

LaTeX

$$$ENNReal.ofNNReal\left(s.indicator\, f\, a\right) = s.indicator\left(\lambda x. ENNReal.ofNNReal(f x)\right) a$$$

Lean4

@[simp, norm_cast]
theorem coe_indicator {α} (s : Set α) (f : α → ℝ≥0) (a : α) :
    ((s.indicator f a : ℝ≥0) : ℝ≥0∞) = s.indicator (fun x => ↑(f x)) a :=
  (ofNNRealHom : ℝ≥0 →+ ℝ≥0∞).map_indicator _ _ _

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