Let X, Tx, Y, Ty and x be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
Assume HxX: x ∈ X.
Set eval to be the term graph (function_space X Y) (λf : set ⇒ apply_fun f x).
We will prove continuous_map (function_space X Y) (compact_convergence_topology X Tx Y Ty) Y Ty eval.
We will prove topology_on (function_space X Y) (compact_convergence_topology X Tx Y Ty) ∧ topology_on Y Ty ∧ function_on eval (function_space X Y) Y ∧ ∀V : set, V ∈ Ty → preimage_of (function_space X Y) eval V ∈ (compact_convergence_topology X Tx Y Ty).
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 (compact_convergence_topology_is_topology X Tx Y Ty HTx HTy).
An exact proof term for the current goal is HTy.
Let f be given.
Assume Hf: f ∈ function_space X Y.
We will prove apply_fun eval f ∈ Y.
rewrite the current goal using (apply_fun_graph (function_space X Y) (λg : set ⇒ apply_fun g x) f Hf) (from left to right).
We prove the intermediate claim Hfunf: function_on f X Y.
An exact proof term for the current goal is (function_on_of_function_space f X Y Hf).
An exact proof term for the current goal is (Hfunf x HxX).
Let V be given.
Assume HV: V ∈ Ty.
We will prove preimage_of (function_space X Y) eval V ∈ (compact_convergence_topology X Tx Y Ty).
Set K to be the term {x}.
Set S0 to be the term {f ∈ function_space X Y|K ⊆ preimage_of X f V}.
We prove the intermediate claim HKsub: K ⊆ X.
Let t be given.
Assume Ht: t ∈ K.
We prove the intermediate claim Hteq: t = x.
An exact proof term for the current goal is (SingE x t Ht).
rewrite the current goal using Hteq (from left to right).
An exact proof term for the current goal is HxX.
We prove the intermediate claim HTK: topology_on K (subspace_topology X Tx K).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx K HTx HKsub).
We prove the intermediate claim HKcomp: compact_space K (subspace_topology X Tx K).
We prove the intermediate claim HKdef: K = {x}.
Use reflexivity.
An exact proof term for the current goal is (compact_space_singleton K (subspace_topology X Tx K) x HKdef HTK).
We prove the intermediate claim HS0inSub: S0 ∈ compact_open_subbasis X Tx Y Ty.
We prove the intermediate claim HS0sub: S0 ⊆ function_space X Y.
Let f be given.
Assume HfS0: f ∈ S0.
An exact proof term for the current goal is (SepE1 (function_space X Y) (λf0 : set ⇒ K ⊆ preimage_of X f0 V) f HfS0).
We prove the intermediate claim HS0pow: S0 ∈ 𝒫 (function_space X Y).
An exact proof term for the current goal is (PowerI (function_space X Y) S0 HS0sub).
We prove the intermediate claim HS0prop: ∃K0 U : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U ∈ Ty ∧ S0 = {f0 ∈ function_space X Y|K0 ⊆ preimage_of X f0 U}.
We use K to witness the existential quantifier.
We use V to witness the existential quantifier.
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 HKcomp.
An exact proof term for the current goal is HKsub.
An exact proof term for the current goal is HV.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 (function_space X Y)) (λS : set ⇒ ∃K0 U : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U ∈ Ty ∧ S = {f0 ∈ function_space X Y|K0 ⊆ preimage_of X f0 U}) S0 HS0pow HS0prop).
We prove the intermediate claim HpreEq: preimage_of (function_space X Y) eval V = S0.
Apply set_ext to the current goal.
Let f be given.
Assume Hfpre: f ∈ preimage_of (function_space X Y) eval V.
We will prove f ∈ S0.
We prove the intermediate claim HfDom: f ∈ function_space X Y.
An exact proof term for the current goal is (SepE1 (function_space X Y) (λu : set ⇒ apply_fun eval u ∈ V) f Hfpre).
We prove the intermediate claim HevalV: apply_fun eval f ∈ V.
An exact proof term for the current goal is (SepE2 (function_space X Y) (λu : set ⇒ apply_fun eval u ∈ V) f Hfpre).
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
rewrite the current goal using (apply_fun_graph (function_space X Y) (λg : set ⇒ apply_fun g x) f HfDom) (from right to left).
An exact proof term for the current goal is HevalV.
We prove the intermediate claim HKpre: K ⊆ preimage_of X f V.
Let t be given.
Assume HtK: t ∈ K.
We will prove t ∈ preimage_of X f V.
We prove the intermediate claim Hteq: t = x.
An exact proof term for the current goal is (SingE x t HtK).
rewrite the current goal using Hteq (from left to right).
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ V) x HxX HfxV).
An exact proof term for the current goal is (SepI (function_space X Y) (λf0 : set ⇒ K ⊆ preimage_of X f0 V) f HfDom HKpre).
Let f be given.
Assume HfS0: f ∈ S0.
We will prove f ∈ preimage_of (function_space X Y) eval V.
We prove the intermediate claim HfDom: f ∈ function_space X Y.
An exact proof term for the current goal is (SepE1 (function_space X Y) (λf0 : set ⇒ K ⊆ preimage_of X f0 V) f HfS0).
We prove the intermediate claim HKpre: K ⊆ preimage_of X f V.
An exact proof term for the current goal is (SepE2 (function_space X Y) (λf0 : set ⇒ K ⊆ preimage_of X f0 V) f HfS0).
We prove the intermediate claim HxK: x ∈ K.
An exact proof term for the current goal is (SingI x).
We prove the intermediate claim Hxpre: x ∈ preimage_of X f V.
An exact proof term for the current goal is (HKpre x HxK).
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ V) x Hxpre).
We prove the intermediate claim HevalV: apply_fun eval f ∈ V.
rewrite the current goal using (apply_fun_graph (function_space X Y) (λg : set ⇒ apply_fun g x) f HfDom) (from left to right).
An exact proof term for the current goal is HfxV.
An exact proof term for the current goal is (SepI (function_space X Y) (λu : set ⇒ apply_fun eval u ∈ V) f HfDom HevalV).
rewrite the current goal using HpreEq (from left to right).
We prove the intermediate claim HSsub: subbasis_on (function_space X Y) (compact_open_subbasis X Tx Y Ty).
An exact proof term for the current goal is (compact_open_subbasis_is_subbasis X Tx Y Ty HTx HTy).
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis (function_space X Y) (compact_open_subbasis X Tx Y Ty) S0 HSsub HS0inSub).
∎