compLp_zero — Mathlib

English

If g(0)=0 and g is Lipschitz, then composing the zero element of Lp with g via compLp yields the zero element in Lp.

Русский

Если g(0)=0 и g Lipschitz, то compLp(0) = 0 в Lp.

LaTeX

$$compLp_zero$$

Lean4

@[simp]
theorem compLp_zero (hg : LipschitzWith c g) (g0 : g 0 = 0) : hg.compLp g0 (0 : Lp E p μ) = 0 :=
  by
  rw [Lp.eq_zero_iff_ae_eq_zero]
  apply (coeFn_compLp _ _ _).trans
  filter_upwards [Lp.coeFn_zero E p μ] with _ ha
  simp only [ha, g0, Function.comp_apply, Pi.zero_apply]

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