Let X, Tx, Y, Ty, f and A be given.
Assume HTx: topology_on X Tx.
Assume HA: A ⊆ X.
Assume Hf: continuous_map X Tx Y Ty f.
We will prove continuous_map A (subspace_topology X Tx A) Y Ty f.
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (andER (topology_on X Tx) (topology_on Y Ty) (andEL (topology_on X Tx ∧ topology_on Y Ty) (function_on f X Y) (andEL (topology_on X Tx ∧ topology_on Y Ty ∧ function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hf))).
We prove the intermediate claim Hfun: function_on f X Y.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ topology_on Y Ty) (function_on f X Y) (andEL (topology_on X Tx ∧ topology_on Y Ty ∧ function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hf)).
We prove the intermediate claim Hf_preimg: ∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ topology_on Y Ty ∧ function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hf).
We prove the intermediate claim HTsubspace: topology_on A (subspace_topology X Tx A).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx A HTx HA).
We prove the intermediate claim Hfun_A: function_on f A Y.
We will prove ∀x : set, x ∈ A → apply_fun f x ∈ Y.
Let x be given.
Assume HxA: x ∈ A.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HA x HxA).
An exact proof term for the current goal is (Hfun x HxX).
We prove the intermediate claim Hpreimg_subspace: ∀V : set, V ∈ Ty → preimage_of A f V ∈ subspace_topology X Tx A.
Let V be given.
Assume HV: V ∈ Ty.
We will prove preimage_of A f V ∈ subspace_topology X Tx A.
Set U to be the term preimage_of X f V.
We prove the intermediate claim HU_open: U ∈ Tx.
An exact proof term for the current goal is (Hf_preimg V HV).
We prove the intermediate claim Hpreimg_eq: preimage_of A f V = U ∩ A.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of A f V.
We will prove x ∈ U ∩ A.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (SepE1 A (λy ⇒ apply_fun f y ∈ V) x Hx).
We prove the intermediate claim Hfx_V: apply_fun f x ∈ V.
An exact proof term for the current goal is (SepE2 A (λy ⇒ apply_fun f y ∈ V) x Hx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HA x HxA).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (SepI X (λy ⇒ apply_fun f y ∈ V) x HxX Hfx_V).
An exact proof term for the current goal is (binintersectI U A x HxU HxA).
Let x be given.
Assume Hx: x ∈ U ∩ A.
We will prove x ∈ preimage_of A f V.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binintersectE1 U A x Hx).
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectE2 U A x Hx).
We prove the intermediate claim Hfx_V: apply_fun f x ∈ V.
An exact proof term for the current goal is (SepE2 X (λy ⇒ apply_fun f y ∈ V) x HxU).
An exact proof term for the current goal is (SepI A (λy ⇒ apply_fun f y ∈ V) x HxA Hfx_V).
We will prove preimage_of A f V ∈ {W ∈ 𝒫 A|∃Z ∈ Tx, W = Z ∩ A}.
We prove the intermediate claim HpAV_PowerA: preimage_of A f V ∈ 𝒫 A.
Apply PowerI to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of A f V.
An exact proof term for the current goal is (SepE1 A (λy ⇒ apply_fun f y ∈ V) x Hx).
We prove the intermediate claim Hexists: ∃Z ∈ Tx, preimage_of A f V = Z ∩ A.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HU_open.
An exact proof term for the current goal is Hpreimg_eq.
An exact proof term for the current goal is (SepI (𝒫 A) (λW ⇒ ∃Z ∈ Tx, W = Z ∩ A) (preimage_of A f V) HpAV_PowerA Hexists).
We prove the intermediate claim Hpart1: topology_on A (subspace_topology X Tx A) ∧ topology_on Y Ty.
Apply andI to the current goal.
An exact proof term for the current goal is HTsubspace.
An exact proof term for the current goal is HTy.
We prove the intermediate claim Hpart2: (topology_on A (subspace_topology X Tx A) ∧ topology_on Y Ty) ∧ function_on f A Y.
Apply andI to the current goal.
An exact proof term for the current goal is Hpart1.
An exact proof term for the current goal is Hfun_A.
We will prove (topology_on A (subspace_topology X Tx A) ∧ topology_on Y Ty ∧ function_on f A Y) ∧ (∀V : set, V ∈ Ty → preimage_of A f V ∈ subspace_topology X Tx A).
Apply andI to the current goal.
An exact proof term for the current goal is Hpart2.
An exact proof term for the current goal is Hpreimg_subspace.
∎