Let X, Tx, Y, Ty, f and A be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
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 HTA: 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 HpreX: ∀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 Htmp: (topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y.
An exact proof term for the current goal is (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 HfunXY: 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) Htmp).
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.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HTA.
An exact proof term for the current goal is HTy.
Let a be given.
Assume HaA: a ∈ A.
We will prove apply_fun f a ∈ Y.
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HA a HaA).
An exact proof term for the current goal is (HfunXY a HaX).
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 (HpreX V HV).
We prove the intermediate claim Heq: preimage_of A f V = U ∩ A.
Apply set_ext to the current goal.
Let a be given.
Assume Ha: a ∈ preimage_of A f V.
We will prove a ∈ U ∩ A.
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (SepE1 A (λu : set ⇒ apply_fun f u ∈ V) a Ha).
We prove the intermediate claim HaU: a ∈ U.
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HA a HaA).
We prove the intermediate claim HaV: apply_fun f a ∈ V.
An exact proof term for the current goal is (SepE2 A (λu : set ⇒ apply_fun f u ∈ V) a Ha).
An exact proof term for the current goal is (SepI X (λx : set ⇒ apply_fun f x ∈ V) a HaX HaV).
An exact proof term for the current goal is (binintersectI U A a HaU HaA).
Let a be given.
Assume Ha: a ∈ U ∩ A.
We will prove a ∈ preimage_of A f V.
We prove the intermediate claim HaU: a ∈ U.
An exact proof term for the current goal is (binintersectE1 U A a Ha).
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (binintersectE2 U A a Ha).
We prove the intermediate claim HaV: apply_fun f a ∈ V.
An exact proof term for the current goal is (SepE2 X (λx : set ⇒ apply_fun f x ∈ V) a HaU).
An exact proof term for the current goal is (SepI A (λu : set ⇒ apply_fun f u ∈ V) a HaA HaV).
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HWpow: (U ∩ A) ∈ 𝒫 A.
Apply PowerI to the current goal.
Let a be given.
Assume Ha: a ∈ U ∩ A.
An exact proof term for the current goal is (binintersectE2 U A a Ha).
We prove the intermediate claim HexW: ∃W ∈ Tx, U ∩ A = W ∩ 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.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 A) (λU0 : set ⇒ ∃W ∈ Tx, U0 = W ∩ A) (U ∩ A) HWpow HexW).
∎