Let X, Tx, Y, Ty and f be given.
Assume Hcomp: compact_space X Tx.
Assume HH: Hausdorff_space Y Ty.
Assume Hcont: continuous_map X Tx Y Ty f.
Assume Hbij: bijection X Y f.
Set g to be the term inv_fun_graph X f Y.
We will prove continuous_map Y Ty X Tx g.
We will prove topology_on Y Ty ∧ topology_on X Tx ∧ function_on g Y X ∧ ∀V : set, V ∈ Tx → preimage_of Y g V ∈ Ty.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (compact_space_topology X Tx Hcomp).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (andEL (topology_on Y Ty) (∀x1 x2 : set, x1 ∈ Y → x2 ∈ Y → x1 ≠ x2 → ∃U V : set, U ∈ Ty ∧ V ∈ Ty ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty) HH).
We prove the intermediate claim Hfun: function_on f X Y.
An exact proof term for the current goal is (andEL (function_on f X Y) (∀y : set, y ∈ Y → ∃x0 : set, x0 ∈ X ∧ apply_fun f x0 = y ∧ (∀x' : set, x' ∈ X → apply_fun f x' = y → x' = x0)) Hbij).
We prove the intermediate claim Hgfun: function_on g Y X.
Let y be given.
Assume Hy: y ∈ Y.
We will prove apply_fun g y ∈ X.
We prove the intermediate claim Hginv: apply_fun g y = inv X (λu : set ⇒ apply_fun f u) y.
An exact proof term for the current goal is (inv_fun_graph_apply X Y f y Hy).
rewrite the current goal using Hginv (from left to right).
We prove the intermediate claim Hsurj: ∀w ∈ Y, ∃u ∈ X, apply_fun f u = w.
Let w be given.
Assume Hw: w ∈ Y.
We prove the intermediate claim Hex: ∃u : set, u ∈ X ∧ apply_fun f u = w.
An exact proof term for the current goal is (bijection_surj X Y f w Hbij Hw).
An exact proof term for the current goal is Hex.
We prove the intermediate claim Hpair: inv X (λu : set ⇒ apply_fun f u) y ∈ X ∧ apply_fun f (inv X (λu : set ⇒ apply_fun f u) y) = y.
An exact proof term for the current goal is (surj_rinv X Y (λu : set ⇒ apply_fun f u) Hsurj y Hy).
An exact proof term for the current goal is (andEL (inv X (λu : set ⇒ apply_fun f u) y ∈ X) (apply_fun f (inv X (λu : set ⇒ apply_fun f u) y) = y) Hpair).
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 HTy.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is Hgfun.
Let V be given.
Assume HV: V ∈ Tx.
We will prove preimage_of Y g V ∈ Ty.
Set C to be the term X ∖ V.
We prove the intermediate claim HCclosed: closed_in X Tx C.
An exact proof term for the current goal is (closed_of_open_complement X Tx V HTx HV).
We prove the intermediate claim HCsub: C ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx C HCclosed).
We prove the intermediate claim HpreCeq: preimage_of Y g C = image_of_fun f C.
An exact proof term for the current goal is (inv_fun_graph_preimage_eq_image X Y f C Hbij HCsub).
We prove the intermediate claim HimgSubY: image_of_fun f C ⊆ Y.
Let y be given.
Assume Hy: y ∈ image_of_fun f C.
Apply (ReplE_impred C (λx0 : set ⇒ apply_fun f x0) y Hy) to the current goal.
Let x0 be given.
Assume Hx0C: x0 ∈ C.
Assume Heq: y = apply_fun f x0.
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (HCsub x0 Hx0C).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (Hfun x0 Hx0X).
We prove the intermediate claim HcompC: compact_space C (subspace_topology X Tx C).
An exact proof term for the current goal is (closed_subspace_compact X Tx C Hcomp HCclosed).
We prove the intermediate claim HcontC: continuous_map C (subspace_topology X Tx C) Y Ty f.
An exact proof term for the current goal is (continuous_on_subspace X Tx Y Ty f C HTx HCsub Hcont).
We prove the intermediate claim HimgComp: compact_space (image_of_fun f C) (subspace_topology Y Ty (image_of_fun f C)).
An exact proof term for the current goal is (continuous_image_compact C (subspace_topology X Tx C) Y Ty f HcompC HcontC).
We prove the intermediate claim HimgClosed: closed_in Y Ty (image_of_fun f C).
An exact proof term for the current goal is (compact_subspace_in_Hausdorff_closed Y Ty (image_of_fun f C) HH HimgSubY HimgComp).
We prove the intermediate claim HpreClosed: closed_in Y Ty (preimage_of Y g C).
rewrite the current goal using HpreCeq (from left to right) at position 1.
An exact proof term for the current goal is HimgClosed.
We prove the intermediate claim Hop: open_in Y Ty (Y ∖ preimage_of Y g C).
An exact proof term for the current goal is (open_of_closed_complement Y Ty (preimage_of Y g C) HpreClosed).
We prove the intermediate claim HopTy: (Y ∖ preimage_of Y g C) ∈ Ty.
An exact proof term for the current goal is (andER (topology_on Y Ty) ((Y ∖ preimage_of Y g C) ∈ Ty) Hop).
We prove the intermediate claim HpreEq: preimage_of Y g V = Y ∖ preimage_of Y g C.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ preimage_of Y g V.
We will prove y ∈ Y ∖ preimage_of Y g C.
We prove the intermediate claim HyY: y ∈ Y.
An exact proof term for the current goal is (SepE1 Y (λu : set ⇒ apply_fun g u ∈ V) y Hy).
We prove the intermediate claim HgyV: apply_fun g y ∈ V.
An exact proof term for the current goal is (SepE2 Y (λu : set ⇒ apply_fun g u ∈ V) y Hy).
Apply setminusI to the current goal.
An exact proof term for the current goal is HyY.
Assume HyC: y ∈ preimage_of Y g C.
We prove the intermediate claim HgyC: apply_fun g y ∈ C.
An exact proof term for the current goal is (SepE2 Y (λu : set ⇒ apply_fun g u ∈ C) y HyC).
Apply (setminusE X V (apply_fun g y) HgyC) to the current goal.
Assume _.
Assume HnotV.
An exact proof term for the current goal is (HnotV HgyV).
Let y be given.
Assume Hy: y ∈ Y ∖ preimage_of Y g C.
We will prove y ∈ preimage_of Y g V.
Apply (setminusE Y (preimage_of Y g C) y Hy) to the current goal.
Assume HyY: y ∈ Y.
Assume HyNot: y ∉ preimage_of Y g C.
We will prove y ∈ {u ∈ Y|apply_fun g u ∈ V}.
Apply SepI to the current goal.
An exact proof term for the current goal is HyY.
We will prove apply_fun g y ∈ V.
We prove the intermediate claim HgyX: apply_fun g y ∈ X.
An exact proof term for the current goal is (Hgfun y HyY).
Apply (xm (apply_fun g y ∈ V)) to the current goal.
Assume HVin.
An exact proof term for the current goal is HVin.
Assume HnotV: ¬ (apply_fun g y ∈ V).
We prove the intermediate claim HnotVin: apply_fun g y ∉ V.
Assume H0.
An exact proof term for the current goal is (HnotV H0).
We prove the intermediate claim HgyC: apply_fun g y ∈ C.
An exact proof term for the current goal is (setminusI X V (apply_fun g y) HgyX HnotVin).
We prove the intermediate claim HyC: y ∈ preimage_of Y g C.
We will prove y ∈ {u ∈ Y|apply_fun g u ∈ C}.
Apply SepI to the current goal.
An exact proof term for the current goal is HyY.
An exact proof term for the current goal is HgyC.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HyNot HyC).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is HopTy.
∎