indicatorConstLp_coeFn_mem — Mathlib

English

Almost everywhere with respect to μ, the function indicatorConstLp(p, s, hμs, c) equals c on s; i.e., for μ-a.e. x ∈ s we have indicatorConstLp(p, s, hμs, c)(x) = c.

Русский

Почти всюду по μ на s выполняется indicatorConstLp(p, s, hμs, c)(x) = c.

LaTeX

$$$\text{ae}_{\mu}\; indicatorConstLp(p, s, hμs, c)(x) = c \qquad \text{for } x \in s.$$$

Lean4

theorem indicatorConstLp_coeFn_mem : ∀ᵐ x : α ∂μ, x ∈ s → indicatorConstLp p hs hμs c x = c :=
  indicatorConstLp_coeFn.mono fun _x hx hxs => hx.trans (Set.indicator_of_mem hxs _)

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