sub_toSimpleFunc — Mathlib

English

The toSimpleFunc of a scalar multiple equals the scalar multiple of toSimpleFunc, almost everywhere.

Русский

toSimpleFunc(k·f) =ᵐ μ k·toSimpleFunc(f).

LaTeX

$$$toSimpleFunc(k\cdot f) =_{\mu} k\cdot toSimpleFunc(f)$$$

Lean4

theorem sub_toSimpleFunc (f g : Lp.simpleFunc E p μ) : toSimpleFunc (f - g) =ᵐ[μ] toSimpleFunc f - toSimpleFunc g :=
  by
  filter_upwards [toSimpleFunc_eq_toFun (f - g), toSimpleFunc_eq_toFun f, toSimpleFunc_eq_toFun g,
    Lp.coeFn_sub (f : Lp E p μ) g] with _
  simp only [AddSubgroup.coe_sub, Pi.sub_apply]
  repeat' intro h; rw [h]

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