exact eventually_of_mem this (fun x hx => le_antisymm (g.le_one x) (by simpa [hx] using g.h3 x))
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
g : trunc
this : Set.Icc (-1) 1 ∈ 𝓝 0
⊢ g.toFun =ᶠ[𝓝 0] 1
no goals