Let X, Tx, Y and Ty be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
We will prove subbasis_on (function_space X Y) (compact_open_subbasis X Tx Y Ty).
We will prove compact_open_subbasis X Tx Y Ty ⊆ 𝒫 (function_space X Y) ∧ ⋃ (compact_open_subbasis X Tx Y Ty) = function_space X Y.
Apply andI to the current goal.
Let S be given.
Assume HS: S ∈ compact_open_subbasis X Tx Y Ty.
We will prove S ∈ 𝒫 (function_space X Y).
An exact proof term for the current goal is (SepE1 (𝒫 (function_space X Y)) (λS0 : set ⇒ ∃K U : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U ∈ Ty ∧ S0 = {f ∈ function_space X Y|K ⊆ preimage_of X f U}) S HS).
Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ ⋃ (compact_open_subbasis X Tx Y Ty).
We will prove f ∈ function_space X Y.
Apply (UnionE_impred (compact_open_subbasis X Tx Y Ty) f Hf) to the current goal.
Let S be given.
Assume HfS: f ∈ S.
Assume HS: S ∈ compact_open_subbasis X Tx Y Ty.
We prove the intermediate claim HSpow: S ∈ 𝒫 (function_space X Y).
An exact proof term for the current goal is ((SepE1 (𝒫 (function_space X Y)) (λS0 : set ⇒ ∃K U : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U ∈ Ty ∧ S0 = {f0 ∈ function_space X Y|K ⊆ preimage_of X f0 U}) S HS)).
An exact proof term for the current goal is (PowerE (function_space X Y) S HSpow f HfS).
Let f be given.
Assume Hf: f ∈ function_space X Y.
We will prove f ∈ ⋃ (compact_open_subbasis X Tx Y Ty).
Set S0 to be the term {g ∈ function_space X Y|Empty ⊆ preimage_of X g Empty}.
We prove the intermediate claim HS0eq: S0 = function_space X Y.
Apply set_ext to the current goal.
Let g be given.
Assume Hg: g ∈ S0.
An exact proof term for the current goal is (SepE1 (function_space X Y) (λg0 : set ⇒ Empty ⊆ preimage_of X g0 Empty) g Hg).
Let g be given.
Assume Hg: g ∈ function_space X Y.
We will prove g ∈ S0.
An exact proof term for the current goal is (SepI (function_space X Y) (λg0 : set ⇒ Empty ⊆ preimage_of X g0 Empty) g Hg (Subq_Empty (preimage_of X g Empty))).
We prove the intermediate claim HEmptyComp: compact_space Empty (subspace_topology X Tx Empty).
An exact proof term for the current goal is (compact_empty_subspace X Tx HTx).
We prove the intermediate claim HEmptyOpen: Empty ∈ Ty.
An exact proof term for the current goal is (topology_has_empty Y Ty HTy).
We prove the intermediate claim HS0in: S0 ∈ compact_open_subbasis X Tx Y Ty.
We prove the intermediate claim HS0pow: S0 ∈ 𝒫 (function_space X Y).
rewrite the current goal using HS0eq (from left to right).
An exact proof term for the current goal is (PowerI (function_space X Y) (function_space X Y) (Subq_ref (function_space X Y))).
We prove the intermediate claim HS0prop: ∃K U : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U ∈ Ty ∧ S0 = {f0 ∈ function_space X Y|K ⊆ preimage_of X f0 U}.
We use Empty to witness the existential quantifier.
We use Empty 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 HEmptyComp.
An exact proof term for the current goal is (Subq_Empty X).
An exact proof term for the current goal is HEmptyOpen.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 (function_space X Y)) (λS : set ⇒ ∃K U : set, compact_space K (subspace_topology X Tx K) ∧ K ⊆ X ∧ U ∈ Ty ∧ S = {f0 ∈ function_space X Y|K ⊆ preimage_of X f0 U}) S0 HS0pow HS0prop).
We prove the intermediate claim HfS0: f ∈ S0.
rewrite the current goal using HS0eq (from left to right) at position 1.
An exact proof term for the current goal is Hf.
An exact proof term for the current goal is (UnionI (compact_open_subbasis X Tx Y Ty) f S0 HfS0 HS0in).
∎