indicatorConstLp_coeFn — Mathlib

English

The constant-valued indicator LP function is almost everywhere equal to the simple function that is c on s and 0 outside s; i.e., indicatorConstLp(p, s, hμs, c) =_ae μ s.indicator (function x ↦ c).

Русский

Функция indicatorConstLp(p, s, hμs, c) почти всюду равна простой функции, равной c на s и 0 вне s; то есть indicatorConstLp(p, s, hμs, c) =_ae μ s.indicator (функция x ↦ c).

LaTeX

$$$indicatorConstLp(p, s, hμs, c) =_{ae,\mu} s.indicator (\lambda x. c).$$$

Lean4

theorem indicatorConstLp_coeFn : ⇑(indicatorConstLp p hs hμs c) =ᵐ[μ] s.indicator fun _ => c :=
  MemLp.coeFn_toLp (memLp_indicator_const p hs c (Or.inr hμs))

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