Let X, Tx, Y, Ty and f be given.
Assume Hcont: continuous_map X Tx Y Ty f.
We prove the intermediate claim Hpreimg: ∀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) Hcont).
We prove the intermediate claim Hleft: (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) Hcont).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (topology_on Y Ty) (andEL (topology_on X Tx ∧ topology_on Y Ty) (function_on f X Y) Hleft)).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (andER (topology_on X Tx) (topology_on Y Ty) (andEL (topology_on X Tx ∧ topology_on Y Ty) (function_on f X Y) Hleft)).
We prove the intermediate claim Hf: 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) Hleft).
Let C be given.
Assume HC: closed_in Y Ty C.
We prove the intermediate claim Hright: C ⊆ Y ∧ ∃U ∈ Ty, C = Y ∖ U.
An exact proof term for the current goal is (andER (topology_on Y Ty) (C ⊆ Y ∧ ∃U ∈ Ty, C = Y ∖ U) HC).
We prove the intermediate claim HCsub: C ⊆ Y.
An exact proof term for the current goal is (andEL (C ⊆ Y) (∃U ∈ Ty, C = Y ∖ U) Hright).
We prove the intermediate claim HU: ∃U ∈ Ty, C = Y ∖ U.
An exact proof term for the current goal is (andER (C ⊆ Y) (∃U ∈ Ty, C = Y ∖ U) Hright).
Apply HU to the current goal.
Let U be given.
Assume HU.
Apply HU to the current goal.
Assume HUTy: U ∈ Ty.
Assume HCeq: C = Y ∖ U.
We will prove closed_in X Tx (preimage_of X f C).
We will prove topology_on X Tx ∧ (preimage_of X f C ⊆ X ∧ ∃V ∈ Tx, preimage_of X f C = X ∖ V).
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
We will prove preimage_of X f C ⊆ X ∧ ∃V ∈ Tx, preimage_of X f C = X ∖ V.
Apply andI to the current goal.
We will prove preimage_of X f C ⊆ X.
Let x be given.
Assume Hx: x ∈ preimage_of X f C.
We will prove x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx ⇒ apply_fun f x ∈ C) x Hx).
We will prove ∃V ∈ Tx, preimage_of X f C = X ∖ V.
We use (preimage_of X f U) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (Hpreimg U HUTy).
We will prove preimage_of X f C = X ∖ preimage_of X f U.
rewrite the current goal using HCeq (from left to right).
We will prove preimage_of X f (Y ∖ U) = X ∖ preimage_of X f U.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X f (Y ∖ U).
We will prove x ∈ X ∖ preimage_of X f U.
Apply (SepE X (λx ⇒ apply_fun f x ∈ Y ∖ U) x Hx) to the current goal.
Assume HxX: x ∈ X.
Assume Hfx: apply_fun f x ∈ Y ∖ U.
Apply (setminusE Y U (apply_fun f x) Hfx) to the current goal.
Assume HfxY: apply_fun f x ∈ Y.
Assume HfxU: apply_fun f x ∉ U.
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
We will prove x ∉ preimage_of X f U.
Assume Hxpre: x ∈ preimage_of X f U.
Apply (SepE X (λx ⇒ apply_fun f x ∈ U) x Hxpre) to the current goal.
Assume _.
Assume HfxU2: apply_fun f x ∈ U.
An exact proof term for the current goal is (HfxU HfxU2).
Let x be given.
Assume Hx: x ∈ X ∖ preimage_of X f U.
We will prove x ∈ preimage_of X f (Y ∖ U).
Apply (setminusE X (preimage_of X f U) x Hx) to the current goal.
Assume HxX: x ∈ X.
Assume Hxpre: x ∉ preimage_of X f U.
We will prove x ∈ {x ∈ X|apply_fun f x ∈ Y ∖ U}.
Apply SepI to the current goal.
An exact proof term for the current goal is HxX.
We will prove apply_fun f x ∈ Y ∖ U.
Apply setminusI to the current goal.
An exact proof term for the current goal is (Hf x HxX).
We will prove apply_fun f x ∉ U.
Assume HfxU: apply_fun f x ∈ U.
We prove the intermediate claim Hxpre2: x ∈ preimage_of X f U.
An exact proof term for the current goal is (SepI X (λx ⇒ apply_fun f x ∈ U) x HxX HfxU).
An exact proof term for the current goal is (Hxpre Hxpre2).
∎