coe_indicatorConst — Mathlib

English

The canonical inclusion of indicatorConst into Lp.simpleFunc coincides with its natural Lp representation.

Русский

Каноническое вложение indicatorConst в Lp.simpleFunc совпадает с его естественным представлением в Lp.

LaTeX

$$$ (\\uparrow)(indicatorConst p hs hμs c) = indicatorConstLp p hs hμs c $$$

Lean4

@[simp]
theorem coe_indicatorConst {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (c : E) :
    (↑(indicatorConst p hs hμs c) : Lp E p μ) = indicatorConstLp p hs hμs c :=
  rfl

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