Local smooth representatives at the finite source regularity order.

theorem AVenhance.Infra.Section4.amnr_finite_smooth_local_representative {U : Set AmnrSpace} (hU : IsOpen U) {f : AmnrSpace → ℝ} {N : ℕ} (hf : ContDiffOn ℝ (↑N) f U) {z : AmnrSpace} (hz : z ∈ U) : ∃ (g : AmnrSpace → ℝ), ContDiff ℝ (↑N) g ∧ g =ᶠ[nhds z] f

A scalar field smooth on an open domain has a globally smooth local representative. This does not impose any extension condition on the solution.