Let X, A, B, Y, Tx, Ty, f and g be given.
Assume HTx: topology_on X Tx.
Assume HclA: closed_in X Tx A.
Assume HclB: closed_in X Tx B.
Assume HABeq: A ∪ B = X.
Assume Hf: continuous_map A (subspace_topology X Tx A) Y Ty f.
Assume Hg: continuous_map B (subspace_topology X Tx B) Y Ty g.
Assume Hagree: ∀x : set, x ∈ (A ∩ B) → apply_fun f x = apply_fun g x.
Set h to be the term graph X (λx0 : set ⇒ if x0 ∈ A then apply_fun f x0 else apply_fun g x0).
We use h to witness the existential quantifier.
We will prove continuous_map X Tx Y Ty h ∧ ((∀x : set, x ∈ A → apply_fun h x = apply_fun f x) ∧ (∀x : set, x ∈ B → apply_fun h x = apply_fun g x)).
Apply andI to the current goal.
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (continuous_map_topology_cod A (subspace_topology X Tx A) Y Ty f Hf).
We prove the intermediate claim Hfunf: function_on f A Y.
An exact proof term for the current goal is (continuous_map_function_on A (subspace_topology X Tx A) Y Ty f Hf).
We prove the intermediate claim Hfung: function_on g B Y.
An exact proof term for the current goal is (continuous_map_function_on B (subspace_topology X Tx B) Y Ty g Hg).
We will prove continuous_map X Tx Y Ty h.
We will prove topology_on X Tx ∧ topology_on Y Ty ∧ function_on h X Y ∧ ∀V : set, V ∈ Ty → preimage_of X h 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.
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun h x ∈ Y.
We prove the intermediate claim Happ: apply_fun h x = if x ∈ A then apply_fun f x else apply_fun g x.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ if x0 ∈ A then apply_fun f x0 else apply_fun g x0) x HxX) (from left to right).
Use reflexivity.
rewrite the current goal using Happ (from left to right).
Apply (xm (x ∈ A)) to the current goal.
Assume HxA: x ∈ A.
rewrite the current goal using (If_i_1 (x ∈ A) (apply_fun f x) (apply_fun g x) HxA) (from left to right).
An exact proof term for the current goal is (Hfunf x HxA).
Assume HxNotA: x ∉ A.
We prove the intermediate claim HxAB: x ∈ A ∪ B.
rewrite the current goal using HABeq (from left to right).
An exact proof term for the current goal is HxX.
Apply (binunionE A B x HxAB) to the current goal.
Assume HxA: x ∈ A.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxNotA HxA).
Assume HxB: x ∈ B.
rewrite the current goal using (If_i_0 (x ∈ A) (apply_fun f x) (apply_fun g x) HxNotA) (from left to right).
An exact proof term for the current goal is (Hfung x HxB).
Let V be given.
Assume HV: V ∈ Ty.
We prove the intermediate claim HpreA: preimage_of A f V ∈ subspace_topology X Tx A.
An exact proof term for the current goal is (continuous_map_preimage A (subspace_topology X Tx A) Y Ty f Hf V HV).
We prove the intermediate claim HpreB: preimage_of B g V ∈ subspace_topology X Tx B.
An exact proof term for the current goal is (continuous_map_preimage B (subspace_topology X Tx B) Y Ty g Hg V HV).
We prove the intermediate claim HexU0: ∃U0 ∈ Tx, preimage_of A f V = U0 ∩ A.
An exact proof term for the current goal is (SepE2 (𝒫 A) (λU : set ⇒ ∃U0 ∈ Tx, U = U0 ∩ A) (preimage_of A f V) HpreA).
Apply HexU0 to the current goal.
Let U0 be given.
Assume HU0pair.
We prove the intermediate claim HU0: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (preimage_of A f V = U0 ∩ A) HU0pair).
We prove the intermediate claim HpreAeq: preimage_of A f V = U0 ∩ A.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (preimage_of A f V = U0 ∩ A) HU0pair).
We prove the intermediate claim HexW0: ∃W0 ∈ Tx, preimage_of B g V = W0 ∩ B.
An exact proof term for the current goal is (SepE2 (𝒫 B) (λU : set ⇒ ∃W0 ∈ Tx, U = W0 ∩ B) (preimage_of B g V) HpreB).
Apply HexW0 to the current goal.
Let W0 be given.
Assume HW0pair.
We prove the intermediate claim HW0: W0 ∈ Tx.
An exact proof term for the current goal is (andEL (W0 ∈ Tx) (preimage_of B g V = W0 ∩ B) HW0pair).
We prove the intermediate claim HpreBeq: preimage_of B g V = W0 ∩ B.
An exact proof term for the current goal is (andER (W0 ∈ Tx) (preimage_of B g V = W0 ∩ B) HW0pair).
We prove the intermediate claim HcompAin: open_in X Tx (X ∖ A).
An exact proof term for the current goal is (open_of_closed_complement X Tx A HclA).
We prove the intermediate claim HcompA: (X ∖ A) ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx (X ∖ A) HcompAin).
We prove the intermediate claim HcompBin: open_in X Tx (X ∖ B).
An exact proof term for the current goal is (open_of_closed_complement X Tx B HclB).
We prove the intermediate claim HcompB: (X ∖ B) ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx (X ∖ B) HcompBin).
Set U to be the term U0 ∪ (X ∖ A).
Set W to be the term W0 ∪ (X ∖ B).
We prove the intermediate claim HUopen: U ∈ Tx.
An exact proof term for the current goal is (topology_binunion_closed X Tx U0 (X ∖ A) HTx HU0 HcompA).
We prove the intermediate claim HWopen: W ∈ Tx.
An exact proof term for the current goal is (topology_binunion_closed X Tx W0 (X ∖ B) HTx HW0 HcompB).
We prove the intermediate claim Heq: preimage_of X h V = U ∩ W.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ preimage_of X h V.
We will prove x ∈ U ∩ W.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun h x0 ∈ V) x Hx).
We prove the intermediate claim HhxV: apply_fun h x ∈ V.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun h x0 ∈ V) x Hx).
We prove the intermediate claim HxU: x ∈ U.
Apply (xm (x ∈ A)) to the current goal.
Assume HxA: x ∈ A.
We prove the intermediate claim Happ: apply_fun h x = apply_fun f x.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ if x0 ∈ A then apply_fun f x0 else apply_fun g x0) x HxX) (from left to right).
rewrite the current goal using (If_i_1 (x ∈ A) (apply_fun f x) (apply_fun g x) HxA) (from left to right).
Use reflexivity.
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is HhxV.
We prove the intermediate claim HxPreA: x ∈ preimage_of A f V.
An exact proof term for the current goal is (SepI A (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxA HfxV).
We prove the intermediate claim HxU0A: x ∈ U0 ∩ A.
rewrite the current goal using HpreAeq (from right to left).
An exact proof term for the current goal is HxPreA.
We prove the intermediate claim HxU0: x ∈ U0.
An exact proof term for the current goal is (binintersectE1 U0 A x HxU0A).
An exact proof term for the current goal is (binunionI1 U0 (X ∖ A) x HxU0).
Assume HxNotA: x ∉ A.
We prove the intermediate claim HxXA: x ∈ (X ∖ A).
An exact proof term for the current goal is (setminusI X A x HxX HxNotA).
An exact proof term for the current goal is (binunionI2 U0 (X ∖ A) x HxXA).
We prove the intermediate claim HxW: x ∈ W.
Apply (xm (x ∈ B)) to the current goal.
Assume HxB: x ∈ B.
We prove the intermediate claim HgV: apply_fun g x ∈ V.
Apply (xm (x ∈ A)) to the current goal.
Assume HxA: x ∈ A.
We prove the intermediate claim HxAB: x ∈ A ∩ B.
An exact proof term for the current goal is (binintersectI A B x HxA HxB).
We prove the intermediate claim Heqfg: apply_fun f x = apply_fun g x.
An exact proof term for the current goal is (Hagree x HxAB).
We prove the intermediate claim Happ: apply_fun h x = apply_fun f x.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ if x0 ∈ A then apply_fun f x0 else apply_fun g x0) x HxX) (from left to right).
rewrite the current goal using (If_i_1 (x ∈ A) (apply_fun f x) (apply_fun g x) HxA) (from left to right).
Use reflexivity.
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is HhxV.
rewrite the current goal using Heqfg (from right to left).
An exact proof term for the current goal is HfxV.
Assume HxNotA: x ∉ A.
We prove the intermediate claim Happ: apply_fun h x = apply_fun g x.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ if x0 ∈ A then apply_fun f x0 else apply_fun g x0) x HxX) (from left to right).
rewrite the current goal using (If_i_0 (x ∈ A) (apply_fun f x) (apply_fun g x) HxNotA) (from left to right).
Use reflexivity.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is HhxV.
We prove the intermediate claim HxPreB: x ∈ preimage_of B g V.
An exact proof term for the current goal is (SepI B (λx0 : set ⇒ apply_fun g x0 ∈ V) x HxB HgV).
We prove the intermediate claim HxW0B: x ∈ W0 ∩ B.
rewrite the current goal using HpreBeq (from right to left).
An exact proof term for the current goal is HxPreB.
We prove the intermediate claim HxW0: x ∈ W0.
An exact proof term for the current goal is (binintersectE1 W0 B x HxW0B).
An exact proof term for the current goal is (binunionI1 W0 (X ∖ B) x HxW0).
Assume HxNotB: x ∉ B.
We prove the intermediate claim HxXB: x ∈ (X ∖ B).
An exact proof term for the current goal is (setminusI X B x HxX HxNotB).
An exact proof term for the current goal is (binunionI2 W0 (X ∖ B) x HxXB).
An exact proof term for the current goal is (binintersectI U W x HxU HxW).
Let x be given.
Assume Hx: x ∈ U ∩ W.
We will prove x ∈ preimage_of X h V.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binintersectE1 U W x Hx).
We prove the intermediate claim HxW: x ∈ W.
An exact proof term for the current goal is (binintersectE2 U W x Hx).
Apply (xm (x ∈ A)) to the current goal.
Assume HxA: x ∈ A.
We prove the intermediate claim HxX: x ∈ X.
We prove the intermediate claim HA_sub: A ⊆ X.
rewrite the current goal using HABeq (from right to left).
An exact proof term for the current goal is (binunion_Subq_1 A B).
An exact proof term for the current goal is (HA_sub x HxA).
We prove the intermediate claim HxU0: x ∈ U0.
Apply (binunionE U0 (X ∖ A) x HxU) to the current goal.
Assume HxU0: x ∈ U0.
An exact proof term for the current goal is HxU0.
Assume HxXA: x ∈ (X ∖ A).
We prove the intermediate claim HnotA: x ∉ A.
An exact proof term for the current goal is (setminusE2 X A x HxXA).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnotA HxA).
We prove the intermediate claim HxPreA: x ∈ preimage_of A f V.
We prove the intermediate claim HxU0A: x ∈ U0 ∩ A.
An exact proof term for the current goal is (binintersectI U0 A x HxU0 HxA).
rewrite the current goal using HpreAeq (from left to right).
An exact proof term for the current goal is HxU0A.
We prove the intermediate claim HfxV: apply_fun f x ∈ V.
An exact proof term for the current goal is (SepE2 A (λx0 : set ⇒ apply_fun f x0 ∈ V) x HxPreA).
We prove the intermediate claim Happ: apply_fun h x = apply_fun f x.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ if x0 ∈ A then apply_fun f x0 else apply_fun g x0) x HxX) (from left to right).
rewrite the current goal using (If_i_1 (x ∈ A) (apply_fun f x) (apply_fun g x) HxA) (from left to right).
Use reflexivity.
We will prove x ∈ preimage_of X h V.
We prove the intermediate claim HhxV': apply_fun h x ∈ V.
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is HfxV.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun h x0 ∈ V) x HxX HhxV').
Assume HxNotA: x ∉ A.
We prove the intermediate claim HxX: x ∈ X.
Apply (binunionE U0 (X ∖ A) x HxU) to the current goal.
Assume HxU0: x ∈ U0.
We prove the intermediate claim HU0sub: U0 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U0 HTx HU0).
An exact proof term for the current goal is (HU0sub x HxU0).
Assume HxXA: x ∈ (X ∖ A).
An exact proof term for the current goal is (setminusE1 X A x HxXA).
We prove the intermediate claim HxAB: x ∈ A ∪ B.
rewrite the current goal using HABeq (from left to right).
An exact proof term for the current goal is HxX.
We prove the intermediate claim HxB: x ∈ B.
Apply (binunionE A B x HxAB) to the current goal.
Assume HxA: x ∈ A.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HxNotA HxA).
Assume HxB: x ∈ B.
An exact proof term for the current goal is HxB.
We prove the intermediate claim HxW0: x ∈ W0.
Apply (binunionE W0 (X ∖ B) x HxW) to the current goal.
Assume HxW0: x ∈ W0.
An exact proof term for the current goal is HxW0.
Assume HxXB: x ∈ (X ∖ B).
We prove the intermediate claim HnotB: x ∉ B.
An exact proof term for the current goal is (setminusE2 X B x HxXB).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnotB HxB).
We prove the intermediate claim HxPreB: x ∈ preimage_of B g V.
We prove the intermediate claim HxW0B: x ∈ W0 ∩ B.
An exact proof term for the current goal is (binintersectI W0 B x HxW0 HxB).
rewrite the current goal using HpreBeq (from left to right).
An exact proof term for the current goal is HxW0B.
We prove the intermediate claim HgV: apply_fun g x ∈ V.
An exact proof term for the current goal is (SepE2 B (λx0 : set ⇒ apply_fun g x0 ∈ V) x HxPreB).
We prove the intermediate claim Happ: apply_fun h x = apply_fun g x.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ if x0 ∈ A then apply_fun f x0 else apply_fun g x0) x HxX) (from left to right).
rewrite the current goal using (If_i_0 (x ∈ A) (apply_fun f x) (apply_fun g x) HxNotA) (from left to right).
Use reflexivity.
We will prove x ∈ preimage_of X h V.
We prove the intermediate claim HhxV': apply_fun h x ∈ V.
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is HgV.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun h x0 ∈ V) x HxX HhxV').
We will prove preimage_of X h V ∈ Tx.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (topology_binintersect_closed X Tx U W HTx HUopen HWopen).
Apply andI to the current goal.
Let x be given.
Assume HxA: x ∈ A.
We prove the intermediate claim HxAB: x ∈ A ∪ B.
An exact proof term for the current goal is (binunionI1 A B x HxA).
We prove the intermediate claim HxX: x ∈ X.
rewrite the current goal using HABeq (from right to left).
An exact proof term for the current goal is HxAB.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ if x0 ∈ A then apply_fun f x0 else apply_fun g x0) x HxX) (from left to right).
rewrite the current goal using (If_i_1 (x ∈ A) (apply_fun f x) (apply_fun g x) HxA) (from left to right).
Use reflexivity.
Let x be given.
Assume HxB: x ∈ B.
We prove the intermediate claim HxAB: x ∈ A ∪ B.
An exact proof term for the current goal is (binunionI2 A B x HxB).
We prove the intermediate claim HxX: x ∈ X.
rewrite the current goal using HABeq (from right to left).
An exact proof term for the current goal is HxAB.
Apply (xm (x ∈ A)) to the current goal.
Assume HxA: x ∈ A.
We prove the intermediate claim HxABi: x ∈ A ∩ B.
An exact proof term for the current goal is (binintersectI A B x HxA HxB).
We prove the intermediate claim Heqfg: apply_fun f x = apply_fun g x.
An exact proof term for the current goal is (Hagree x HxABi).
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ if x0 ∈ A then apply_fun f x0 else apply_fun g x0) x HxX) (from left to right).
rewrite the current goal using (If_i_1 (x ∈ A) (apply_fun f x) (apply_fun g x) HxA) (from left to right).
rewrite the current goal using Heqfg (from left to right).
Use reflexivity.
Assume HxNotA: x ∉ A.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ if x0 ∈ A then apply_fun f x0 else apply_fun g x0) x HxX) (from left to right).
rewrite the current goal using (If_i_0 (x ∈ A) (apply_fun f x) (apply_fun g x) HxNotA) (from left to right).
Use reflexivity.
∎