Let X, Y, d, fn and f be given.
Assume Hunif: uniform_limit_metric X Y d fn f.
We will prove pointwise_limit_metric X Y d fn f.
Let x be given.
Assume HxX: x ∈ X.
Let eps be given.
Assume HepsR: eps ∈ R.
Assume HepsPos: Rlt 0 eps.
Apply (Hunif eps HepsR HepsPos) to the current goal.
Let N be given.
Assume HNpair: N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → ∀x0 : set, x0 ∈ X → Rlt (apply_fun d (apply_fun (apply_fun fn n) x0,apply_fun f x0)) eps.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → ∀x0 : set, x0 ∈ X → Rlt (apply_fun d (apply_fun (apply_fun fn n) x0,apply_fun f x0)) eps) HNpair).
Let n be given.
Assume HnO: n ∈ ω.
Assume HNn: N ⊆ n.
We will prove Rlt (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) eps.
We prove the intermediate claim Htail: ∀n0 : set, n0 ∈ ω → N ⊆ n0 → ∀x0 : set, x0 ∈ X → Rlt (apply_fun d (apply_fun (apply_fun fn n0) x0,apply_fun f x0)) eps.
An exact proof term for the current goal is (andER (N ∈ ω) (∀n0 : set, n0 ∈ ω → N ⊆ n0 → ∀x0 : set, x0 ∈ X → Rlt (apply_fun d (apply_fun (apply_fun fn n0) x0,apply_fun f x0)) eps) HNpair).
An exact proof term for the current goal is (Htail n HnO HNn x HxX).
∎