Theorem: limit_const (LeanTeaching/TutoLib.lean)

State before:
x ε : ℝ
ε_pos : ε > 0
x✝¹ : ℕ
x✝ : x✝¹ ≥ 0
⊢ |(fun x_1 => x) x✝¹ - x| ≤ ε
Tactic:
simp [le_of_lt ε_pos]
State after:
no goals