Theorem: Bump₁.absNthDeriv_continuous (ForML/BumpTopology.lean)

State before:
n : ℕ
f : Bump ℝ
⊢ Continuous (absNthDeriv n f)
Tactic:
simp [absNthDeriv_def]
State after:
n : ℕ
f : Bump ℝ
⊢ Continuous fun x => ‖iteratedDeriv n (↑f) x‖₊

State before:
n : ℕ
f : Bump ℝ
⊢ Continuous fun x => ‖iteratedDeriv n (↑f) x‖₊
Tactic:
apply Continuous.nnnorm
State after:
case a
n : ℕ
f : Bump ℝ
⊢ Continuous fun x => iteratedDeriv n (↑f) x

State before:
case a
n : ℕ
f : Bump ℝ
⊢ Continuous fun x => iteratedDeriv n (↑f) x
Tactic:
exact ContDiff.continuous_iteratedDeriv _ f.contDiff (by norm_num)
State after:
no goals

State before:
n : ℕ
f : Bump ℝ
⊢ ↑n ≤ ⊤
Tactic:
norm_num
State after:
no goals