Assume Hf: continuous_map X Tx Y Ty f.

We will prove function_on f X Y ∧ (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) ∧ (∀C : set, closed_in Y Ty C → closed_in X Tx (preimage_of X f C)) ∧ (∀x : set, x ∈ X → ∀V : set, V ∈ Ty → apply_fun f x ∈ V → ∃U : set, U ∈ Tx ∧ x ∈ U ∧ ∀u : set, u ∈ U → apply_fun f u ∈ V).

We prove the intermediate claim Hpreimage: ∀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 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)).

Apply andI to the current goal.

An exact proof term for the current goal is Hfun.

An exact proof term for the current goal is Hpreimage.

An exact proof term for the current goal is (continuous_preserves_closed X Tx Y Ty f Hf).

An exact proof term for the current goal is (continuous_local_neighborhood X Tx Y Ty f HTx HTy Hfun Hpreimage).

Assume Hconds.

We will prove continuous_map X Tx Y Ty f.

We prove the intermediate claim Habc: (function_on f X Y ∧ (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx)) ∧ (∀C : set, closed_in Y Ty C → closed_in X Tx (preimage_of X f C)).

An exact proof term for the current goal is (andEL (((function_on f X Y ∧ (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx)) ∧ (∀C : set, closed_in Y Ty C → closed_in X Tx (preimage_of X f C)))) (∀x : set, x ∈ X → ∀V : set, V ∈ Ty → apply_fun f x ∈ V → ∃U : set, U ∈ Tx ∧ x ∈ U ∧ ∀u : set, u ∈ U → apply_fun f u ∈ V) Hconds).

We prove the intermediate claim Hab: function_on f X Y ∧ (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx).

An exact proof term for the current goal is (andEL (function_on f X Y ∧ (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx)) (∀C : set, closed_in Y Ty C → closed_in X Tx (preimage_of X f C)) Habc).

We prove the intermediate claim Hfun: function_on f X Y.

An exact proof term for the current goal is (andEL (function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hab).

We prove the intermediate claim Hpreimage: ∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx.

An exact proof term for the current goal is (andER (function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hab).

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.

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.

An exact proof term for the current goal is Hpreimage.