Let X, Tx and A be given.
Assume HTx: topology_on X Tx.
Assume HA: A ⊆ X.
Set j to be the term {(y,y)|y ∈ A}.
We will prove continuous_map A (subspace_topology X Tx A) X Tx j.
We will prove topology_on A (subspace_topology X Tx A) ∧ topology_on X Tx ∧ function_on j A X ∧ ∀V : set, V ∈ Tx → preimage_of A j 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 (subspace_topology_is_topology X Tx A HTx HA).
An exact proof term for the current goal is HTx.
Let a be given.
Assume HaA: a ∈ A.
We will prove apply_fun j a ∈ X.
We prove the intermediate claim Haj: apply_fun j a = a.
An exact proof term for the current goal is (identity_function_apply A a HaA).
rewrite the current goal using Haj (from left to right).
An exact proof term for the current goal is (HA a HaA).
Let V be given.
Assume HV: V ∈ Tx.
We will prove preimage_of A j V ∈ subspace_topology X Tx A.
We prove the intermediate claim Heq: preimage_of A j V = V ∩ A.
Apply set_ext to the current goal.
Let a be given.
Assume Ha: a ∈ preimage_of A j V.
We will prove a ∈ V ∩ A.
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (SepE1 A (λu : set ⇒ apply_fun j u ∈ V) a Ha).
We prove the intermediate claim Haj: apply_fun j a = a.
An exact proof term for the current goal is (identity_function_apply A a HaA).
We prove the intermediate claim HaV: a ∈ V.
rewrite the current goal using Haj (from right to left).
An exact proof term for the current goal is (SepE2 A (λu : set ⇒ apply_fun j u ∈ V) a Ha).
An exact proof term for the current goal is (binintersectI V A a HaV HaA).
Let a be given.
Assume Ha: a ∈ V ∩ A.
We will prove a ∈ preimage_of A j V.
We prove the intermediate claim HaV: a ∈ V.
An exact proof term for the current goal is (binintersectE1 V A a Ha).
We prove the intermediate claim HaA: a ∈ A.
An exact proof term for the current goal is (binintersectE2 V A a Ha).
We will prove a ∈ {u ∈ A|apply_fun j u ∈ V}.
Apply (SepI A (λu : set ⇒ apply_fun j u ∈ V) a HaA) to the current goal.
We prove the intermediate claim Haj: apply_fun j a = a.
An exact proof term for the current goal is (identity_function_apply A a HaA).
rewrite the current goal using Haj (from left to right).
An exact proof term for the current goal is HaV.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (subspace_topologyI X Tx A V HV).
∎