indicatorConst — Mathlib

English

Given a measurable set s with finite measure and c ∈ E, the function equal to c on s and 0 outside s represents an Lp-simple function.

Русский

Пусть s измеримо и μ(s) < ∞, и c ∈ E. Функция, равная c на s и 0 вне s, задаёт элемент Lp.simpleFunc.

LaTeX

$$$ \\text{indicatorConst}(p, hs, hμs, c) = \\text{toLp}\\left( (\\text{SimpleFunc.const } c) \\text{.piecewise } s\\; hs\\; ( \\text{SimpleFunc.const } 0) \\right) $$$

Lean4

/-- The characteristic function of a finite-measure measurable set `s`, as an `Lp` simple function.
-/
def indicatorConst {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (c : E) : Lp.simpleFunc E p μ :=
  toLp ((SimpleFunc.const _ c).piecewise s hs (SimpleFunc.const _ 0)) (memLp_indicator_const p hs c (Or.inr hμs))

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