Theorems · Theorem · global analysis

ContDiff.contDiffBump

∀ {E : Type u_1} {X : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup X]
  [inst_3 : NormedSpace ℝ X] [inst_4 : HasContDiffBump E] {n : ℕ∞} {c g : X → E} {f : (x : X) → ContDiffBump (c x)},
  ContDiff ℝ (↑n) c →
    (ContDiff ℝ ↑n fun x => (f x).rIn) →
      (ContDiff ℝ ↑n fun x => (f x).rOut) → ContDiff ℝ (↑n) g → ContDiff ℝ ↑n fun x => ↑(f x) (g x)

Defined in

Mathlib.Analysis.Calculus.BumpFunction.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceHasContDiffBump