Let X, Tx, Y, Ty, Z0, Tz0 and f be given.
Assume Hf: continuous_map X Tx Y Ty f.
Assume HYZ0: Y ⊆ Z0.
Assume HTz0: topology_on Z0 Tz0.
Assume HTy_eq: Ty = subspace_topology Z0 Tz0 Y.
We will prove continuous_map X Tx Z0 Tz0 f.
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 HpreY: ∀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 Htmp: (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) Hf).
We prove the intermediate claim HfunXY: 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) Htmp).
We prove the intermediate claim HfunXZ0: function_on f X Z0.
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (HYZ0 (apply_fun f x) (HfunXY x HxX)).
We will prove (topology_on X Tx ∧ topology_on Z0 Tz0 ∧ function_on f X Z0) ∧ ∀W : set, W ∈ Tz0 → preimage_of X f W ∈ 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 HTz0.
An exact proof term for the current goal is HfunXZ0.
Let W be given.
Assume HW: W ∈ Tz0.
Set B to be the term W ∩ Y.
We prove the intermediate claim HB_inTy: B ∈ Ty.
rewrite the current goal using HTy_eq (from left to right).
We prove the intermediate claim HBpow: B ∈ 𝒫 Y.
Apply PowerI to the current goal.
Let y be given.
Assume HyB: y ∈ B.
An exact proof term for the current goal is (binintersectE2 W Y y HyB).
We prove the intermediate claim Hex: ∃Z ∈ Tz0, B = Z ∩ Y.
We use W to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HW.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ ∃V ∈ Tz0, U0 = V ∩ Y) B HBpow Hex).
We prove the intermediate claim HpreEq: preimage_of X f W = preimage_of X f B.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X f W.
We will prove x ∈ preimage_of X f B.
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 ∈ W) x Hx).
We prove the intermediate claim HfxW: apply_fun f x ∈ W.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ W) x Hx).
We prove the intermediate claim HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (HfunXY x HxX).
We prove the intermediate claim HfxB: apply_fun f x ∈ B.
An exact proof term for the current goal is (binintersectI W Y (apply_fun f x) HfxW HfxY).
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ B) x HxX HfxB).
Let x be given.
Assume Hx: x ∈ preimage_of X f B.
We will prove x ∈ preimage_of X f W.
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 ∈ B) x Hx).
We prove the intermediate claim HfxB: apply_fun f x ∈ B.
An exact proof term for the current goal is (SepE2 X (λu : set ⇒ apply_fun f u ∈ B) x Hx).
We prove the intermediate claim HfxW: apply_fun f x ∈ W.
An exact proof term for the current goal is (binintersectE1 W Y (apply_fun f x) HfxB).
An exact proof term for the current goal is (SepI X (λu : set ⇒ apply_fun f u ∈ W) x HxX HfxW).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is (HpreY B HB_inTy).
∎