Theorem: trunc.zero (PrimeNumberTheoremAnd/Sobolev.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
g : trunc
⊢ g.toFun =ᶠ[𝓝 0] 1
Tactic:
have : Set.Icc (-1) 1 ∈ 𝓝 (0 : ℝ) := by apply Icc_mem_nhds <;> linarith
State after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
g : trunc
this : Set.Icc (-1) 1 ∈ 𝓝 0
⊢ g.toFun =ᶠ[𝓝 0] 1

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

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
g : trunc
⊢ Set.Icc (-1) 1 ∈ 𝓝 0
Tactic:
apply Icc_mem_nhds <;> linarith
State after:
no goals

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
g : trunc
this : Set.Icc (-1) 1 ∈ 𝓝 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ 1 x ≤ g.toFun x
Tactic:
simpa [hx] using g.h3 x
State after:
no goals