Let X, Tx, Y, Ty, f and g be given.
Assume Hf: continuous_map X Tx Y Ty f.
Assume Hgfun: function_on g X Y.
Assume Heq: ∀x : set, x ∈ X → apply_fun f x = apply_fun g x.
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 Hf).
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 Hf).
We will prove continuous_map X Tx Y Ty g.
We will prove topology_on X Tx ∧ topology_on Y Ty ∧ function_on g X Y ∧ ∀V : set, V ∈ Ty → preimage_of X g 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 Hgfun.
Let V be given.
Assume HV: V ∈ Ty.
We prove the intermediate claim HpreF: preimage_of X f V ∈ Tx.
An exact proof term for the current goal is (continuous_map_preimage X Tx Y Ty f Hf V HV).
We prove the intermediate claim HeqPre: preimage_of X g V = preimage_of X f V.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X g V.
We will prove x ∈ preimage_of X f V.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun g u ∈ V) x Hx).
We prove the intermediate claim HgxV: apply_fun g x ∈ V.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun g u ∈ V) x Hx).
We prove the intermediate claim Hfx: apply_fun f x = apply_fun g x.
An exact proof term for the current goal is (Heq x HxX).
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
rewrite the current goal using Hfx (from left to right).
An exact proof term for the current goal is HgxV.
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ V) x HxX HfxV).
Let x be given.
Assume Hx: x ∈ preimage_of X f V.
We will prove x ∈ preimage_of X g V.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λu : set ⇒ apply_fun f u ∈ V) x Hx).
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ V) x Hx).
We prove the intermediate claim Hfx: apply_fun f x = apply_fun g x.
An exact proof term for the current goal is (Heq x HxX).
We prove the intermediate claim HgxV: apply_fun g x ∈ V.
rewrite the current goal using Hfx (from right to left).
An exact proof term for the current goal is HfxV.
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun g u ∈ V) x HxX HgxV).
rewrite the current goal using HeqPre (from left to right).
An exact proof term for the current goal is HpreF.
∎