zero_toSimpleFunc — Mathlib

English

The simple function corresponding to the zero Lp.simpleFunc is almost everywhere zero.

Русский

Простой нулевой функции соответствует нулевая функция почти всюду.

LaTeX

$$$\mathrm{toSimpleFunc}(0) =ᵐ_{\mu} 0$$$

Lean4

theorem zero_toSimpleFunc : toSimpleFunc (0 : Lp.simpleFunc E p μ) =ᵐ[μ] 0 :=
  by
  filter_upwards [toSimpleFunc_eq_toFun (0 : Lp.simpleFunc E p μ), Lp.coeFn_zero E 1 μ] with _ h₁ _
  rwa [h₁]

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