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

State before:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ ⨆ x ∈ K, ↑(absNthDeriv n f x) ≠ ⊤
Tactic:
rw [iSup₂_coe_eq_coe_sSup hK]
State after:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ ↑(sSup (absNthDeriv n f '' K)) ≠ ⊤

State before:
n : ℕ
f : Bump ℝ
K : Set ℝ
hK : IsCompact K
⊢ ↑(sSup (absNthDeriv n f '' K)) ≠ ⊤
Tactic:
simp
State after:
no goals