Let X, Tx, Y, dY and F be given.
Assume HTx: topology_on X Tx.
Assume HdY: metric_on Y dY.
Assume Hrel: relatively_compact_in_compact_convergence X Tx Y dY F.
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 Tcc to be the term compact_convergence_topology_metric_C X Tx Y dY.
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 prove the intermediate claim HHY: Hausdorff_space Y Ty.
An exact proof term for the current goal is (metric_topology_Hausdorff Y dY HdY).
We prove the intermediate claim HCXYsubDom: CXY ⊆ function_space X Y.
An exact proof term for the current goal is (continuous_function_space_sub X Tx Y Ty).
We prove the intermediate claim HFsubCXY: F ⊆ CXY.
An exact proof term for the current goal is (andEL (F ⊆ CXY) (∃H : set, F ⊆ H ∧ H ⊆ CXY ∧ compact_space H (subspace_topology CXY Tcc H)) Hrel).
We prove the intermediate claim HexH: ∃H : set, F ⊆ H ∧ H ⊆ CXY ∧ compact_space H (subspace_topology CXY Tcc H).
An exact proof term for the current goal is (andER (F ⊆ CXY) (∃H : set, F ⊆ H ∧ H ⊆ CXY ∧ compact_space H (subspace_topology CXY Tcc H)) Hrel).
Apply HexH to the current goal.
Let H be given.
Assume Hpack: F ⊆ H ∧ H ⊆ CXY ∧ compact_space H (subspace_topology CXY Tcc H).
We will prove Ascoli_pointwise_compact_closure X Y dY F.
We prove the intermediate claim Hmid: F ⊆ H ∧ H ⊆ CXY.
An exact proof term for the current goal is (andEL (F ⊆ H ∧ H ⊆ CXY) (compact_space H (subspace_topology CXY Tcc H)) Hpack).
We prove the intermediate claim HFsubH: F ⊆ H.
An exact proof term for the current goal is (andEL (F ⊆ H) (H ⊆ CXY) Hmid).
We prove the intermediate claim HHsubCXY: H ⊆ CXY.
An exact proof term for the current goal is (andER (F ⊆ H) (H ⊆ CXY) Hmid).
We prove the intermediate claim HcompHcc: compact_space H (subspace_topology CXY Tcc H).
An exact proof term for the current goal is (andER (F ⊆ H ∧ H ⊆ CXY) (compact_space H (subspace_topology CXY Tcc H)) Hpack).
Let a be given.
Assume HaX: a ∈ X.
We will prove compact_space (closure_of Y Ty (Ascoli_F_at X Y a F)) (subspace_topology Y Ty (closure_of Y Ty (Ascoli_F_at X Y a F))).
Set AF to be the term Ascoli_F_at X Y a F.
Set AH to be the term Ascoli_F_at X Y a H.
Set clF to be the term closure_of Y Ty AF.
Set clH to be the term closure_of Y Ty AH.
We prove the intermediate claim HAFsubAH: AF ⊆ AH.
Let y be given.
Assume Hy: y ∈ AF.
Apply (ReplE_impred F (λf0 : set ⇒ apply_fun f0 a) y Hy (y ∈ AH)) to the current goal.
Let f0 be given.
Assume Hf0F: f0 ∈ F.
Assume Hyeq: y = apply_fun f0 a.
rewrite the current goal using Hyeq (from left to right).
We prove the intermediate claim Hf0H: f0 ∈ H.
An exact proof term for the current goal is (HFsubH f0 Hf0F).
An exact proof term for the current goal is (ReplI H (λf1 : set ⇒ apply_fun f1 a) f0 Hf0H).
We prove the intermediate claim HAHsubY: AH ⊆ Y.
Let y be given.
Assume Hy: y ∈ AH.
Apply (ReplE_impred H (λf0 : set ⇒ apply_fun f0 a) y Hy (y ∈ Y)) to the current goal.
Let f0 be given.
Assume Hf0H: f0 ∈ H.
Assume Hyeq: y = apply_fun f0 a.
rewrite the current goal using Hyeq (from left to right).
We prove the intermediate claim Hf0C: f0 ∈ CXY.
An exact proof term for the current goal is (HHsubCXY f0 Hf0H).
We prove the intermediate claim Hf0Dom: f0 ∈ function_space X Y.
An exact proof term for the current goal is (HCXYsubDom f0 Hf0C).
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 Hf0Dom).
An exact proof term for the current goal is (Hf0fun a HaX).
We prove the intermediate claim HclFsubclH: clF ⊆ clH.
An exact proof term for the current goal is (closure_monotone Y Ty AF AH HTy HAFsubAH HAHsubY).
Set eval to be the term graph (function_space X Y) (λf0 : set ⇒ apply_fun f0 a).
We prove the intermediate claim HtopDom: topology_on (function_space X Y) (compact_convergence_topology X Tx Y Ty).
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 HevalContDom: continuous_map (function_space X Y) (compact_convergence_topology X Tx Y Ty) Y Ty eval.
An exact proof term for the current goal is (compact_convergence_eval_continuous X Tx Y Ty a HTx HTy HaX).
We prove the intermediate claim HevalContCXY: continuous_map CXY Tco Y Ty eval.
An exact proof term for the current goal is (continuous_on_subspace_rule (function_space X Y) (compact_convergence_topology X Tx Y Ty) Y Ty eval CXY HtopDom HTy HCXYsubDom HevalContDom).
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 HevalContH: continuous_map H (subspace_topology CXY Tco H) Y Ty eval.
An exact proof term for the current goal is (continuous_on_subspace_rule CXY Tco Y Ty eval H HTco HTy HHsubCXY HevalContCXY).
We prove the intermediate claim HeqTop: compact_open_topology_C X Tx Y Ty = compact_convergence_topology_metric_C X Tx Y dY.
An exact proof term for the current goal is (compact_open_eq_compact_convergence_on_C X Tx Y dY HTx HdY).
We prove the intermediate claim HeqTop': Tcc = Tco.
rewrite the current goal using HeqTop (from right to left).
Use reflexivity.
We prove the intermediate claim HsubEq: subspace_topology CXY Tcc H = subspace_topology CXY Tco H.
An exact proof term for the current goal is (subspace_topology_eq_of_eq CXY Tcc Tco H HeqTop').
We prove the intermediate claim HcompH: compact_space H (subspace_topology CXY Tco H).
rewrite the current goal using HsubEq (from right to left).
An exact proof term for the current goal is HcompHcc.
We prove the intermediate claim HimgComp: compact_space (image_of_fun eval H) (subspace_topology Y Ty (image_of_fun eval H)).
An exact proof term for the current goal is (continuous_image_compact H (subspace_topology CXY Tco H) Y Ty eval HcompH HevalContH).
We prove the intermediate claim HimgEq: image_of_fun eval H = AH.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ image_of_fun eval H.
We will prove y ∈ AH.
Apply (ReplE_impred H (λu : set ⇒ apply_fun eval u) y Hy (y ∈ AH)) to the current goal.
Let f0 be given.
Assume Hf0H: f0 ∈ H.
Assume Hyeq: y = apply_fun eval f0.
rewrite the current goal using Hyeq (from left to right).
rewrite the current goal using (apply_fun_graph (function_space X Y) (λg : set ⇒ apply_fun g a) f0 (HCXYsubDom f0 (HHsubCXY f0 Hf0H))) (from left to right).
An exact proof term for the current goal is (ReplI H (λf1 : set ⇒ apply_fun f1 a) f0 Hf0H).
Let y be given.
Assume Hy: y ∈ AH.
We will prove y ∈ image_of_fun eval H.
Apply (ReplE_impred H (λf0 : set ⇒ apply_fun f0 a) y Hy (y ∈ image_of_fun eval H)) to the current goal.
Let f0 be given.
Assume Hf0H: f0 ∈ H.
Assume Hyeq: y = apply_fun f0 a.
rewrite the current goal using Hyeq (from left to right).
rewrite the current goal using (apply_fun_graph (function_space X Y) (λg : set ⇒ apply_fun g a) f0 (HCXYsubDom f0 (HHsubCXY f0 Hf0H))) (from right to left).
An exact proof term for the current goal is (ReplI H (λu : set ⇒ apply_fun eval u) f0 Hf0H).
We prove the intermediate claim HAHcomp: compact_space AH (subspace_topology Y Ty AH).
rewrite the current goal using HimgEq (from right to left).
An exact proof term for the current goal is HimgComp.
We prove the intermediate claim HAHclosed: closed_in Y Ty AH.
We prove the intermediate claim HAHsubY': AH ⊆ Y.
An exact proof term for the current goal is HAHsubY.
An exact proof term for the current goal is (compact_subspace_in_Hausdorff_closed Y Ty AH HHY HAHsubY' HAHcomp).
We prove the intermediate claim HclHeq: clH = AH.
An exact proof term for the current goal is (closed_closure_eq Y Ty AH HTy HAHclosed).
We prove the intermediate claim HclFsubAH: clF ⊆ AH.
rewrite the current goal using HclHeq (from right to left) at position 1.
An exact proof term for the current goal is HclFsubclH.
We prove the intermediate claim HAFsubY: AF ⊆ Y.
Let y be given.
Assume Hy: y ∈ AF.
Apply (ReplE_impred F (λf0 : set ⇒ apply_fun f0 a) y Hy (y ∈ Y)) to the current goal.
Let f0 be given.
Assume Hf0F: f0 ∈ F.
Assume Hyeq: y = apply_fun f0 a.
rewrite the current goal using Hyeq (from left to right).
We prove the intermediate claim Hf0C: f0 ∈ CXY.
An exact proof term for the current goal is (HFsubCXY f0 Hf0F).
We prove the intermediate claim Hf0Dom: f0 ∈ function_space X Y.
An exact proof term for the current goal is (HCXYsubDom f0 Hf0C).
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 Hf0Dom).
An exact proof term for the current goal is (Hf0fun a HaX).
We prove the intermediate claim HclFclosed: closed_in Y Ty clF.
An exact proof term for the current goal is (closure_is_closed Y Ty AF HTy HAFsubY).
We prove the intermediate claim HclFclosed_in_AH: closed_in AH (subspace_topology Y Ty AH) clF.
We prove the intermediate claim HTAH: topology_on AH (subspace_topology Y Ty AH).
An exact proof term for the current goal is (subspace_topology_is_topology Y Ty AH HTy HAHsubY).
Apply (iffER (closed_in AH (subspace_topology Y Ty AH) clF) (∃C : set, closed_in Y Ty C ∧ clF = C ∩ AH) (closed_in_subspace_iff_intersection Y Ty AH clF HTy HAHsubY)) to the current goal.
We use clF to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HclFclosed.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ clF.
We will prove z ∈ clF ∩ AH.
Apply binintersectI to the current goal.
An exact proof term for the current goal is Hz.
An exact proof term for the current goal is (HclFsubAH z Hz).
Let z be given.
Assume Hz: z ∈ clF ∩ AH.
An exact proof term for the current goal is (binintersectE1 clF AH z Hz).
We prove the intermediate claim HclFcomp_in_AH: compact_space clF (subspace_topology AH (subspace_topology Y Ty AH) clF).
An exact proof term for the current goal is (closed_subspace_compact AH (subspace_topology Y Ty AH) clF HAHcomp HclFclosed_in_AH).
We prove the intermediate claim HclFTopEq: subspace_topology AH (subspace_topology Y Ty AH) clF = subspace_topology Y Ty clF.
An exact proof term for the current goal is (ex16_1_subspace_transitive Y Ty AH clF HTy HAHsubY HclFsubAH).
rewrite the current goal using HclFTopEq (from right to left).
An exact proof term for the current goal is HclFcomp_in_AH.
∎