Let Xi, Ti, A, B, i and fi be given.
Assume Hchain: coherent_chain Xi Ti.
Assume Hnorms: ∀j : set, j ∈ ω → normal_space (apply_fun Xi j) (apply_fun Ti j).
Assume HiO: i ∈ ω.
Assume HAcl: closed_in (coherent_union Xi) (coherent_topology Xi Ti) A.
Assume HBcl: closed_in (coherent_union Xi) (coherent_topology Xi Ti) B.
Assume Hab: A ∩ B = Empty.
Assume Hfi: continuous_map (apply_fun Xi i) (apply_fun Ti i) (closed_interval 0 1) (closed_interval_topology 0 1) fi.
Assume HfiA0: ∀x : set, x ∈ (A ∩ apply_fun Xi i) → apply_fun fi x = 0.
Assume HfiB1: ∀x : set, x ∈ (B ∩ apply_fun Xi i) → apply_fun fi x = 1.
Set Xi_i to be the term apply_fun Xi i.
Set Ti_i to be the term apply_fun Ti i.
Set Xi_s to be the term apply_fun Xi (ordsucc i).
Set Ti_s to be the term apply_fun Ti (ordsucc i).
Set X to be the term coherent_union Xi.
Set Tx to be the term coherent_topology Xi Ti.
Set I01 to be the term closed_interval 0 1.
Set T01 to be the term closed_interval_topology 0 1.
We prove the intermediate claim Hab01: Rle 0 1.
An exact proof term for the current goal is (RleI 0 1 real_0 real_1 (not_Rlt_sym 0 1 Rlt_0_1)).
We prove the intermediate claim H0I01: 0 ∈ I01.
An exact proof term for the current goal is (left_endpoint_in_closed_interval 0 1 Hab01).
We prove the intermediate claim H1I01: 1 ∈ I01.
An exact proof term for the current goal is (right_endpoint_in_closed_interval 0 1 Hab01).
Set A0 to be the term (∀j : set, j ∈ ω → topology_on (apply_fun Xi j) (apply_fun Ti j)).
Set B0 to be the term (∀j : set, j ∈ ω → apply_fun Xi j ⊆ apply_fun Xi (ordsucc j)).
Set C0 to be the term (∀j : set, j ∈ ω → subspace_topology (apply_fun Xi (ordsucc j)) (apply_fun Ti (ordsucc j)) (apply_fun Xi j) = apply_fun Ti j).
Set D0 to be the term (∀j : set, j ∈ ω → closed_in (apply_fun Xi (ordsucc j)) (apply_fun Ti (ordsucc j)) (apply_fun Xi j)).
We prove the intermediate claim Habc: (A0 ∧ B0) ∧ C0.
An exact proof term for the current goal is (andEL ((A0 ∧ B0) ∧ C0) D0 Hchain).
We prove the intermediate claim HAall: A0.
An exact proof term for the current goal is (andEL A0 B0 (andEL (A0 ∧ B0) C0 Habc)).
We prove the intermediate claim HC: C0.
An exact proof term for the current goal is (andER (A0 ∧ B0) C0 Habc).
We prove the intermediate claim HD: D0.
An exact proof term for the current goal is (andER ((A0 ∧ B0) ∧ C0) D0 Hchain).
We prove the intermediate claim Htop_s: topology_on Xi_s Ti_s.
An exact proof term for the current goal is (HAall (ordsucc i) (omega_ordsucc i HiO)).
We prove the intermediate claim Hnorm_s: normal_space Xi_s Ti_s.
An exact proof term for the current goal is (Hnorms (ordsucc i) (omega_ordsucc i HiO)).
We prove the intermediate claim HA_s_closed: closed_in Xi_s Ti_s (A ∩ Xi_s).
An exact proof term for the current goal is (closed_in_coherent_component Xi Ti A (ordsucc i) HAall HAcl (omega_ordsucc i HiO)).
We prove the intermediate claim HB_s_closed: closed_in Xi_s Ti_s (B ∩ Xi_s).
An exact proof term for the current goal is (closed_in_coherent_component Xi Ti B (ordsucc i) HAall HBcl (omega_ordsucc i HiO)).
We prove the intermediate claim HXi_i_closed: closed_in Xi_s Ti_s Xi_i.
An exact proof term for the current goal is (HD i HiO).
We prove the intermediate claim Hsubeq: subspace_topology Xi_s Ti_s Xi_i = Ti_i.
An exact proof term for the current goal is (HC i HiO).
Set As to be the term A ∩ Xi_s.
Set Bs to be the term B ∩ Xi_s.
Set X1 to be the term Xi_i ∪ As.
Set D to be the term X1 ∪ Bs.
Set Tx1 to be the term subspace_topology Xi_s Ti_s X1.
Set TxD to be the term subspace_topology Xi_s Ti_s D.
We prove the intermediate claim HX1sub: X1 ⊆ Xi_s.
Apply binunion_Subq_min to the current goal.
We prove the intermediate claim HsubXi: Xi_i ⊆ Xi_s.
An exact proof term for the current goal is (andER A0 B0 (andEL (A0 ∧ B0) C0 Habc) i HiO).
An exact proof term for the current goal is HsubXi.
An exact proof term for the current goal is (binintersect_Subq_2 A Xi_s).
We prove the intermediate claim HXi_i_closed_X1: closed_in X1 Tx1 Xi_i.
Apply (iffER (closed_in X1 Tx1 Xi_i) (∃C : set, closed_in Xi_s Ti_s C ∧ Xi_i = C ∩ X1) (closed_in_subspace_iff_intersection Xi_s Ti_s X1 Xi_i Htop_s HX1sub)) to the current goal.
We use Xi_i to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HXi_i_closed.
We will prove Xi_i = Xi_i ∩ X1.
We prove the intermediate claim HXiSub: Xi_i ⊆ X1.
An exact proof term for the current goal is (binunion_Subq_1 Xi_i As).
rewrite the current goal using (binintersect_Subq_eq_1 Xi_i X1 HXiSub) (from left to right).
Use reflexivity.
We prove the intermediate claim HAs_closed_X1: closed_in X1 Tx1 As.
Apply (iffER (closed_in X1 Tx1 As) (∃C : set, closed_in Xi_s Ti_s C ∧ As = C ∩ X1) (closed_in_subspace_iff_intersection Xi_s Ti_s X1 As Htop_s HX1sub)) to the current goal.
We use As to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HA_s_closed.
We will prove As = As ∩ X1.
We prove the intermediate claim HAsSub: As ⊆ X1.
An exact proof term for the current goal is (binunion_Subq_2 Xi_i As).
rewrite the current goal using (binintersect_Subq_eq_1 As X1 HAsSub) (from left to right).
Use reflexivity.
We prove the intermediate claim Hfi_X1: continuous_map Xi_i (subspace_topology X1 Tx1 Xi_i) I01 T01 fi.
We prove the intermediate claim HXisubX1: Xi_i ⊆ X1.
An exact proof term for the current goal is (binunion_Subq_1 Xi_i As).
We prove the intermediate claim HX1subXis: X1 ⊆ Xi_s.
An exact proof term for the current goal is HX1sub.
We prove the intermediate claim HeqTrans: subspace_topology X1 (subspace_topology Xi_s Ti_s X1) Xi_i = subspace_topology Xi_s Ti_s Xi_i.
An exact proof term for the current goal is (ex16_1_subspace_transitive Xi_s Ti_s X1 Xi_i Htop_s HX1subXis HXisubX1).
We prove the intermediate claim HeqTi: subspace_topology Xi_s Ti_s Xi_i = Ti_i.
An exact proof term for the current goal is Hsubeq.
We prove the intermediate claim HTx1def: Tx1 = subspace_topology Xi_s Ti_s X1.
Use reflexivity.
rewrite the current goal using HTx1def (from left to right).
rewrite the current goal using HeqTrans (from left to right).
rewrite the current goal using HeqTi (from left to right).
An exact proof term for the current goal is Hfi.
Set fA to be the term const_fun As 0.
We prove the intermediate claim HtopAs: topology_on As (subspace_topology X1 Tx1 As).
An exact proof term for the current goal is (subspace_topology_is_topology X1 Tx1 As (subspace_topology_is_topology Xi_s Ti_s X1 Htop_s HX1sub) (binunion_Subq_2 Xi_i As)).
We prove the intermediate claim HI01top: topology_on I01 T01.
An exact proof term for the current goal is (closed_interval_topology_on 0 1).
We prove the intermediate claim HfA_cont: continuous_map As (subspace_topology X1 Tx1 As) I01 T01 fA.
An exact proof term for the current goal is (const_fun_continuous As (subspace_topology X1 Tx1 As) I01 T01 0 HtopAs HI01top H0I01).
We prove the intermediate claim Hagree1: ∀x : set, x ∈ (Xi_i ∩ As) → apply_fun fi x = apply_fun fA x.
Let x be given.
Assume Hx: x ∈ Xi_i ∩ As.
We prove the intermediate claim HxAi: x ∈ (A ∩ Xi_i).
Apply binintersectE Xi_i As x Hx to the current goal.
Assume HxXi HxAs.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectE1 A Xi_s x HxAs).
An exact proof term for the current goal is (binintersectI A Xi_i x HxA HxXi).
We prove the intermediate claim Hfi0: apply_fun fi x = 0.
An exact proof term for the current goal is (HfiA0 x HxAi).
We prove the intermediate claim HfA0: apply_fun fA x = 0.
An exact proof term for the current goal is (const_fun_apply As 0 x (binintersectE2 Xi_i As x Hx)).
rewrite the current goal using Hfi0 (from left to right).
rewrite the current goal using HfA0 (from left to right).
Use reflexivity.
We prove the intermediate claim HX1eq: Xi_i ∪ As = X1.
Use reflexivity.
We prove the intermediate claim Hexh1: ∃h1 : set, continuous_map X1 Tx1 I01 T01 h1 ∧ ((∀x : set, x ∈ Xi_i → apply_fun h1 x = apply_fun fi x) ∧ (∀x : set, x ∈ As → apply_fun h1 x = apply_fun fA x)).
An exact proof term for the current goal is (pasting_lemma X1 Xi_i As I01 Tx1 T01 fi fA (subspace_topology_is_topology Xi_s Ti_s X1 Htop_s HX1sub) HXi_i_closed_X1 HAs_closed_X1 HX1eq Hfi_X1 HfA_cont Hagree1).
Apply Hexh1 to the current goal.
Let h1 be given.
Assume Hh1pack.
We prove the intermediate claim Hh1cont: continuous_map X1 Tx1 I01 T01 h1.
An exact proof term for the current goal is (andEL (continuous_map X1 Tx1 I01 T01 h1) ((∀x : set, x ∈ Xi_i → apply_fun h1 x = apply_fun fi x) ∧ (∀x : set, x ∈ As → apply_fun h1 x = apply_fun fA x)) Hh1pack).
We prove the intermediate claim Hh1rest: (∀x : set, x ∈ Xi_i → apply_fun h1 x = apply_fun fi x) ∧ (∀x : set, x ∈ As → apply_fun h1 x = apply_fun fA x).
An exact proof term for the current goal is (andER (continuous_map X1 Tx1 I01 T01 h1) ((∀x : set, x ∈ Xi_i → apply_fun h1 x = apply_fun fi x) ∧ (∀x : set, x ∈ As → apply_fun h1 x = apply_fun fA x)) Hh1pack).
We prove the intermediate claim HDsub: D ⊆ Xi_s.
Apply binunion_Subq_min to the current goal.
An exact proof term for the current goal is (Subq_tra X1 Xi_s Xi_s HX1sub (Subq_ref Xi_s)).
An exact proof term for the current goal is (binintersect_Subq_2 B Xi_s).
We prove the intermediate claim HX1subD: X1 ⊆ D.
An exact proof term for the current goal is (binunion_Subq_1 X1 Bs).
We prove the intermediate claim HBsSubD: Bs ⊆ D.
An exact proof term for the current goal is (binunion_Subq_2 X1 Bs).
We prove the intermediate claim HX1_closed_D: closed_in D TxD X1.
Apply (iffER (closed_in D TxD X1) (∃C : set, closed_in Xi_s Ti_s C ∧ X1 = C ∩ D) (closed_in_subspace_iff_intersection Xi_s Ti_s D X1 Htop_s HDsub)) to the current goal.
We use X1 to witness the existential quantifier.
Apply andI to the current goal.
rewrite the current goal using HX1eq (from right to left).
An exact proof term for the current goal is (closed_binunion Xi_s Ti_s Xi_i As HXi_i_closed HA_s_closed).
We will prove X1 = X1 ∩ D.
rewrite the current goal using (binintersect_Subq_eq_1 X1 D HX1subD) (from left to right).
Use reflexivity.
We prove the intermediate claim HBs_closed_D: closed_in D TxD Bs.
Apply (iffER (closed_in D TxD Bs) (∃C : set, closed_in Xi_s Ti_s C ∧ Bs = C ∩ D) (closed_in_subspace_iff_intersection Xi_s Ti_s D Bs Htop_s HDsub)) to the current goal.
We use Bs to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HB_s_closed.
We will prove Bs = Bs ∩ D.
rewrite the current goal using (binintersect_Subq_eq_1 Bs D HBsSubD) (from left to right).
Use reflexivity.
We prove the intermediate claim Hh1_XD: continuous_map X1 (subspace_topology D TxD X1) I01 T01 h1.
We prove the intermediate claim HeqTrans: subspace_topology D (subspace_topology Xi_s Ti_s D) X1 = subspace_topology Xi_s Ti_s X1.
An exact proof term for the current goal is (ex16_1_subspace_transitive Xi_s Ti_s D X1 Htop_s HDsub HX1subD).
We prove the intermediate claim HTxDdef: TxD = subspace_topology Xi_s Ti_s D.
Use reflexivity.
rewrite the current goal using HTxDdef (from left to right).
rewrite the current goal using HeqTrans (from left to right).
An exact proof term for the current goal is Hh1cont.
Set fB to be the term const_fun Bs 1.
We prove the intermediate claim HtopBs: topology_on Bs (subspace_topology D TxD Bs).
An exact proof term for the current goal is (subspace_topology_is_topology D TxD Bs (subspace_topology_is_topology Xi_s Ti_s D Htop_s HDsub) HBsSubD).
We prove the intermediate claim HfB_cont: continuous_map Bs (subspace_topology D TxD Bs) I01 T01 fB.
An exact proof term for the current goal is (const_fun_continuous Bs (subspace_topology D TxD Bs) I01 T01 1 HtopBs HI01top H1I01).
We prove the intermediate claim Hagree2: ∀x : set, x ∈ (X1 ∩ Bs) → apply_fun h1 x = apply_fun fB x.
Let x be given.
Assume Hx: x ∈ X1 ∩ Bs.
We prove the intermediate claim HxBs: x ∈ Bs.
An exact proof term for the current goal is (binintersectE2 X1 Bs x Hx).
We prove the intermediate claim HxB: x ∈ B.
An exact proof term for the current goal is (binintersectE1 B Xi_s x HxBs).
We prove the intermediate claim HxX1: x ∈ X1.
An exact proof term for the current goal is (binintersectE1 X1 Bs x Hx).
Apply (binunionE' Xi_i As x (apply_fun h1 x = apply_fun fB x)) to the current goal.
Assume HxXi: x ∈ Xi_i.
We prove the intermediate claim HxBi: x ∈ (B ∩ Xi_i).
An exact proof term for the current goal is (binintersectI B Xi_i x HxB HxXi).
We prove the intermediate claim Hfi1: apply_fun fi x = 1.
An exact proof term for the current goal is (HfiB1 x HxBi).
We prove the intermediate claim Hh1fi: apply_fun h1 x = apply_fun fi x.
An exact proof term for the current goal is ((andEL (∀y : set, y ∈ Xi_i → apply_fun h1 y = apply_fun fi y) (∀y : set, y ∈ As → apply_fun h1 y = apply_fun fA y) Hh1rest) x HxXi).
We prove the intermediate claim HfB1: apply_fun fB x = 1.
An exact proof term for the current goal is (const_fun_apply Bs 1 x HxBs).
rewrite the current goal using Hh1fi (from left to right).
rewrite the current goal using Hfi1 (from left to right).
rewrite the current goal using HfB1 (from left to right).
Use reflexivity.
Assume HxAs: x ∈ As.
We prove the intermediate claim HxAB: x ∈ A ∩ B.
An exact proof term for the current goal is (binintersectI A B x (binintersectE1 A Xi_s x HxAs) HxB).
We prove the intermediate claim HxEmpty: x ∈ Empty.
rewrite the current goal using Hab (from right to left).
An exact proof term for the current goal is HxAB.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE x HxEmpty).
An exact proof term for the current goal is HxX1.
We prove the intermediate claim HDeq: X1 ∪ Bs = D.
Use reflexivity.
We prove the intermediate claim HexhD: ∃hD : set, continuous_map D TxD I01 T01 hD ∧ ((∀x : set, x ∈ X1 → apply_fun hD x = apply_fun h1 x) ∧ (∀x : set, x ∈ Bs → apply_fun hD x = apply_fun fB x)).
An exact proof term for the current goal is (pasting_lemma D X1 Bs I01 TxD T01 h1 fB (subspace_topology_is_topology Xi_s Ti_s D Htop_s HDsub) HX1_closed_D HBs_closed_D HDeq Hh1_XD HfB_cont Hagree2).
Apply HexhD to the current goal.
Let hD be given.
Assume HhDpack.
We prove the intermediate claim HhDcont: continuous_map D TxD I01 T01 hD.
An exact proof term for the current goal is (andEL (continuous_map D TxD I01 T01 hD) ((∀x : set, x ∈ X1 → apply_fun hD x = apply_fun h1 x) ∧ (∀x : set, x ∈ Bs → apply_fun hD x = apply_fun fB x)) HhDpack).
We prove the intermediate claim HhDrest: (∀x : set, x ∈ X1 → apply_fun hD x = apply_fun h1 x) ∧ (∀x : set, x ∈ Bs → apply_fun hD x = apply_fun fB x).
An exact proof term for the current goal is (andER (continuous_map D TxD I01 T01 hD) ((∀x : set, x ∈ X1 → apply_fun hD x = apply_fun h1 x) ∧ (∀x : set, x ∈ Bs → apply_fun hD x = apply_fun fB x)) HhDpack).
We prove the intermediate claim HDclosed: closed_in Xi_s Ti_s D.
We prove the intermediate claim HX1closed: closed_in Xi_s Ti_s X1.
rewrite the current goal using HX1eq (from right to left).
An exact proof term for the current goal is (closed_binunion Xi_s Ti_s Xi_i As HXi_i_closed HA_s_closed).
rewrite the current goal using HDeq (from right to left).
An exact proof term for the current goal is (closed_binunion Xi_s Ti_s X1 Bs HX1closed HB_s_closed).
We prove the intermediate claim Hext: ∃gi : set, continuous_map Xi_s Ti_s I01 T01 gi ∧ (∀x : set, x ∈ D → apply_fun gi x = apply_fun hD x).
An exact proof term for the current goal is (Tietze_extension_interval Xi_s Ti_s D 0 1 hD Hab01 Hnorm_s HDclosed HhDcont).
Apply Hext to the current goal.
Let gi be given.
Assume Hgi.
We use gi to witness the existential quantifier.
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 (andEL (continuous_map Xi_s Ti_s I01 T01 gi) (∀x : set, x ∈ D → apply_fun gi x = apply_fun hD x) Hgi).
Let x be given.
Assume HxXi: x ∈ Xi_i.
We prove the intermediate claim HxX1: x ∈ X1.
An exact proof term for the current goal is (binunionI1 Xi_i As x HxXi).
We prove the intermediate claim HxD: x ∈ D.
An exact proof term for the current goal is (binunionI1 X1 Bs x HxX1).
We prove the intermediate claim HgihD: apply_fun gi x = apply_fun hD x.
An exact proof term for the current goal is ((andER (continuous_map Xi_s Ti_s I01 T01 gi) (∀y : set, y ∈ D → apply_fun gi y = apply_fun hD y) Hgi) x HxD).
We prove the intermediate claim HhDh1: apply_fun hD x = apply_fun h1 x.
An exact proof term for the current goal is ((andEL (∀y : set, y ∈ X1 → apply_fun hD y = apply_fun h1 y) (∀y : set, y ∈ Bs → apply_fun hD y = apply_fun fB y) HhDrest) x HxX1).
We prove the intermediate claim Hh1fi: apply_fun h1 x = apply_fun fi x.
An exact proof term for the current goal is ((andEL (∀y : set, y ∈ Xi_i → apply_fun h1 y = apply_fun fi y) (∀y : set, y ∈ As → apply_fun h1 y = apply_fun fA y) Hh1rest) x HxXi).
rewrite the current goal using HgihD (from left to right).
rewrite the current goal using HhDh1 (from left to right).
rewrite the current goal using Hh1fi (from left to right).
Use reflexivity.
Let x be given.
Assume HxAs: x ∈ (A ∩ Xi_s).
We prove the intermediate claim HxX1: x ∈ X1.
An exact proof term for the current goal is (binunionI2 Xi_i As x HxAs).
We prove the intermediate claim HxD: x ∈ D.
An exact proof term for the current goal is (binunionI1 X1 Bs x HxX1).
We prove the intermediate claim HgihD: apply_fun gi x = apply_fun hD x.
An exact proof term for the current goal is ((andER (continuous_map Xi_s Ti_s I01 T01 gi) (∀y : set, y ∈ D → apply_fun gi y = apply_fun hD y) Hgi) x HxD).
We prove the intermediate claim HhDh1: apply_fun hD x = apply_fun h1 x.
An exact proof term for the current goal is ((andEL (∀y : set, y ∈ X1 → apply_fun hD y = apply_fun h1 y) (∀y : set, y ∈ Bs → apply_fun hD y = apply_fun fB y) HhDrest) x HxX1).
We prove the intermediate claim Hh1fA: apply_fun h1 x = apply_fun fA x.
An exact proof term for the current goal is ((andER (∀y : set, y ∈ Xi_i → apply_fun h1 y = apply_fun fi y) (∀y : set, y ∈ As → apply_fun h1 y = apply_fun fA y) Hh1rest) x HxAs).
We prove the intermediate claim HfA0: apply_fun fA x = 0.
An exact proof term for the current goal is (const_fun_apply As 0 x HxAs).
rewrite the current goal using HgihD (from left to right).
rewrite the current goal using HhDh1 (from left to right).
rewrite the current goal using Hh1fA (from left to right).
rewrite the current goal using HfA0 (from left to right).
Use reflexivity.
Let x be given.
Assume HxBs: x ∈ (B ∩ Xi_s).
We prove the intermediate claim HxD: x ∈ D.
An exact proof term for the current goal is (binunionI2 X1 Bs x HxBs).
We prove the intermediate claim HgihD: apply_fun gi x = apply_fun hD x.
An exact proof term for the current goal is ((andER (continuous_map Xi_s Ti_s I01 T01 gi) (∀y : set, y ∈ D → apply_fun gi y = apply_fun hD y) Hgi) x HxD).
We prove the intermediate claim HhDfB: apply_fun hD x = apply_fun fB x.
An exact proof term for the current goal is ((andER (∀y : set, y ∈ X1 → apply_fun hD y = apply_fun h1 y) (∀y : set, y ∈ Bs → apply_fun hD y = apply_fun fB y) HhDrest) x HxBs).
We prove the intermediate claim HfB1: apply_fun fB x = 1.
An exact proof term for the current goal is (const_fun_apply Bs 1 x HxBs).
rewrite the current goal using HgihD (from left to right).
rewrite the current goal using HhDfB (from left to right).
rewrite the current goal using HfB1 (from left to right).
Use reflexivity.
∎