Theorems · Theorem · global analysis

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

ContDiffBump is 𝒞ⁿ in all its arguments.

Defined in

Mathlib.Analysis.Calculus.BumpFunction.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceHasContDiffBump