Theorems · Theorem · global analysis

ContDiffAt.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)}
  {x : X},
  ContDiffAt ℝ (↑n) c x →
    ContDiffAt ℝ (↑n) (fun x => (f x).rIn) x →
      ContDiffAt ℝ (↑n) (fun x => (f x).rOut) x → ContDiffAt ℝ (↑n) g x → ContDiffAt ℝ (↑n) (fun x => ↑(f x) (g x)) x

ContDiffBump is 𝒞ⁿ in all its arguments.

Defined in

Mathlib.Analysis.Calculus.BumpFunction.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceHasContDiffBump