Let X, Y, d, fn, f and eps be given.
Assume Hd: metric_on_total Y d.
Assume Hfn: ∀n : set, n ∈ ω → function_on (apply_fun fn n) X Y.
Assume Hf: function_on f X Y.
Assume Hlim: pointwise_limit_metric X Y d fn f.
Assume HepsR: eps ∈ R.
Assume HepsPos: Rlt 0 eps.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim HexNsmall: ∃Nsmall ∈ ω, eps_ Nsmall < eps.
An exact proof term for the current goal is (exists_eps_lt_pos_Euclid eps HepsR HepsPos).
Apply HexNsmall to the current goal.
Let Nsmall be given.
Assume HNsmallpair.
We prove the intermediate claim HNsmallO: Nsmall ∈ ω.
An exact proof term for the current goal is (andEL (Nsmall ∈ ω) (eps_ Nsmall < eps) HNsmallpair).
We prove the intermediate claim HepsNlt: eps_ Nsmall < eps.
An exact proof term for the current goal is (andER (Nsmall ∈ ω) (eps_ Nsmall < eps) HNsmallpair).
We prove the intermediate claim HNsmallNat: nat_p Nsmall.
An exact proof term for the current goal is (omega_nat_p Nsmall HNsmallO).
We prove the intermediate claim HNsuccO: ordsucc Nsmall ∈ ω.
An exact proof term for the current goal is (omega_ordsucc Nsmall HNsmallO).
Set eps2 to be the term eps_ (ordsucc Nsmall).
We prove the intermediate claim Heps2R: eps2 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real eps2 (SNo_eps_SNoS_omega (ordsucc Nsmall) HNsuccO)).
We prove the intermediate claim Heps2Pos: Rlt 0 eps2.
An exact proof term for the current goal is (RltI 0 eps2 real_0 Heps2R (SNo_eps_pos (ordsucc Nsmall) HNsuccO)).
We prove the intermediate claim HepsHalf: add_SNo eps2 eps2 = eps_ Nsmall.
An exact proof term for the current goal is (eps_ordsucc_half_add Nsmall HNsmallNat).
We prove the intermediate claim HepsNR: eps_ Nsmall ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ Nsmall) (SNo_eps_SNoS_omega Nsmall HNsmallO)).
We prove the intermediate claim HepsNS: SNo (eps_ Nsmall).
An exact proof term for the current goal is (real_SNo (eps_ Nsmall) HepsNR).
We prove the intermediate claim HepsS: SNo eps.
An exact proof term for the current goal is (real_SNo eps HepsR).
We prove the intermediate claim HepsNltR: Rlt (eps_ Nsmall) eps.
An exact proof term for the current goal is (RltI (eps_ Nsmall) eps HepsNR HepsR HepsNlt).
We prove the intermediate claim HexN0: ∃N0 : set, N0 ∈ ω ∧ ∀n : set, n ∈ ω → N0 ⊆ n → Rlt (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) eps2.
An exact proof term for the current goal is (Hlim x HxX eps2 Heps2R Heps2Pos).
Apply HexN0 to the current goal.
Let N0 be given.
Assume HN0pair.
We prove the intermediate claim HN0O: N0 ∈ ω.
An exact proof term for the current goal is (andEL (N0 ∈ ω) (∀n : set, n ∈ ω → N0 ⊆ n → Rlt (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) eps2) HN0pair).
We prove the intermediate claim Htail: ∀n : set, n ∈ ω → N0 ⊆ n → Rlt (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) eps2.
An exact proof term for the current goal is (andER (N0 ∈ ω) (∀n : set, n ∈ ω → N0 ⊆ n → Rlt (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) eps2) HN0pair).
We use N0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HN0O.
We prove the intermediate claim HdefA: A_N_eps X Y d fn N0 eps = {x0 ∈ X|∀n : set, n ∈ ω → N0 ⊆ n → ∀m : set, m ∈ ω → N0 ⊆ m → Rle (apply_fun d (apply_fun (apply_fun fn n) x0,apply_fun (apply_fun fn m) x0)) eps}.
Use reflexivity.
rewrite the current goal using HdefA (from left to right).
Apply (SepI X (λx0 : set ⇒ ∀n : set, n ∈ ω → N0 ⊆ n → ∀m : set, m ∈ ω → N0 ⊆ m → Rle (apply_fun d (apply_fun (apply_fun fn n) x0,apply_fun (apply_fun fn m) x0)) eps) x HxX) to the current goal.
Let n be given.
Assume HnO: n ∈ ω.
Assume HN0n: N0 ⊆ n.
Let m be given.
Assume HmO: m ∈ ω.
Assume HN0m: N0 ⊆ m.
We prove the intermediate claim HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hf x HxX).
We prove the intermediate claim HfnxY: apply_fun (apply_fun fn n) x ∈ Y.
An exact proof term for the current goal is ((Hfn n HnO) x HxX).
We prove the intermediate claim HfmxY: apply_fun (apply_fun fn m) x ∈ Y.
An exact proof term for the current goal is ((Hfn m HmO) x HxX).
We prove the intermediate claim HmY: metric_on Y d.
An exact proof term for the current goal is (metric_on_total_imp_metric_on Y d Hd).
We prove the intermediate claim Hsym: apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x) = apply_fun d (apply_fun (apply_fun fn m) x,apply_fun f x).
An exact proof term for the current goal is (metric_on_symmetric Y d (apply_fun f x) (apply_fun (apply_fun fn m) x) HmY HfxY HfmxY).
We prove the intermediate claim Hdn: Rlt (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) eps2.
An exact proof term for the current goal is (Htail n HnO HN0n).
We prove the intermediate claim Hdm: Rlt (apply_fun d (apply_fun (apply_fun fn m) x,apply_fun f x)) eps2.
An exact proof term for the current goal is (Htail m HmO HN0m).
We prove the intermediate claim Hdm2: Rlt (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x)) eps2.
rewrite the current goal using Hsym (from left to right).
An exact proof term for the current goal is Hdm.
We prove the intermediate claim HdR: metric_on Y d.
An exact proof term for the current goal is HmY.
We prove the intermediate claim Htri: Rle (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x)) (add_SNo (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x))).
An exact proof term for the current goal is (metric_triangle_Rle Y d (apply_fun (apply_fun fn n) x) (apply_fun f x) (apply_fun (apply_fun fn m) x) HdR HfnxY HfxY HfmxY).
We prove the intermediate claim Hdnlt: (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) < eps2.
An exact proof term for the current goal is (RltE_lt (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) eps2 Hdn).
We prove the intermediate claim Hdmlt: (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x)) < eps2.
An exact proof term for the current goal is (RltE_lt (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x)) eps2 Hdm2).
We prove the intermediate claim HdnR: (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) ∈ R.
An exact proof term for the current goal is (RltE_left (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) eps2 Hdn).
We prove the intermediate claim HdmR: (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x)) ∈ R.
An exact proof term for the current goal is (RltE_left (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x)) eps2 Hdm2).
We prove the intermediate claim HdnS: SNo (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)).
An exact proof term for the current goal is (real_SNo (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) HdnR).
We prove the intermediate claim HdmS: SNo (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x)).
An exact proof term for the current goal is (real_SNo (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x)) HdmR).
We prove the intermediate claim Heps2S: SNo eps2.
An exact proof term for the current goal is (real_SNo eps2 Heps2R).
We prove the intermediate claim Hsumlt: add_SNo (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x)) < add_SNo eps2 eps2.
An exact proof term for the current goal is (add_SNo_Lt3 (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x)) eps2 eps2 HdnS HdmS Heps2S Heps2S Hdnlt Hdmlt).
We prove the intermediate claim HsumR: add_SNo (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x)) ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) HdnR (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x)) HdmR).
We prove the intermediate claim Hsumlt2: add_SNo (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x)) < eps_ Nsmall.
rewrite the current goal using HepsHalf (from right to left).
An exact proof term for the current goal is Hsumlt.
We prove the intermediate claim Hsumlt3: add_SNo (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x)) < eps.
An exact proof term for the current goal is (SNoLt_tra (add_SNo (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x))) (eps_ Nsmall) eps (SNo_add_SNo (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x)) HdnS HdmS) HepsNS HepsS Hsumlt2 HepsNlt).
We prove the intermediate claim HsumepsR: Rlt (add_SNo (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x))) eps.
An exact proof term for the current goal is (RltI (add_SNo (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x))) eps HsumR HepsR Hsumlt3).
We prove the intermediate claim HdnmLt: Rlt (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x)) eps.
An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x)) (add_SNo (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun f x)) (apply_fun d (apply_fun f x,apply_fun (apply_fun fn m) x))) eps Htri HsumepsR).
An exact proof term for the current goal is (Rlt_implies_Rle (apply_fun d (apply_fun (apply_fun fn n) x,apply_fun (apply_fun fn m) x)) eps HdnmLt).
∎