Let X, Tx, Y, Ty, Ty' and f be given.
Assume Hcont: continuous_map X Tx Y Ty f.
Assume HTy': topology_on Y Ty'.
Assume Hsub: Ty' ⊆ Ty.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (continuous_map_topology_dom X Tx Y Ty f Hcont).
We prove the intermediate claim Hfun: function_on f X Y.
An exact proof term for the current goal is (continuous_map_function_on X Tx Y Ty f Hcont).
We will prove continuous_map X Tx Y Ty' f.
We will prove topology_on X Tx ∧ topology_on Y Ty' ∧ function_on f X Y ∧ ∀V : set, V ∈ Ty' → preimage_of X f V ∈ Tx.
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 HTx.
An exact proof term for the current goal is HTy'.
An exact proof term for the current goal is Hfun.
Let V be given.
Assume HV': V ∈ Ty'.
We prove the intermediate claim HV: V ∈ Ty.
An exact proof term for the current goal is (Hsub V HV').
An exact proof term for the current goal is (continuous_map_preimage X Tx Y Ty f Hcont V HV).
∎