Let X, Tx, Y, dY and H be given.
Assume HTx: topology_on X Tx.
Assume HdY: metric_on 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).
Set Ty to be the term metric_topology Y dY.
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 HTy: topology_on Y Ty.
An exact proof term for the current goal is (metric_topology_is_topology Y dY HdY).
We will prove equicontinuous_family X Tx Y dY H.
We will prove topology_on X Tx ∧ metric_on Y dY ∧ H ⊆ continuous_function_space X Tx Y (metric_topology Y dY) ∧ ∀x0 : set, x0 ∈ X → ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃U : set, U ∈ Tx ∧ x0 ∈ U ∧ ∀f : set, f ∈ H → ∀x : set, x ∈ X → x ∈ U → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) 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 HTx.
An exact proof term for the current goal is HdY.
An exact proof term for the current goal is HHsub.
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 HexN: ∃N ∈ ω, eps_ N < eps.
An exact proof term for the current goal is (exists_eps_lt_pos eps HepsR HepsPos).
Apply HexN to the current goal.
Let N be given.
Assume HNpair.
We prove the intermediate claim HNomega: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (eps_ N < eps) HNpair).
We prove the intermediate claim HepsNlt: eps_ N < eps.
An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < eps) HNpair).
We prove the intermediate claim HepsNR: eps_ N ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ N) (SNo_eps_SNoS_omega N HNomega)).
We prove the intermediate claim HepsNRlt: Rlt (eps_ N) eps.
An exact proof term for the current goal is (RltI (eps_ N) eps HepsNR HepsR HepsNlt).
We prove the intermediate claim HNnat: nat_p N.
An exact proof term for the current goal is (omega_nat_p N HNomega).
Set N1 to be the term ordsucc N.
We prove the intermediate claim HN1omega: N1 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N HNomega).
We prove the intermediate claim HN1nat: nat_p N1.
An exact proof term for the current goal is (omega_nat_p N1 HN1omega).
Set N2 to be the term ordsucc N1.
We prove the intermediate claim HN2omega: N2 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N1 HN1omega).
We prove the intermediate claim HN2nat: nat_p N2.
An exact proof term for the current goal is (omega_nat_p N2 HN2omega).
Set r to be the term eps_ N2.
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (SNoS_omega_real r (SNo_eps_SNoS_omega N2 HN2omega)).
We prove the intermediate claim HrposS: 0 < r.
An exact proof term for the current goal is (SNo_eps_pos N2 HN2omega).
We prove the intermediate claim Hrpos: Rlt 0 r.
An exact proof term for the current goal is (RltI 0 r real_0 HrR HrposS).
Set rr to be the term add_SNo r r.
We prove the intermediate claim HrrEq: rr = eps_ N1.
An exact proof term for the current goal is (eps_ordsucc_half_add N1 HN1nat).
Set r4 to be the term add_SNo rr rr.
We prove the intermediate claim Hr4Eq: r4 = eps_ N.
rewrite the current goal using HrrEq (from left to right).
An exact proof term for the current goal is (eps_ordsucc_half_add N HNnat).
We prove the intermediate claim Hr4lt: Rlt r4 eps.
rewrite the current goal using Hr4Eq (from left to right).
An exact proof term for the current goal is HepsNRlt.
Set DomFS to be the term function_space X Y.
Set Tcc to be the term compact_convergence_topology X Tx Y Ty.
Set eval0 to be the term graph DomFS (λf : set ⇒ apply_fun f x0).
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.
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 HHsub Heval0CXY).
Set Img0 to be the term image_of_fun eval0 H.
We prove the intermediate claim HImg0comp: compact_space Img0 (subspace_topology Y Ty Img0).
An exact proof term for the current goal is (continuous_image_compact H TH Y Ty eval0 Hcomp Heval0H).
We prove the intermediate claim HfunEval0: function_on eval0 H Y.
An exact proof term for the current goal is (continuous_map_function_on H TH Y Ty eval0 Heval0H).
We prove the intermediate claim HImg0subY: Img0 ⊆ Y.
Let y be given.
Assume Hy: y ∈ Img0.
We will prove y ∈ Y.
Apply (ReplE_impred H (λf0 : set ⇒ apply_fun eval0 f0) y Hy (y ∈ Y)) to the current goal.
Let f0 be given.
Assume Hf0H: f0 ∈ H.
Assume HyEq: y = apply_fun eval0 f0.
rewrite the current goal using HyEq (from left to right).
An exact proof term for the current goal is (HfunEval0 f0 Hf0H).
Set FamBalls to be the term {open_ball Y dY y r|y ∈ Img0}.
We prove the intermediate claim HFamBallsSub: FamBalls ⊆ Ty.
Let b be given.
Assume Hb: b ∈ FamBalls.
We will prove b ∈ Ty.
Apply (ReplE_impred Img0 (λy0 : set ⇒ open_ball Y dY y0 r) b Hb (b ∈ Ty)) to the current goal.
Let y0 be given.
Assume Hy0Img: y0 ∈ Img0.
Assume HbEq: b = open_ball Y dY y0 r.
rewrite the current goal using HbEq (from left to right).
We prove the intermediate claim Hy0Y: y0 ∈ Y.
An exact proof term for the current goal is (HImg0subY y0 Hy0Img).
An exact proof term for the current goal is (open_ball_in_metric_topology Y dY y0 r HdY Hy0Y Hrpos).
We prove the intermediate claim HImg0covBalls: Img0 ⊆ ⋃ FamBalls.
Let y be given.
Assume HyImg: y ∈ Img0.
We will prove y ∈ ⋃ FamBalls.
Set b to be the term open_ball Y dY y r.
We prove the intermediate claim HbFam: b ∈ FamBalls.
An exact proof term for the current goal is (ReplI Img0 (λy0 : set ⇒ open_ball Y dY y0 r) y HyImg).
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (HImg0subY y HyImg).
We prove the intermediate claim Hyb: y ∈ b.
An exact proof term for the current goal is (center_in_open_ball Y dY y r HdY HyY Hrpos).
An exact proof term for the current goal is (UnionI FamBalls y b Hyb HbFam).
We prove the intermediate claim HcompAmb: ∀Fam : set, (Fam ⊆ Ty ∧ Img0 ⊆ ⋃ Fam) → has_finite_subcover Img0 Ty Fam.
An exact proof term for the current goal is (iffEL (compact_space Img0 (subspace_topology Y Ty Img0)) (∀Fam : set, (Fam ⊆ Ty ∧ Img0 ⊆ ⋃ Fam) → has_finite_subcover Img0 Ty Fam) (compact_subspace_via_ambient_covers Y Ty Img0 HTy HImg0subY) HImg0comp).
We prove the intermediate claim HcovPair: FamBalls ⊆ Ty ∧ Img0 ⊆ ⋃ FamBalls.
Apply andI to the current goal.
An exact proof term for the current goal is HFamBallsSub.
An exact proof term for the current goal is HImg0covBalls.
We prove the intermediate claim HfinSub: has_finite_subcover Img0 Ty FamBalls.
An exact proof term for the current goal is (HcompAmb FamBalls HcovPair).
Apply HfinSub to the current goal.
Let Gballs be given.
Assume HGballs.
We prove the intermediate claim HGleft: Gballs ⊆ FamBalls ∧ finite Gballs.
An exact proof term for the current goal is (andEL (Gballs ⊆ FamBalls ∧ finite Gballs) (Img0 ⊆ ⋃ Gballs) HGballs).
We prove the intermediate claim HGsub: Gballs ⊆ FamBalls.
An exact proof term for the current goal is (andEL (Gballs ⊆ FamBalls) (finite Gballs) HGleft).
We prove the intermediate claim HGfin: finite Gballs.
An exact proof term for the current goal is (andER (Gballs ⊆ FamBalls) (finite Gballs) HGleft).
We prove the intermediate claim HImg0covG: Img0 ⊆ ⋃ Gballs.
An exact proof term for the current goal is (andER (Gballs ⊆ FamBalls ∧ finite Gballs) (Img0 ⊆ ⋃ Gballs) HGballs).
Set Q to be the term λb U : set ⇒ U ∈ Tx ∧ x0 ∈ U ∧ ∀f : set, f ∈ H → apply_fun eval0 f ∈ closure_of Y Ty b → ∀x1 : set, x1 ∈ X → x1 ∈ U → Rlt (apply_fun dY (apply_fun f x1,apply_fun f x0)) eps.
We prove the intermediate claim HperBall: ∀b : set, b ∈ Gballs → ∃U : set, Q b U.
Let b be given.
Assume HbG: b ∈ Gballs.
We prove the intermediate claim HTyEq: Ty = metric_topology Y dY.
Use reflexivity.
We prove the intermediate claim Heval0Def: eval0 = graph (function_space X Y) (λf : set ⇒ apply_fun f x0).
Use reflexivity.
We prove the intermediate claim Hr4Form: r4 = add_SNo (add_SNo r r) (add_SNo r r).
Use reflexivity.
We prove the intermediate claim Hr4lt': Rlt (add_SNo (add_SNo r r) (add_SNo r r)) eps.
rewrite the current goal using Hr4Form (from right to left).
An exact proof term for the current goal is Hr4lt.
We prove the intermediate claim HImg0Eq: Img0 = image_of_fun eval0 H.
Use reflexivity.
We prove the intermediate claim HFamEq: FamBalls = {open_ball Y dY y r|y ∈ Img0}.
Use reflexivity.
Apply (compact_subspace_CXY_equicontinuous_per_ball X Tx Y dY H x0 eps r Ty eval0 Img0 FamBalls Gballs HTx HdY HTyEq Hlc HHx HHsub Hcomp Heval0Def Hx0X HepsR HepsPos HrR Hrpos Hr4lt' HImg0Eq HFamEq HGsub b HbG) to the current goal.
Set pickU to be the term λb : set ⇒ Eps_i (λU : set ⇒ Q b U).
Set UFam to be the term {pickU b|b ∈ Gballs}.
We prove the intermediate claim HUFamFin: finite UFam.
An exact proof term for the current goal is (Repl_finite (λb0 : set ⇒ pickU b0) Gballs HGfin).
We prove the intermediate claim HUFamSubTx: UFam ⊆ Tx.
Let U be given.
Assume HU: U ∈ UFam.
We will prove U ∈ Tx.
Apply (ReplE_impred Gballs (λb0 : set ⇒ pickU b0) U HU (U ∈ Tx)) to the current goal.
Let b be given.
Assume HbG: b ∈ Gballs.
Assume HUeq: U = pickU b.
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim Hex: ∃U0 : set, Q b U0.
An exact proof term for the current goal is (HperBall b HbG).
We prove the intermediate claim HQ: Q b (pickU b).
An exact proof term for the current goal is (Eps_i_ex (λU0 : set ⇒ Q b U0) Hex).
We prove the intermediate claim HQleft: pickU b ∈ Tx ∧ x0 ∈ pickU b.
An exact proof term for the current goal is (andEL (pickU b ∈ Tx ∧ x0 ∈ pickU b) (∀f : set, f ∈ H → apply_fun eval0 f ∈ closure_of Y Ty b → ∀x : set, x ∈ X → x ∈ pickU b → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps) HQ).
An exact proof term for the current goal is (andEL (pickU b ∈ Tx) (x0 ∈ pickU b) HQleft).
We prove the intermediate claim HUFamPow: UFam ∈ 𝒫 Tx.
An exact proof term for the current goal is (PowerI Tx UFam HUFamSubTx).
Set U to be the term intersection_of_family X UFam.
We prove the intermediate claim HUopen: U ∈ Tx.
An exact proof term for the current goal is (finite_intersection_in_topology X Tx UFam HTx HUFamPow HUFamFin).
We prove the intermediate claim Hx0U: x0 ∈ U.
We prove the intermediate claim HUdef: U = intersection_of_family X UFam.
Use reflexivity.
We prove the intermediate claim HallU: ∀U0 : set, U0 ∈ UFam → x0 ∈ U0.
Let U0 be given.
Assume HU0: U0 ∈ UFam.
We will prove x0 ∈ U0.
Apply (ReplE_impred Gballs (λb0 : set ⇒ pickU b0) U0 HU0 (x0 ∈ U0)) to the current goal.
Let b be given.
Assume HbG: b ∈ Gballs.
Assume HU0eq: U0 = pickU b.
rewrite the current goal using HU0eq (from left to right).
We prove the intermediate claim Hex: ∃U1 : set, Q b U1.
An exact proof term for the current goal is (HperBall b HbG).
We prove the intermediate claim HQ: Q b (pickU b).
An exact proof term for the current goal is (Eps_i_ex (λU1 : set ⇒ Q b U1) Hex).
We prove the intermediate claim HQleft: pickU b ∈ Tx ∧ x0 ∈ pickU b.
An exact proof term for the current goal is (andEL (pickU b ∈ Tx ∧ x0 ∈ pickU b) (∀f : set, f ∈ H → apply_fun eval0 f ∈ closure_of Y Ty b → ∀x : set, x ∈ X → x ∈ pickU b → Rlt (apply_fun dY (apply_fun f x,apply_fun f x0)) eps) HQ).
An exact proof term for the current goal is (andER (pickU b ∈ Tx) (x0 ∈ pickU b) HQleft).
rewrite the current goal using HUdef (from left to right).
An exact proof term for the current goal is (intersection_of_familyI X UFam x0 Hx0X HallU).
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.
Let x be given.
Assume HxX: x ∈ X.
Assume HxU: x ∈ U.
We prove the intermediate claim HvalInImg0: apply_fun eval0 f ∈ Img0.
An exact proof term for the current goal is (ReplI H (λf0 : set ⇒ apply_fun eval0 f0) f HfH).
We prove the intermediate claim HvalInUnion: apply_fun eval0 f ∈ ⋃ Gballs.
An exact proof term for the current goal is (HImg0covG (apply_fun eval0 f) HvalInImg0).
Apply (UnionE Gballs (apply_fun eval0 f) HvalInUnion) to the current goal.
Let b be given.
Assume HbPack.
We prove the intermediate claim HbG: b ∈ Gballs.
An exact proof term for the current goal is (andER (apply_fun eval0 f ∈ b) (b ∈ Gballs) HbPack).
We prove the intermediate claim HvalInb: apply_fun eval0 f ∈ b.
An exact proof term for the current goal is (andEL (apply_fun eval0 f ∈ b) (b ∈ Gballs) HbPack).
We prove the intermediate claim HbsubY: b ⊆ Y.
We prove the intermediate claim HbFam: b ∈ FamBalls.
An exact proof term for the current goal is (HGsub b HbG).
Apply (ReplE_impred Img0 (λy0 : set ⇒ open_ball Y dY y0 r) b HbFam (b ⊆ Y)) to the current goal.
Let y0 be given.
Assume Hy0Img: y0 ∈ Img0.
Assume Hbeq: b = open_ball Y dY y0 r.
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 HsubCl: b ⊆ closure_of Y Ty b.
An exact proof term for the current goal is (subset_of_closure Y Ty b HTy HbsubY).
We prove the intermediate claim HvalInCl: apply_fun eval0 f ∈ closure_of Y Ty b.
An exact proof term for the current goal is (HsubCl (apply_fun eval0 f) HvalInb).
We prove the intermediate claim Hex: ∃U1 : set, Q b U1.
An exact proof term for the current goal is (HperBall b HbG).
We prove the intermediate claim HQ: Q b (pickU b).
An exact proof term for the current goal is (Eps_i_ex (λU1 : set ⇒ Q b U1) Hex).
We prove the intermediate claim HxInUb: x ∈ pickU b.
An exact proof term for the current goal is (intersection_of_familyE2 X UFam x HxU (pickU b) (ReplI Gballs (λb0 : set ⇒ pickU b0) b HbG)).
We prove the intermediate claim HQright: ∀f0 : set, f0 ∈ H → apply_fun eval0 f0 ∈ closure_of Y Ty b → ∀x1 : set, x1 ∈ X → x1 ∈ pickU b → Rlt (apply_fun dY (apply_fun f0 x1,apply_fun f0 x0)) eps.
An exact proof term for the current goal is (andER (pickU b ∈ Tx ∧ x0 ∈ pickU b) (∀f0 : set, f0 ∈ H → apply_fun eval0 f0 ∈ closure_of Y Ty b → ∀x1 : set, x1 ∈ X → x1 ∈ pickU b → Rlt (apply_fun dY (apply_fun f0 x1,apply_fun f0 x0)) eps) HQ).
An exact proof term for the current goal is (HQright f HfH HvalInCl x HxX HxInUb).
∎