Let X, Tx, Y, Ty, f and C be given.
Assume Hcont: continuous_map X Tx Y Ty f.
Assume HCcl: closed_in Y Ty C.
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 HTy: topology_on Y Ty.
An exact proof term for the current goal is (continuous_map_topology_cod X Tx Y Ty f Hcont).
We prove the intermediate claim HfunXY: 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 prove the intermediate claim Hex: ∃U : set, U ∈ Ty ∧ C = Y ∖ U.
An exact proof term for the current goal is (closed_in_exists_open_complement Y Ty C HCcl).
Apply Hex to the current goal.
Let U be given.
Assume HUpair.
We prove the intermediate claim HUopen: U ∈ Ty.
An exact proof term for the current goal is (andEL (U ∈ Ty) (C = Y ∖ U) HUpair).
We prove the intermediate claim HCe: C = Y ∖ U.
An exact proof term for the current goal is (andER (U ∈ Ty) (C = Y ∖ U) HUpair).
We prove the intermediate claim HpreUopen: preimage_of X f U ∈ Tx.
An exact proof term for the current goal is (continuous_map_preimage X Tx Y Ty f Hcont U HUopen).
We prove the intermediate claim HpreEq: preimage_of X f C = X ∖ preimage_of X f U.
rewrite the current goal using HCe (from left to right).
An exact proof term for the current goal is (preimage_of_complement X Y f U HfunXY).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is (closed_of_open_complement X Tx (preimage_of X f U) HTx HpreUopen).
∎