Let X, Tx, m, U, V, f and x be given.
Assume HmO: m ∈ ω.
Assume HTx: topology_on X Tx.
Assume HUopen: open_in X Tx U.
Assume HxU: x ∈ U.
Assume HVsubE: V ⊆ (euclidean_space m).
Assume HVopenE: open_in (euclidean_space m) (euclidean_topology m) V.
Assume Hhom: homeomorphism U (subspace_topology X Tx U) V (subspace_topology (euclidean_space m) (euclidean_topology m) V) f.
Set Tu to be the term subspace_topology X Tx U.
Set Tv to be the term subspace_topology (euclidean_space m) (euclidean_topology m) V.
We prove the intermediate claim Hcontf: continuous_map U Tu V Tv f.
An exact proof term for the current goal is (homeomorphism_continuous U Tu V Tv f Hhom).
We prove the intermediate claim Hfunf: function_on f U V.
An exact proof term for the current goal is (continuous_map_function_on U Tu V Tv f Hcontf).
Set y to be the term apply_fun f x.
We prove the intermediate claim HyV: y ∈ V.
An exact proof term for the current goal is (Hfunf x HxU).
We prove the intermediate claim Hexg: ∃g : set, continuous_map V Tv U Tu g ∧ (∀x0 : set, x0 ∈ U → apply_fun g (apply_fun f x0) = x0) ∧ (∀y0 : set, y0 ∈ V → apply_fun f (apply_fun g y0) = y0).
An exact proof term for the current goal is (homeomorphism_inverse_package U Tu V Tv f Hhom).
Apply Hexg to the current goal.
Let g be given.
Assume Hgpack.
We prove the intermediate claim Hgleft: (continuous_map V Tv U Tu g ∧ (∀x0 : set, x0 ∈ U → apply_fun g (apply_fun f x0) = x0)).
An exact proof term for the current goal is (andEL (continuous_map V Tv U Tu g ∧ (∀x0 : set, x0 ∈ U → apply_fun g (apply_fun f x0) = x0)) (∀y0 : set, y0 ∈ V → apply_fun f (apply_fun g y0) = y0) Hgpack).
We prove the intermediate claim Hgcont: continuous_map V Tv U Tu g.
An exact proof term for the current goal is (andEL (continuous_map V Tv U Tu g) (∀x0 : set, x0 ∈ U → apply_fun g (apply_fun f x0) = x0) Hgleft).
We prove the intermediate claim Hgf: ∀x0 : set, x0 ∈ U → apply_fun g (apply_fun f x0) = x0.
An exact proof term for the current goal is (andER (continuous_map V Tv U Tu g) (∀x0 : set, x0 ∈ U → apply_fun g (apply_fun f x0) = x0) Hgleft).
We prove the intermediate claim HtopE: topology_on (euclidean_space m) (euclidean_topology m).
An exact proof term for the current goal is (Hausdorff_space_topology (euclidean_space m) (euclidean_topology m) (euclidean_space_Hausdorff m)).
We prove the intermediate claim HexW: ∃W : set, W ∈ (euclidean_topology m) ∧ y ∈ W ∧ closure_of (euclidean_space m) (euclidean_topology m) W ⊆ V ∧ compact_space (closure_of (euclidean_space m) (euclidean_topology m) W) (subspace_topology (euclidean_space m) (euclidean_topology m) (closure_of (euclidean_space m) (euclidean_topology m) W)).
An exact proof term for the current goal is (euclidean_open_has_compact_closure_neighborhood m V y HmO HVsubE HVopenE HyV).
Apply HexW to the current goal.
Let W be given.
Assume HWpack.
Apply (and4E (W ∈ (euclidean_topology m)) (y ∈ W) (closure_of (euclidean_space m) (euclidean_topology m) W ⊆ V) (compact_space (closure_of (euclidean_space m) (euclidean_topology m) W) (subspace_topology (euclidean_space m) (euclidean_topology m) (closure_of (euclidean_space m) (euclidean_topology m) W))) HWpack) to the current goal.
Assume HWopen HyW HK0subV HK0comp.
Set K0 to be the term closure_of (euclidean_space m) (euclidean_topology m) W.
We prove the intermediate claim HWsubV: W ⊆ V.
We prove the intermediate claim HWsubK0: W ⊆ K0.
An exact proof term for the current goal is (subset_of_closure (euclidean_space m) (euclidean_topology m) W HtopE (topology_elem_subset (euclidean_space m) (euclidean_topology m) W HtopE HWopen)).
An exact proof term for the current goal is (Subq_tra W K0 V HWsubK0 HK0subV).
Set U1 to be the term preimage_of U f W.
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx U HUopen).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HUinTx).
We prove the intermediate claim HU1subU: U1 ⊆ U.
Let z be given.
Assume Hz: z ∈ U1.
An exact proof term for the current goal is (SepE1 U (λu0 : set ⇒ apply_fun f u0 ∈ W) z Hz).
We prove the intermediate claim HWinTv: W ∈ Tv.
We prove the intermediate claim HWcapV: W ∩ V ∈ Tv.
An exact proof term for the current goal is (subspace_topologyI (euclidean_space m) (euclidean_topology m) V W HWopen).
rewrite the current goal using (binintersect_Subq_eq_1 W V HWsubV) (from right to left).
An exact proof term for the current goal is HWcapV.
We prove the intermediate claim HU1openU: U1 ∈ Tu.
An exact proof term for the current goal is (continuous_map_preimage U Tu V Tv f Hcontf W HWinTv).
We prove the intermediate claim HU1inTx: U1 ∈ Tx.
We prove the intermediate claim HtopU: topology_on U Tu.
An exact proof term for the current goal is (subspace_topology_is_topology X Tx U HTx HUsubX).
We prove the intermediate claim HU1openinU: open_in U Tu U1.
An exact proof term for the current goal is (andI (topology_on U Tu) (U1 ∈ Tu) HtopU HU1openU).
An exact proof term for the current goal is (open_in_subspace_if_ambient_open X Tx U U1 HTx HUinTx HU1subU HU1openinU).
We prove the intermediate claim HxU1: x ∈ U1.
We prove the intermediate claim Hyeq: y = apply_fun f x.
Use reflexivity.
We prove the intermediate claim HfxW: apply_fun f x ∈ W.
rewrite the current goal using Hyeq (from right to left).
An exact proof term for the current goal is HyW.
An exact proof term for the current goal is (SepI U (λu0 : set ⇒ apply_fun f u0 ∈ W) x HxU HfxW).
Set gIm to be the term image_of_fun g K0.
We prove the intermediate claim HK0subE: K0 ⊆ (euclidean_space m).
An exact proof term for the current goal is (closure_in_space (euclidean_space m) (euclidean_topology m) W HtopE).
We prove the intermediate claim HK0subV2: K0 ⊆ V.
An exact proof term for the current goal is HK0subV.
We prove the intermediate claim HtopV: topology_on V Tv.
An exact proof term for the current goal is (subspace_topology_is_topology (euclidean_space m) (euclidean_topology m) V HtopE HVsubE).
We prove the intermediate claim HgXcont: continuous_map V Tv X Tx g.
We prove the intermediate claim HTuEq: Tu = subspace_topology X Tx U.
Use reflexivity.
An exact proof term for the current goal is (continuous_map_range_expand V Tv U Tu X Tx g Hgcont HUsubX HTx HTuEq).
We prove the intermediate claim HgK0contV: continuous_map K0 (subspace_topology V Tv K0) X Tx g.
An exact proof term for the current goal is (continuous_on_subspace_rule V Tv X Tx g K0 HtopV HTx HK0subV2 HgXcont).
We prove the intermediate claim HtopK0eq: subspace_topology V Tv K0 = subspace_topology (euclidean_space m) (euclidean_topology m) K0.
An exact proof term for the current goal is (ex16_1_subspace_transitive (euclidean_space m) (euclidean_topology m) V K0 HtopE HVsubE HK0subV2).
We prove the intermediate claim HgK0cont: continuous_map K0 (subspace_topology (euclidean_space m) (euclidean_topology m) K0) X Tx g.
rewrite the current goal using HtopK0eq (from right to left).
An exact proof term for the current goal is HgK0contV.
We prove the intermediate claim HgIm_comp: compact_space gIm (subspace_topology X Tx gIm).
An exact proof term for the current goal is (continuous_image_compact K0 (subspace_topology (euclidean_space m) (euclidean_topology m) K0) X Tx g HK0comp HgK0cont).
We prove the intermediate claim HU1subgIm: U1 ⊆ gIm.
Let z be given.
Assume HzU1: z ∈ U1.
We will prove z ∈ gIm.
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (SepE1 U (λu0 : set ⇒ apply_fun f u0 ∈ W) z HzU1).
We prove the intermediate claim HfzW: apply_fun f z ∈ W.
An exact proof term for the current goal is (SepE2 U (λu0 : set ⇒ apply_fun f u0 ∈ W) z HzU1).
We prove the intermediate claim HfzK0: apply_fun f z ∈ K0.
An exact proof term for the current goal is ((subset_of_closure (euclidean_space m) (euclidean_topology m) W HtopE (topology_elem_subset (euclidean_space m) (euclidean_topology m) W HtopE HWopen)) (apply_fun f z) HfzW).
We prove the intermediate claim HzEq: z = apply_fun g (apply_fun f z).
rewrite the current goal using (Hgf z HzU) (from left to right).
Use reflexivity.
rewrite the current goal using HzEq (from left to right).
An exact proof term for the current goal is (ReplI K0 (λy0 : set ⇒ apply_fun g y0) (apply_fun f z) HfzK0).
We prove the intermediate claim HclU1sub: closure_of X Tx U1 ⊆ closure_of X Tx gIm.
We prove the intermediate claim Hfun_gVX: function_on g V X.
An exact proof term for the current goal is (continuous_map_function_on V Tv X Tx g HgXcont).
We prove the intermediate claim HgImsubX: gIm ⊆ X.
An exact proof term for the current goal is (image_of_sub_codomain g V X K0 Hfun_gVX HK0subV2).
An exact proof term for the current goal is (closure_monotone X Tx U1 gIm HTx HU1subgIm HgImsubX).
We prove the intermediate claim HclgIm_comp: compact_space (closure_of X Tx gIm) (subspace_topology X Tx (closure_of X Tx gIm)).
We prove the intermediate claim Hfun_gVX: function_on g V X.
An exact proof term for the current goal is (continuous_map_function_on V Tv X Tx g HgXcont).
We prove the intermediate claim HgImsubX: gIm ⊆ X.
An exact proof term for the current goal is (image_of_sub_codomain g V X K0 Hfun_gVX HK0subV2).
An exact proof term for the current goal is (closure_of_compact_subspace_compact X Tx gIm HTx HgImsubX HgIm_comp).
We prove the intermediate claim HclU1_closed: closed_in X Tx (closure_of X Tx U1).
An exact proof term for the current goal is (andER (closure_of X Tx (closure_of X Tx U1) = closure_of X Tx U1) (closed_in X Tx (closure_of X Tx U1)) (closure_idempotent_and_closed X Tx U1 HTx)).
We prove the intermediate claim HclU1_comp: compact_space (closure_of X Tx U1) (subspace_topology X Tx (closure_of X Tx U1)).
Set C to be the term closure_of X Tx gIm.
Set Tc to be the term subspace_topology X Tx C.
We prove the intermediate claim HCsubX: C ⊆ X.
An exact proof term for the current goal is (closure_in_space X Tx gIm HTx).
We prove the intermediate claim HCcomp: compact_space C Tc.
An exact proof term for the current goal is HclgIm_comp.
We prove the intermediate claim HclU1subC: closure_of X Tx U1 ⊆ C.
An exact proof term for the current goal is HclU1sub.
We prove the intermediate claim HclU1_closed_in_C: closed_in C Tc (closure_of X Tx U1).
Apply (iffER (closed_in C (subspace_topology X Tx C) (closure_of X Tx U1)) (∃D : set, closed_in X Tx D ∧ (closure_of X Tx U1) = D ∩ C) (closed_in_subspace_iff_intersection X Tx C (closure_of X Tx U1) HTx HCsubX)) to the current goal.
We use (closure_of X Tx U1) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HclU1_closed.
rewrite the current goal using (binintersect_Subq_eq_1 (closure_of X Tx U1) C HclU1subC) (from left to right).
Use reflexivity.
We prove the intermediate claim HcompSub: compact_space (closure_of X Tx U1) (subspace_topology C Tc (closure_of X Tx U1)).
An exact proof term for the current goal is (closed_subspace_compact C Tc (closure_of X Tx U1) HCcomp HclU1_closed_in_C).
We prove the intermediate claim HeqTop: subspace_topology C Tc (closure_of X Tx U1) = subspace_topology X Tx (closure_of X Tx U1).
An exact proof term for the current goal is (ex16_1_subspace_transitive X Tx C (closure_of X Tx U1) HTx HCsubX HclU1subC).
rewrite the current goal using HeqTop (from right to left).
An exact proof term for the current goal is HcompSub.
We use U1 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HU1inTx.
An exact proof term for the current goal is HxU1.
An exact proof term for the current goal is HclU1_comp.
∎