Let X, dX, Y, dY, f_seq and f be given.
Assume HdX: metric_on X dX.
Assume HdY: metric_on Y dY.
Assume Hfseq: function_on f_seq ω (function_space X Y).
Assume Hcont: ∀n : set, n ∈ ω → continuous_map X (metric_topology X dX) Y (metric_topology Y dY) (apply_fun f_seq n).
Assume Hunif: uniform_convergence_functions X dX Y dY f_seq f.
We will prove continuous_map X (metric_topology X dX) Y (metric_topology Y dY) f.
We prove the intermediate claim Hf: function_on f X Y.
An exact proof term for the current goal is (uniform_convergence_functions_f X dX Y dY f_seq f Hunif).
We prove the intermediate claim Hed: ∀x0 : set, x0 ∈ X → ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃delta : set, delta ∈ R ∧ Rlt 0 delta ∧ (∀x : set, x ∈ X → Rlt (apply_fun dX (x,x0)) delta → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps).
Let x0 be given.
Assume Hx0X: x0 ∈ X.
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).
We prove the intermediate claim HexN0: ∃N0 ∈ ω, eps_ N0 < eps.
An exact proof term for the current goal is (exists_eps_lt_pos eps HepsR Hepspos).
Apply HexN0 to the current goal.
Let N0 be given.
Assume HN0pair.
We prove the intermediate claim HN0omega: N0 ∈ ω.
An exact proof term for the current goal is (andEL (N0 ∈ ω) (eps_ N0 < eps) HN0pair).
We prove the intermediate claim HepsN0lt: eps_ N0 < eps.
An exact proof term for the current goal is (andER (N0 ∈ ω) (eps_ N0 < eps) HN0pair).
We prove the intermediate claim HN0nat: nat_p N0.
An exact proof term for the current goal is (omega_nat_p N0 HN0omega).
We prove the intermediate claim Hsucc0: ordsucc N0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N0 HN0omega).
We prove the intermediate claim Hsucc1: ordsucc (ordsucc N0) ∈ ω.
An exact proof term for the current goal is (omega_ordsucc (ordsucc N0) Hsucc0).
Set eta to be the term eps_ (ordsucc (ordsucc N0)).
We prove the intermediate claim HetaR: eta ∈ R.
An exact proof term for the current goal is (SNoS_omega_real eta (SNo_eps_SNoS_omega (ordsucc (ordsucc N0)) Hsucc1)).
We prove the intermediate claim HetaS: SNo eta.
An exact proof term for the current goal is (SNo_eps_ (ordsucc (ordsucc N0)) Hsucc1).
We prove the intermediate claim H0lt_eta: 0 < eta.
An exact proof term for the current goal is (SNo_eps_pos (ordsucc (ordsucc N0)) Hsucc1).
We prove the intermediate claim HetaPos: Rlt 0 eta.
An exact proof term for the current goal is (RltI 0 eta real_0 HetaR H0lt_eta).
We prove the intermediate claim HexNu: ∃Nu : set, Nu ∈ ω ∧ ∀n : set, n ∈ ω → Nu ⊆ n → ∀x : set, x ∈ X → Rlt (apply_fun dY (apply_fun (apply_fun f_seq n) x,apply_fun f x)) eta.
An exact proof term for the current goal is (uniform_convergence_functions_eps X dX Y dY f_seq f Hunif eta (andI (eta ∈ R) (Rlt 0 eta) HetaR HetaPos)).
Apply HexNu to the current goal.
Let Nu be given.
Assume HNupair.
We prove the intermediate claim HNuomega: Nu ∈ ω.
An exact proof term for the current goal is (andEL (Nu ∈ ω) (∀n : set, n ∈ ω → Nu ⊆ n → ∀x : set, x ∈ X → Rlt (apply_fun dY (apply_fun (apply_fun f_seq n) x,apply_fun f x)) eta) HNupair).
We prove the intermediate claim HNuprop: ∀n : set, n ∈ ω → Nu ⊆ n → ∀x : set, x ∈ X → Rlt (apply_fun dY (apply_fun (apply_fun f_seq n) x,apply_fun f x)) eta.
An exact proof term for the current goal is (andER (Nu ∈ ω) (∀n : set, n ∈ ω → Nu ⊆ n → ∀x : set, x ∈ X → Rlt (apply_fun dY (apply_fun (apply_fun f_seq n) x,apply_fun f x)) eta) HNupair).
Set fn to be the term apply_fun f_seq Nu.
We prove the intermediate claim Hfncont: continuous_map X (metric_topology X dX) Y (metric_topology Y dY) fn.
An exact proof term for the current goal is (Hcont Nu HNuomega).
We prove the intermediate claim Hfn: function_on fn X Y.
An exact proof term for the current goal is (continuous_map_function_on X (metric_topology X dX) Y (metric_topology Y dY) fn Hfncont).
We prove the intermediate claim Hedfn: ∀x1 : set, x1 ∈ X → ∀eps1 : set, eps1 ∈ R ∧ Rlt 0 eps1 → ∃delta1 : set, delta1 ∈ R ∧ Rlt 0 delta1 ∧ (∀x2 : set, x2 ∈ X → Rlt (apply_fun dX (x2,x1)) delta1 → Rlt (apply_fun dY (apply_fun fn x2,apply_fun fn x1)) eps1).
An exact proof term for the current goal is (iffEL (continuous_map X (metric_topology X dX) Y (metric_topology Y dY) fn) (∀x1 : set, x1 ∈ X → ∀eps1 : set, eps1 ∈ R ∧ Rlt 0 eps1 → ∃delta1 : set, delta1 ∈ R ∧ Rlt 0 delta1 ∧ (∀x2 : set, x2 ∈ X → Rlt (apply_fun dX (x2,x1)) delta1 → Rlt (apply_fun dY (apply_fun fn x2,apply_fun fn x1)) eps1)) (metric_epsilon_delta_continuity X dX Y dY fn HdX HdY Hfn) Hfncont).
Apply (Hedfn x0 Hx0X eta (andI (eta ∈ R) (Rlt 0 eta) HetaR HetaPos)) to the current goal.
Let delta be given.
Assume Hdelta.
We prove the intermediate claim Hdelta12: delta ∈ R ∧ Rlt 0 delta.
An exact proof term for the current goal is (andEL (delta ∈ R ∧ Rlt 0 delta) (∀x2 : set, x2 ∈ X → Rlt (apply_fun dX (x2,x0)) delta → Rlt (apply_fun dY (apply_fun fn x2,apply_fun fn x0)) eta) Hdelta).
We prove the intermediate claim HdeltaImp: ∀x2 : set, x2 ∈ X → Rlt (apply_fun dX (x2,x0)) delta → Rlt (apply_fun dY (apply_fun fn x2,apply_fun fn x0)) eta.
An exact proof term for the current goal is (andER (delta ∈ R ∧ Rlt 0 delta) (∀x2 : set, x2 ∈ X → Rlt (apply_fun dX (x2,x0)) delta → Rlt (apply_fun dY (apply_fun fn x2,apply_fun fn x0)) eta) Hdelta).
We use delta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hdelta12.
Let x be given.
Assume HxX: x ∈ X.
Assume Hdx: Rlt (apply_fun dX (x,x0)) delta.
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 Hfx0Y: apply_fun f x0 ∈ Y.
An exact proof term for the current goal is (Hf x0 Hx0X).
We prove the intermediate claim HfnxY: apply_fun fn x ∈ Y.
An exact proof term for the current goal is (Hfn x HxX).
We prove the intermediate claim Hfnx0Y: apply_fun fn x0 ∈ Y.
An exact proof term for the current goal is (Hfn x0 Hx0X).
We prove the intermediate claim HNuSub: Nu ⊆ Nu.
Let u be given.
Assume Hu: u ∈ Nu.
An exact proof term for the current goal is Hu.
We prove the intermediate claim Huc1: Rlt (apply_fun dY (apply_fun fn x,apply_fun f x)) eta.
An exact proof term for the current goal is (HNuprop Nu HNuomega HNuSub x HxX).
We prove the intermediate claim Huc2: Rlt (apply_fun dY (apply_fun fn x0,apply_fun f x0)) eta.
An exact proof term for the current goal is (HNuprop Nu HNuomega HNuSub x0 Hx0X).
We prove the intermediate claim Hsym1: apply_fun dY (apply_fun f x,apply_fun fn x) = apply_fun dY (apply_fun fn x,apply_fun f x).
An exact proof term for the current goal is (metric_on_symmetric Y dY (apply_fun f x) (apply_fun fn x) HdY HfxY HfnxY).
We prove the intermediate claim Hsym2: apply_fun dY (apply_fun fn x0,apply_fun f x0) = apply_fun dY (apply_fun f x0,apply_fun fn x0).
An exact proof term for the current goal is (metric_on_symmetric Y dY (apply_fun fn x0) (apply_fun f x0) HdY Hfnx0Y Hfx0Y).
We prove the intermediate claim Hp: Rlt (apply_fun dY (apply_fun f x,apply_fun fn x)) eta.
rewrite the current goal using Hsym1 (from left to right).
An exact proof term for the current goal is Huc1.
We prove the intermediate claim Hr: Rlt (apply_fun dY (apply_fun fn x0,apply_fun f x0)) eta.
An exact proof term for the current goal is Huc2.
We prove the intermediate claim Hq: Rlt (apply_fun dY (apply_fun fn x,apply_fun fn x0)) eta.
An exact proof term for the current goal is (HdeltaImp x HxX Hdx).
Set p to be the term apply_fun dY (apply_fun f x,apply_fun fn x).
Set q to be the term apply_fun dY (apply_fun fn x,apply_fun fn x0).
Set r to be the term apply_fun dY (apply_fun fn x0,apply_fun f x0).
We prove the intermediate claim HpR: p ∈ R.
An exact proof term for the current goal is ((metric_on_function_on Y dY HdY) (apply_fun f x,apply_fun fn x) (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun f x) (apply_fun fn x) HfxY HfnxY)).
We prove the intermediate claim HqR: q ∈ R.
An exact proof term for the current goal is ((metric_on_function_on Y dY HdY) (apply_fun fn x,apply_fun fn x0) (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun fn x) (apply_fun fn x0) HfnxY Hfnx0Y)).
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is ((metric_on_function_on Y dY HdY) (apply_fun fn x0,apply_fun f x0) (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun fn x0) (apply_fun f x0) Hfnx0Y Hfx0Y)).
We prove the intermediate claim Hpdlt: p < eta.
An exact proof term for the current goal is (RltE_lt p eta Hp).
We prove the intermediate claim Hqdlt: q < eta.
An exact proof term for the current goal is (RltE_lt q eta Hq).
We prove the intermediate claim Hrdlt: r < eta.
An exact proof term for the current goal is (RltE_lt r eta Hr).
We prove the intermediate claim HpS: SNo p.
An exact proof term for the current goal is (real_SNo p HpR).
We prove the intermediate claim HqS: SNo q.
An exact proof term for the current goal is (real_SNo q HqR).
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim Hsumqr_lt: add_SNo q r < add_SNo eta eta.
We prove the intermediate claim Ht1: add_SNo q r < add_SNo q eta.
An exact proof term for the current goal is (add_SNo_Lt2 q r eta HqS HrS HetaS Hrdlt).
We prove the intermediate claim Ht2: add_SNo q eta < add_SNo eta eta.
An exact proof term for the current goal is (add_SNo_Lt1 q eta eta HqS HetaS HetaS Hqdlt).
An exact proof term for the current goal is (SNoLt_tra (add_SNo q r) (add_SNo q eta) (add_SNo eta eta) (SNo_add_SNo q r HqS HrS) (SNo_add_SNo q eta HqS HetaS) (SNo_add_SNo eta eta HetaS HetaS) Ht1 Ht2).
We prove the intermediate claim Hsum_pqr_lt: add_SNo p (add_SNo q r) < add_SNo eta (add_SNo eta eta).
We prove the intermediate claim Ht1: add_SNo p (add_SNo q r) < add_SNo p (add_SNo eta eta).
An exact proof term for the current goal is (add_SNo_Lt2 p (add_SNo q r) (add_SNo eta eta) HpS (SNo_add_SNo q r HqS HrS) (SNo_add_SNo eta eta HetaS HetaS) Hsumqr_lt).
We prove the intermediate claim Ht2: add_SNo p (add_SNo eta eta) < add_SNo eta (add_SNo eta eta).
An exact proof term for the current goal is (add_SNo_Lt1 p (add_SNo eta eta) eta HpS (SNo_add_SNo eta eta HetaS HetaS) HetaS Hpdlt).
An exact proof term for the current goal is (SNoLt_tra (add_SNo p (add_SNo q r)) (add_SNo p (add_SNo eta eta)) (add_SNo eta (add_SNo eta eta)) (SNo_add_SNo p (add_SNo q r) HpS (SNo_add_SNo q r HqS HrS)) (SNo_add_SNo p (add_SNo eta eta) HpS (SNo_add_SNo eta eta HetaS HetaS)) (SNo_add_SNo eta (add_SNo eta eta) HetaS (SNo_add_SNo eta eta HetaS HetaS)) Ht1 Ht2).
We prove the intermediate claim Heta2eq: add_SNo eta eta = eps_ (ordsucc N0).
An exact proof term for the current goal is (eps_ordsucc_half_add (ordsucc N0) (omega_nat_p (ordsucc N0) Hsucc0)).
We prove the intermediate claim Heta4eq: add_SNo (add_SNo eta eta) (add_SNo eta eta) = eps_ N0.
rewrite the current goal using Heta2eq (from left to right).
An exact proof term for the current goal is (eps_ordsucc_half_add N0 HN0nat).
We prove the intermediate claim Heta3lt_eta4: add_SNo (add_SNo eta eta) eta < add_SNo (add_SNo eta eta) (add_SNo eta eta).
We prove the intermediate claim Heta_lt_2eta: eta < add_SNo eta eta.
We prove the intermediate claim H0lt: 0 < eta.
An exact proof term for the current goal is H0lt_eta.
We prove the intermediate claim H0ltR: Rlt 0 eta.
An exact proof term for the current goal is HetaPos.
We prove the intermediate claim H0ltS: 0 < eta.
An exact proof term for the current goal is H0lt.
We prove the intermediate claim H0lt2: add_SNo 0 eta < add_SNo eta eta.
An exact proof term for the current goal is (add_SNo_Lt1 0 eta eta SNo_0 HetaS HetaS H0ltS).
rewrite the current goal using (add_SNo_0L eta HetaS) (from right to left) at position 1.
An exact proof term for the current goal is H0lt2.
An exact proof term for the current goal is (add_SNo_Lt2 (add_SNo eta eta) eta (add_SNo eta eta) (SNo_add_SNo eta eta HetaS HetaS) HetaS (SNo_add_SNo eta eta HetaS HetaS) Heta_lt_2eta).
We prove the intermediate claim Heta3lt_epsN0: add_SNo (add_SNo eta eta) eta < eps_ N0.
rewrite the current goal using Heta4eq (from right to left).
An exact proof term for the current goal is Heta3lt_eta4.
We prove the intermediate claim HepsN0R: eps_ N0 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ N0) (SNo_eps_SNoS_omega N0 HN0omega)).
We prove the intermediate claim HepsN0S: SNo (eps_ N0).
An exact proof term for the current goal is (real_SNo (eps_ N0) HepsN0R).
We prove the intermediate claim Heta3S: SNo (add_SNo (add_SNo eta eta) eta).
An exact proof term for the current goal is (SNo_add_SNo (add_SNo eta eta) eta (SNo_add_SNo eta eta HetaS HetaS) HetaS).
We prove the intermediate claim Heta3lt_eps: add_SNo (add_SNo eta eta) eta < eps.
An exact proof term for the current goal is (SNoLt_tra (add_SNo (add_SNo eta eta) eta) (eps_ N0) eps Heta3S HepsN0S (real_SNo eps HepsR) Heta3lt_epsN0 HepsN0lt).
We prove the intermediate claim Hsumlt_eps: add_SNo p (add_SNo q r) < eps.
We prove the intermediate claim Hmid: add_SNo eta (add_SNo eta eta) < eps.
rewrite the current goal using (add_SNo_assoc eta eta eta HetaS HetaS HetaS) (from left to right).
An exact proof term for the current goal is Heta3lt_eps.
An exact proof term for the current goal is (SNoLt_tra (add_SNo p (add_SNo q r)) (add_SNo eta (add_SNo eta eta)) eps (SNo_add_SNo p (add_SNo q r) HpS (SNo_add_SNo q r HqS HrS)) (SNo_add_SNo eta (add_SNo eta eta) HetaS (SNo_add_SNo eta eta HetaS HetaS)) (real_SNo eps HepsR) Hsum_pqr_lt Hmid).
We prove the intermediate claim HsumR: add_SNo p (add_SNo q r) ∈ R.
An exact proof term for the current goal is (real_add_SNo p HpR (add_SNo q r) (real_add_SNo q HqR r HrR)).
We prove the intermediate claim HsumRlt: Rlt (add_SNo p (add_SNo q r)) eps.
An exact proof term for the current goal is (RltI (add_SNo p (add_SNo q r)) eps HsumR HepsR Hsumlt_eps).
We prove the intermediate claim Htri1: Rle (apply_fun dY (apply_fun f x,apply_fun f x0)) (add_SNo p (apply_fun dY (apply_fun fn x,apply_fun f x0))).
An exact proof term for the current goal is (metric_triangle_Rle Y dY (apply_fun f x) (apply_fun fn x) (apply_fun f x0) HdY HfxY HfnxY Hfx0Y).
We prove the intermediate claim Htri2: Rle (apply_fun dY (apply_fun fn x,apply_fun f x0)) (add_SNo q r).
An exact proof term for the current goal is (metric_triangle_Rle Y dY (apply_fun fn x) (apply_fun fn x0) (apply_fun f x0) HdY HfnxY Hfnx0Y Hfx0Y).
We prove the intermediate claim Hadd: Rle (add_SNo p (apply_fun dY (apply_fun fn x,apply_fun f x0))) (add_SNo p (add_SNo q r)).
An exact proof term for the current goal is (Rle_add_SNo_2 p (apply_fun dY (apply_fun fn x,apply_fun f x0)) (add_SNo q r) HpR ((metric_on_function_on Y dY HdY) (apply_fun fn x,apply_fun f x0) (tuple_2_setprod_by_pair_Sigma Y Y (apply_fun fn x) (apply_fun f x0) HfnxY Hfx0Y)) (real_add_SNo q HqR r HrR) Htri2).
We prove the intermediate claim Htri3: Rle (apply_fun dY (apply_fun f x,apply_fun f x0)) (add_SNo p (add_SNo q r)).
An exact proof term for the current goal is (Rle_tra (apply_fun dY (apply_fun f x,apply_fun f x0)) (add_SNo p (apply_fun dY (apply_fun fn x,apply_fun f x0))) (add_SNo p (add_SNo q r)) Htri1 Hadd).
An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun dY (apply_fun f x,apply_fun f x0)) (add_SNo p (add_SNo q r)) eps Htri3 HsumRlt).
An exact proof term for the current goal is (iffER (continuous_map X (metric_topology X dX) Y (metric_topology Y dY) f) (∀x0 : set, x0 ∈ X → ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃delta : set, delta ∈ R ∧ Rlt 0 delta ∧ (∀x : set, x ∈ X → Rlt (apply_fun dX (x,x0)) delta → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps)) (metric_epsilon_delta_continuity X dX Y dY f HdX HdY Hf) Hed).
∎