Let X, Y, d, fn, f and x be given.
Assume Hd: metric_on Y d.
Assume Hfn: function_on fn ω (function_space X Y).
Assume Hf: function_on f X Y.
Assume HxX: x ∈ X.
Assume Hunif: uniform_limit_metric X Y d fn f.
Set seqx to be the term graph ω (λn : set ⇒ apply_fun (apply_fun fn n) x).
We will prove sequence_converges_metric Y d seqx (apply_fun f x).
We will prove (((metric_on Y d ∧ sequence_on seqx Y) ∧ apply_fun f x ∈ Y) ∧ ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun d (apply_fun seqx n,apply_fun f x)) eps).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hd.
We will prove sequence_on seqx Y.
Let n be given.
Assume HnO: n ∈ ω.
We will prove apply_fun seqx n ∈ Y.
We prove the intermediate claim Hseqxdef: seqx = graph ω (λn0 : set ⇒ apply_fun (apply_fun fn n0) x).
Use reflexivity.
rewrite the current goal using (apply_fun_of_graph_eq seqx ω (λn0 : set ⇒ apply_fun (apply_fun fn n0) x) n Hseqxdef HnO) (from left to right).
We prove the intermediate claim HfnnFS: apply_fun fn n ∈ function_space X Y.
An exact proof term for the current goal is (Hfn n HnO).
We prove the intermediate claim Hfnn_on: function_on (apply_fun fn n) X Y.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod X Y)) (λf0 : set ⇒ function_on f0 X Y) (apply_fun fn n) HfnnFS).
An exact proof term for the current goal is (Hfnn_on x HxX).
An exact proof term for the current goal is (Hf x HxX).
Let eps be given.
Assume Heps: eps ∈ R ∧ Rlt 0 eps.
We prove the intermediate claim HepsR: eps ∈ R.
An exact proof term for the current goal is (andEL (eps ∈ R) (Rlt 0 eps) Heps).
We prove the intermediate claim HepsPos: Rlt 0 eps.
An exact proof term for the current goal is (andER (eps ∈ R) (Rlt 0 eps) Heps).
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 seqx n,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).
We prove the intermediate claim Hseqxdef: seqx = graph ω (λn0 : set ⇒ apply_fun (apply_fun fn n0) x).
Use reflexivity.
rewrite the current goal using (apply_fun_of_graph_eq seqx ω (λn0 : set ⇒ apply_fun (apply_fun fn n0) x) n Hseqxdef HnO) (from left to right).
An exact proof term for the current goal is (Htail n HnO HNn x HxX).
∎