Theorems · Theorem · functional analysis

LipschitzWith.compLp.congr_simp

∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {g g_1 : E → F} (e_g : g = g_1) {c c_1 : NNReal}
  (e_c : c = c_1) (hg : LipschitzWith c g) (g0 : g 0 = 0) (f f_1 : ↥(MeasureTheory.Lp E p μ)),
  f = f_1 → hg.compLp g0 f = ⋯.compLp ⋯ f_1

Defined in

Mathlib.MeasureTheory.Function.LpSpace.Basic

Cited by

0 results in Mathlib

Foundations

Depth 226 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedAddCommGroup