Let X, Tx, Y, dY, H, x0, eps, r, Ty, eval0, Img0, FamBalls and Gballs be given.
Assume HTx: topology_on X Tx.
Assume HdY: metric_on Y dY.
Assume HTyEq: Ty = metric_topology Y dY.
Assume Hlc: locally_compact X Tx.
Assume HHx: Hausdorff_space X Tx.
Assume HHsub: H ⊆ continuous_function_space X Tx Y (metric_topology Y dY).
Assume Hcomp: compact_space H (subspace_topology (continuous_function_space X Tx Y (metric_topology Y dY)) (compact_open_topology_C X Tx Y (metric_topology Y dY)) H).
Assume Heval0Def: eval0 = graph (function_space X Y) (λf : set ⇒ apply_fun f x0).
Assume Hx0X: x0 ∈ X.
Assume HepsR: eps ∈ R.
Assume HepsPos: Rlt 0 eps.
Assume HrR: r ∈ R.
Assume HrPos: Rlt 0 r.
Assume Hr4lt: Rlt (add_SNo (add_SNo r r) (add_SNo r r)) eps.
Assume HImg0Eq: Img0 = image_of_fun eval0 H.
Assume HFamEq: FamBalls = {open_ball Y dY y r|y ∈ Img0}.
Assume HGsub: Gballs ⊆ FamBalls.
Let b be given.
Assume HbG: b ∈ Gballs.
We prove the intermediate claim HTy: topology_on Y Ty.
rewrite the current goal using HTyEq (from left to right).
An exact proof term for the current goal is (metric_topology_is_topology Y dY HdY).
Set CXY to be the term continuous_function_space X Tx Y Ty.
Set Tco to be the term compact_open_topology_C X Tx Y Ty.
Set TH to be the term subspace_topology CXY Tco H.
We prove the intermediate claim HHsubTy: H ⊆ CXY.
rewrite the current goal using HTyEq (from left to right).
An exact proof term for the current goal is HHsub.
We prove the intermediate claim HcompTy: compact_space H TH.
rewrite the current goal using HTyEq (from left to right).
An exact proof term for the current goal is Hcomp.
We prove the intermediate claim HbFam: b ∈ FamBalls.
An exact proof term for the current goal is (HGsub b HbG).
We prove the intermediate claim HbFam': b ∈ {open_ball Y dY y r|y ∈ Img0}.
rewrite the current goal using HFamEq (from right to left).
An exact proof term for the current goal is HbFam.
Apply (ReplE_impred Img0 (λy0 : set ⇒ open_ball Y dY y0 r) b HbFam') to the current goal.
Let y0 be given.
Assume Hy0Img: y0 ∈ Img0.
Assume Hbeq: b = open_ball Y dY y0 r.
We prove the intermediate claim Hy0Im: y0 ∈ image_of_fun eval0 H.
rewrite the current goal using HImg0Eq (from right to left).
An exact proof term for the current goal is Hy0Img.
We prove the intermediate claim Hy0Y: y0 ∈ Y.
Apply (ReplE_impred H (λf0 : set ⇒ apply_fun eval0 f0) y0 Hy0Im (y0 ∈ Y)) to the current goal.
Let f0 be given.
Assume Hf0H: f0 ∈ H.
Assume Hy0Eq: y0 = apply_fun eval0 f0.
rewrite the current goal using Hy0Eq (from left to right).
We prove the intermediate claim Hf0CXY: f0 ∈ continuous_function_space X Tx Y (metric_topology Y dY).
An exact proof term for the current goal is (HHsub f0 Hf0H).
We prove the intermediate claim HCsubFS: continuous_function_space X Tx Y (metric_topology Y dY) ⊆ function_space X Y.
An exact proof term for the current goal is (continuous_function_space_sub X Tx Y (metric_topology Y dY)).
We prove the intermediate claim Hf0FS: f0 ∈ function_space X Y.
An exact proof term for the current goal is (HCsubFS f0 Hf0CXY).
We prove the intermediate claim Hf0fun: function_on f0 X Y.
An exact proof term for the current goal is (function_on_of_function_space f0 X Y Hf0FS).
rewrite the current goal using Heval0Def (from left to right).
rewrite the current goal using (apply_fun_graph (function_space X Y) (λf1 : set ⇒ apply_fun f1 x0) f0 Hf0FS) (from left to right).
An exact proof term for the current goal is (Hf0fun x0 Hx0X).
Set rr to be the term add_SNo r r.
We prove the intermediate claim HclSub: closure_of Y Ty b ⊆ open_ball Y dY y0 rr.
rewrite the current goal using Hbeq (from left to right).
rewrite the current goal using HTyEq (from left to right).
An exact proof term for the current goal is (closure_open_ball_sub_open_ball_add_radius Y dY y0 r HdY Hy0Y HrR HrPos).
Set Clb to be the term closure_of Y Ty b.
Set Hb to be the term preimage_of H eval0 Clb.
We prove the intermediate claim HHbSubH: Hb ⊆ H.
Let f0 be given.
Assume Hf0: f0 ∈ Hb.
An exact proof term for the current goal is (SepE1 H (λg0 : set ⇒ apply_fun eval0 g0 ∈ Clb) f0 Hf0).
Set DomFS to be the term function_space X Y.
Set Tcc to be the term compact_convergence_topology X Tx Y Ty.
We prove the intermediate claim HTcc: topology_on DomFS Tcc.
An exact proof term for the current goal is (compact_convergence_topology_is_topology X Tx Y Ty HTx HTy).
We prove the intermediate claim HCXYsubFS: CXY ⊆ DomFS.
An exact proof term for the current goal is (continuous_function_space_sub X Tx Y Ty).
We prove the intermediate claim Heval0FS: continuous_map DomFS Tcc Y Ty eval0.
rewrite the current goal using Heval0Def (from left to right).
An exact proof term for the current goal is (compact_convergence_eval_continuous X Tx Y Ty x0 HTx HTy Hx0X).
We prove the intermediate claim Heval0CXY: continuous_map CXY Tco Y Ty eval0.
An exact proof term for the current goal is (continuous_on_subspace_rule DomFS Tcc Y Ty eval0 CXY HTcc HTy HCXYsubFS Heval0FS).
We prove the intermediate claim HTco: topology_on CXY Tco.
An exact proof term for the current goal is (compact_open_topology_C_is_topology X Tx Y Ty HTx HTy).
We prove the intermediate claim Heval0H: continuous_map H TH Y Ty eval0.
An exact proof term for the current goal is (continuous_on_subspace_rule CXY Tco Y Ty eval0 H HTco HTy HHsubTy Heval0CXY).
We prove the intermediate claim HbsubY: b ⊆ Y.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (open_ball_subset_X Y dY y0 r).
We prove the intermediate claim HclClb: closed_in Y Ty Clb.
An exact proof term for the current goal is (closure_is_closed Y Ty b HTy HbsubY).
We prove the intermediate claim HHbClosed: closed_in H TH Hb.
An exact proof term for the current goal is (continuous_map_preimage_closed H TH Y Ty eval0 Clb Heval0H HclClb).
We prove the intermediate claim HHbComp: compact_space Hb (subspace_topology H TH Hb).
An exact proof term for the current goal is (closed_subspace_compact H TH Hb HcompTy HHbClosed).
Set THb to be the term subspace_topology CXY Tco Hb.
We prove the intermediate claim HTHbEq: subspace_topology H TH Hb = THb.
An exact proof term for the current goal is (ex16_1_subspace_transitive CXY Tco H Hb HTco HHsubTy HHbSubH).
We prove the intermediate claim HHbComp2: compact_space Hb THb.
rewrite the current goal using HTHbEq (from right to left).
An exact proof term for the current goal is HHbComp.
We prove the intermediate claim HTHb: topology_on Hb THb.
An exact proof term for the current goal is (compact_space_topology Hb THb HHbComp2).
We prove the intermediate claim HHbSubCXY: Hb ⊆ CXY.
Let f0 be given.
Assume Hf0Hb: f0 ∈ Hb.
We prove the intermediate claim Hf0H: f0 ∈ H.
An exact proof term for the current goal is (HHbSubH f0 Hf0Hb).
An exact proof term for the current goal is (HHsubTy f0 Hf0H).
Set Dom0 to be the term setprod X CXY.
Set Tdom0 to be the term product_topology X Tx CXY Tco.
Set ev to be the term compact_open_evaluation_map X Tx Y Ty.
We prove the intermediate claim Hev0: continuous_map Dom0 Tdom0 Y Ty ev.
An exact proof term for the current goal is (compact_open_evaluation_continuous X Tx Y Ty Hlc HHx HTy).
We prove the intermediate claim HTdom0: topology_on Dom0 Tdom0.
An exact proof term for the current goal is (product_topology_is_topology X Tx CXY Tco HTx HTco).
Set DomHb to be the term setprod X Hb.
We prove the intermediate claim HDomHbSub: DomHb ⊆ Dom0.
An exact proof term for the current goal is (setprod_Subq X Hb X CXY (Subq_ref X) HHbSubCXY).
We prove the intermediate claim HevHb_sub: continuous_map DomHb (subspace_topology Dom0 Tdom0 DomHb) Y Ty ev.
An exact proof term for the current goal is (continuous_on_subspace_rule Dom0 Tdom0 Y Ty ev DomHb HTdom0 HTy HDomHbSub Hev0).
We prove the intermediate claim HTxWhole: subspace_topology X Tx X = Tx.
An exact proof term for the current goal is (subspace_topology_whole X Tx HTx).
We prove the intermediate claim HprodSubEq: product_topology X Tx Hb THb = subspace_topology Dom0 Tdom0 DomHb.
We prove the intermediate claim HTHbdef: THb = subspace_topology CXY Tco Hb.
Use reflexivity.
We prove the intermediate claim HDom0def: Dom0 = setprod X CXY.
Use reflexivity.
We prove the intermediate claim HTdom0def: Tdom0 = product_topology X Tx CXY Tco.
Use reflexivity.
We prove the intermediate claim HDomHbdef: DomHb = setprod X Hb.
Use reflexivity.
rewrite the current goal using HTHbdef (from left to right).
rewrite the current goal using HDom0def (from left to right).
rewrite the current goal using HTdom0def (from left to right).
rewrite the current goal using HDomHbdef (from left to right).
rewrite the current goal using HTxWhole (from right to left) at position 1.
An exact proof term for the current goal is (product_subspace_topology X Tx CXY Tco X Hb HTx HTco (Subq_ref X) HHbSubCXY).
We prove the intermediate claim HevHb: continuous_map DomHb (product_topology X Tx Hb THb) Y Ty ev.
rewrite the current goal using HprodSubEq (from left to right).
An exact proof term for the current goal is HevHb_sub.
We prove the intermediate claim HrrR: rr ∈ R.
An exact proof term for the current goal is (real_add_SNo r HrR r HrR).
We prove the intermediate claim HrrPos: Rlt 0 rr.
We prove the intermediate claim H0lt: Rlt (add_SNo 0 0) rr.
An exact proof term for the current goal is (Rlt_add_SNo 0 r 0 r HrPos HrPos).
We prove the intermediate claim H00eq: add_SNo 0 0 = 0.
An exact proof term for the current goal is (add_SNo_0L 0 SNo_0).
rewrite the current goal using H00eq (from right to left) at position 1.
An exact proof term for the current goal is H0lt.
Set V to be the term open_ball Y dY y0 rr.
We prove the intermediate claim HV: V ∈ Ty.
rewrite the current goal using HTyEq (from left to right).
An exact proof term for the current goal is (open_ball_in_metric_topology Y dY y0 rr HdY Hy0Y HrrPos).
Set N to be the term preimage_of DomHb ev V.
We prove the intermediate claim HNopen: N ∈ product_topology X Tx Hb THb.
An exact proof term for the current goal is (continuous_map_preimage DomHb (product_topology X Tx Hb THb) Y Ty ev HevHb V HV).
We prove the intermediate claim Hx0HbSubN: setprod {x0} Hb ⊆ N.
Let p be given.
Assume Hp: p ∈ setprod {x0} Hb.
We will prove p ∈ N.
We prove the intermediate claim HsingSubX: {x0} ⊆ X.
Let t be given.
Assume Ht: t ∈ {x0}.
We prove the intermediate claim Hteq: t = x0.
An exact proof term for the current goal is (SingE x0 t Ht).
rewrite the current goal using Hteq (from left to right).
An exact proof term for the current goal is Hx0X.
We prove the intermediate claim HsubProd: setprod {x0} Hb ⊆ DomHb.
An exact proof term for the current goal is (setprod_Subq {x0} Hb X Hb HsingSubX (Subq_ref Hb)).
We prove the intermediate claim HpDomHb: p ∈ DomHb.
An exact proof term for the current goal is (HsubProd p Hp).
We prove the intermediate claim HevIn: apply_fun ev p ∈ V.
We prove the intermediate claim Hp0: p 0 ∈ {x0}.
An exact proof term for the current goal is (ap0_Sigma {x0} (λ_ : set ⇒ Hb) p Hp).
We prove the intermediate claim Hp1: p 1 ∈ Hb.
An exact proof term for the current goal is (ap1_Sigma {x0} (λ_ : set ⇒ Hb) p Hp).
We prove the intermediate claim Hp0eq: p 0 = x0.
An exact proof term for the current goal is (SingE x0 (p 0) Hp0).
We prove the intermediate claim Hp1Clb: apply_fun eval0 (p 1) ∈ Clb.
An exact proof term for the current goal is (SepE2 H (λg0 : set ⇒ apply_fun eval0 g0 ∈ Clb) (p 1) Hp1).
We prove the intermediate claim Hp1V0: apply_fun eval0 (p 1) ∈ V.
An exact proof term for the current goal is (HclSub (apply_fun eval0 (p 1)) Hp1Clb).
We prove the intermediate claim HpHbDom0: p ∈ Dom0.
An exact proof term for the current goal is (HDomHbSub p HpDomHb).
We prove the intermediate claim Hp1CXY: p 1 ∈ CXY.
An exact proof term for the current goal is (HHbSubCXY (p 1) Hp1).
We prove the intermediate claim Hp1FS: p 1 ∈ function_space X Y.
An exact proof term for the current goal is (HCXYsubFS (p 1) Hp1CXY).
We prove the intermediate claim Hevdef: ev = graph Dom0 (λq : set ⇒ apply_fun (q 1) (q 0)).
Use reflexivity.
rewrite the current goal using Hevdef (from left to right).
rewrite the current goal using (apply_fun_graph Dom0 (λq : set ⇒ apply_fun (q 1) (q 0)) p HpHbDom0) (from left to right).
rewrite the current goal using Hp0eq (from left to right).
We prove the intermediate claim HeqEv0: apply_fun eval0 (p 1) = apply_fun (p 1) x0.
rewrite the current goal using Heval0Def (from left to right).
An exact proof term for the current goal is (apply_fun_graph (function_space X Y) (λf1 : set ⇒ apply_fun f1 x0) (p 1) Hp1FS).
rewrite the current goal using HeqEv0 (from right to left) at position 1.
An exact proof term for the current goal is Hp1V0.
An exact proof term for the current goal is (SepI DomHb (λq : set ⇒ apply_fun ev q ∈ V) p HpDomHb HevIn).
We prove the intermediate claim HexU: ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ setprod U Hb ⊆ N.
Apply (tube_lemma X Tx Hb THb HTx HTHb HHbComp2 x0 Hx0X N) to the current goal.
An exact proof term for the current goal is (andI (N ∈ product_topology X Tx Hb THb) (setprod {x0} Hb ⊆ N) HNopen Hx0HbSubN).
Apply HexU to the current goal.
Let U be given.
Assume HUpack.
We prove the intermediate claim HUand: U ∈ Tx ∧ x0 ∈ U.
An exact proof term for the current goal is (andEL (U ∈ Tx ∧ x0 ∈ U) (setprod U Hb ⊆ N) HUpack).
We prove the intermediate claim HUopen: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (x0 ∈ U) HUand).
We prove the intermediate claim Hx0U: x0 ∈ U.
An exact proof term for the current goal is (andER (U ∈ Tx) (x0 ∈ U) HUand).
We prove the intermediate claim HUsubN: setprod U Hb ⊆ N.
An exact proof term for the current goal is (andER (U ∈ Tx ∧ x0 ∈ U) (setprod U Hb ⊆ N) HUpack).
We use U to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HUopen.
An exact proof term for the current goal is Hx0U.
Let f be given.
Assume HfH: f ∈ H.
Assume HfCl: apply_fun eval0 f ∈ Clb.
Let x1 be given.
Assume Hx1X: x1 ∈ X.
Assume Hx1U: x1 ∈ U.
We prove the intermediate claim HfHb: f ∈ Hb.
An exact proof term for the current goal is (SepI H (λg0 : set ⇒ apply_fun eval0 g0 ∈ Clb) f HfH HfCl).
We prove the intermediate claim HpDomHb: (x1,f) ∈ DomHb.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X Hb x1 f Hx1X HfHb).
We prove the intermediate claim HpDomN: (x1,f) ∈ N.
We prove the intermediate claim HpProd: (x1,f) ∈ setprod U Hb.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma U Hb x1 f Hx1U HfHb).
An exact proof term for the current goal is (HUsubN (x1,f) HpProd).
We prove the intermediate claim Hfx1V: apply_fun ev (x1,f) ∈ V.
An exact proof term for the current goal is (SepE2 DomHb (λq : set ⇒ apply_fun ev q ∈ V) (x1,f) HpDomN).
Set fx1 to be the term apply_fun f x1.
Set fx0 to be the term apply_fun f x0.
We prove the intermediate claim HfCXY: f ∈ CXY.
An exact proof term for the current goal is (HHsubTy f HfH).
We prove the intermediate claim HfFS: f ∈ function_space X Y.
An exact proof term for the current goal is (continuous_function_space_sub X Tx Y Ty f HfCXY).
We prove the intermediate claim Hffun: function_on f X Y.
An exact proof term for the current goal is (function_on_of_function_space f X Y HfFS).
We prove the intermediate claim Hfx1Y: fx1 ∈ Y.
An exact proof term for the current goal is (Hffun x1 Hx1X).
We prove the intermediate claim Hfx0Y: fx0 ∈ Y.
An exact proof term for the current goal is (Hffun x0 Hx0X).
We prove the intermediate claim HpDom0: (x1,f) ∈ Dom0.
An exact proof term for the current goal is (HDomHbSub (x1,f) HpDomHb).
We prove the intermediate claim Hevdef: ev = graph Dom0 (λq : set ⇒ apply_fun (q 1) (q 0)).
Use reflexivity.
We prove the intermediate claim HevPair: apply_fun ev (x1,f) = fx1.
rewrite the current goal using Hevdef (from left to right).
rewrite the current goal using (apply_fun_graph Dom0 (λq : set ⇒ apply_fun (q 1) (q 0)) (x1,f) HpDom0) (from left to right).
rewrite the current goal using (tuple_2_1_eq x1 f) (from left to right).
rewrite the current goal using (tuple_2_0_eq x1 f) (from left to right).
Use reflexivity.
We prove the intermediate claim Hfx1Ball: fx1 ∈ open_ball Y dY y0 rr.
rewrite the current goal using HevPair (from right to left).
An exact proof term for the current goal is Hfx1V.
We prove the intermediate claim Hdy0_fx1: Rlt (apply_fun dY (y0,fx1)) rr.
An exact proof term for the current goal is (open_ballE2 Y dY y0 rr fx1 Hfx1Ball).
We prove the intermediate claim Heval0fx0: apply_fun eval0 f = fx0.
rewrite the current goal using Heval0Def (from left to right).
An exact proof term for the current goal is (apply_fun_graph (function_space X Y) (λf1 : set ⇒ apply_fun f1 x0) f HfFS).
We prove the intermediate claim Hfx0Ball: fx0 ∈ open_ball Y dY y0 rr.
We prove the intermediate claim Htmp: apply_fun eval0 f ∈ open_ball Y dY y0 rr.
An exact proof term for the current goal is (HclSub (apply_fun eval0 f) HfCl).
rewrite the current goal using Heval0fx0 (from right to left).
An exact proof term for the current goal is Htmp.
We prove the intermediate claim Hdy0_fx0: Rlt (apply_fun dY (y0,fx0)) rr.
An exact proof term for the current goal is (open_ballE2 Y dY y0 rr fx0 Hfx0Ball).
We prove the intermediate claim Hsym1: apply_fun dY (fx1,y0) = apply_fun dY (y0,fx1).
An exact proof term for the current goal is (metric_on_symmetric Y dY fx1 y0 HdY Hfx1Y Hy0Y).
We prove the intermediate claim Hdfx1y0: Rlt (apply_fun dY (fx1,y0)) rr.
rewrite the current goal using Hsym1 (from left to right).
An exact proof term for the current goal is Hdy0_fx1.
We prove the intermediate claim Htri: Rle (apply_fun dY (fx1,fx0)) (add_SNo (apply_fun dY (fx1,y0)) (apply_fun dY (y0,fx0))).
An exact proof term for the current goal is (metric_triangle_Rle Y dY fx1 y0 fx0 HdY Hfx1Y Hy0Y Hfx0Y).
We prove the intermediate claim Haddlt: Rlt (add_SNo (apply_fun dY (fx1,y0)) (apply_fun dY (y0,fx0))) (add_SNo rr rr).
An exact proof term for the current goal is (Rlt_add_SNo (apply_fun dY (fx1,y0)) rr (apply_fun dY (y0,fx0)) rr Hdfx1y0 Hdy0_fx0).
We prove the intermediate claim Hrr2lt: Rlt (add_SNo rr rr) eps.
An exact proof term for the current goal is Hr4lt.
We prove the intermediate claim Hsumlt: Rlt (add_SNo (apply_fun dY (fx1,y0)) (apply_fun dY (y0,fx0))) eps.
An exact proof term for the current goal is (Rlt_tra (add_SNo (apply_fun dY (fx1,y0)) (apply_fun dY (y0,fx0))) (add_SNo rr rr) eps Haddlt Hrr2lt).
An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun dY (fx1,fx0)) (add_SNo (apply_fun dY (fx1,y0)) (apply_fun dY (y0,fx0))) eps Htri Hsumlt).
∎