f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
n : ℕ
x : ↑I
k : Fin (n + 1)
m : k ∈ S f ε h n x
⊢ dist k/ₙ x < ContinuousMap.modulus f (ε / 2) (_ : 0 < ε / 2)
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
n : ℕ
x : ↑I
k : Fin (n + 1)
m : k ∈ S f ε h n x
⊢ abs (↑f k/ₙ - ↑f x) < ε / 2
apply f.dist_lt_of_dist_lt_modulus (ε / 2) (half_pos h)
no goals
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
n : ℕ
x : ↑I
k : Fin (n + 1)
m : k ∈ S f ε h n x
⊢ dist k/ₙ x < ContinuousMap.modulus f (ε / 2) (_ : 0 < ε / 2)
simpa [S, (Set.mem_toFinset)] using m