Theorems · Theorem · real analysis

ContDiff.lipschitzWith_of_hasCompactSupport

∀ {n : WithTop ℕ∞} {𝕂 : Type u_1} [inst : RCLike 𝕂] {E' : Type u_2} [inst_1 : NormedAddCommGroup E']
  [inst_2 : NormedSpace 𝕂 E'] {F' : Type u_3} [inst_3 : NormedAddCommGroup F'] [inst_4 : NormedSpace 𝕂 F']
  {f : E' → F'}, HasCompactSupport f → ContDiff 𝕂 n f → n ≠ 0 → ∃ C, LipschitzWith C f

A C^n function with compact support is Lipschitz.

Defined in: Mathlib.Analysis.Calculus.ContDiff.RCLike
Cited by: 1 results in Mathlib
Foundations: Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: RCLike NormedAddCommGroup NormedSpace NormedAddCommGroup NormedSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realproof · cited by 25,697
NormedAddCommGroupstatement and proof · cited by 15,752
NormedSpacestatement and proof · cited by 12,499
Norm.normproof · cited by 5,413
ENatstatement and proof · cited by 4,985
NNRealstatement · cited by 4,310
WithTopstatement and proof · cited by 3,754
RCLikestatement and proof · cited by 2,829
fderivproof · cited by 398
ContDiffstatement and proof · cited by 352
LipschitzWithstatement · cited by 316
le_max_rightproof · cited by 205

Cited by1

Results whose statement or proof uses this declaration.

LipschitzWith.ae_lineDeriv_sum_eqproof · cited by 1