Let X, Tx and Y be given.
Assume Hcomp: compact_space X Tx.
Assume HY: closed_in X Tx Y.
We will prove compact_space Y (subspace_topology X Tx Y).
Set Ty to be the term subspace_topology X Tx Y.
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 HsubcoverX: ∀Fam : set, open_cover_of X Tx Fam → has_finite_subcover X Tx Fam.
An exact proof term for the current goal is (compact_space_subcover_property X Tx Hcomp).
We prove the intermediate claim HYsub: Y ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx Y HY).
We prove the intermediate claim HexU: ∃U ∈ Tx, Y = X ∖ U.
We prove the intermediate claim HYparts: Y ⊆ X ∧ ∃U ∈ Tx, Y = X ∖ U.
An exact proof term for the current goal is (andER (topology_on X Tx) (Y ⊆ X ∧ ∃U ∈ Tx, Y = X ∖ U) HY).
An exact proof term for the current goal is (andER (Y ⊆ X) (∃U ∈ Tx, Y = X ∖ U) HYparts).
Apply HexU to the current goal.
Let U be given.
Assume HUpair: U ∈ Tx ∧ Y = X ∖ U.
We prove the intermediate claim HUu: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (Y = X ∖ U) HUpair).
We prove the intermediate claim HYeq: Y = X ∖ U.
An exact proof term for the current goal is (andER (U ∈ Tx) (Y = X ∖ U) HUpair).
We prove the intermediate claim Hequiv: (compact_space Y Ty ↔ ∀Fam : set, (Fam ⊆ Tx ∧ Y ⊆ ⋃ Fam) → has_finite_subcover Y Tx Fam).
An exact proof term for the current goal is (compact_subspace_via_ambient_covers X Tx Y HTx HYsub).
Apply (iffER (compact_space Y Ty) (∀Fam : set, (Fam ⊆ Tx ∧ Y ⊆ ⋃ Fam) → has_finite_subcover Y Tx Fam) Hequiv) to the current goal.
Let Fam be given.
Assume HFamcov: Fam ⊆ Tx ∧ Y ⊆ ⋃ Fam.
We prove the intermediate claim HFamSub: Fam ⊆ Tx.
An exact proof term for the current goal is (andEL (Fam ⊆ Tx) (Y ⊆ ⋃ Fam) HFamcov).
We prove the intermediate claim HYcovFam: Y ⊆ ⋃ Fam.
An exact proof term for the current goal is (andER (Fam ⊆ Tx) (Y ⊆ ⋃ Fam) HFamcov).
Set CoverX to be the term Fam ∪ {U}.
We prove the intermediate claim HcoverX: open_cover_of X Tx CoverX.
We will prove topology_on X Tx ∧ CoverX ⊆ 𝒫 X ∧ X ⊆ ⋃ CoverX ∧ (∀V : set, V ∈ CoverX → 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.
Let V be given.
Assume HV: V ∈ CoverX.
We will prove V ∈ 𝒫 X.
Apply (binunionE Fam {U} V HV) to the current goal.
Assume HVF: V ∈ Fam.
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (HFamSub V HVF).
We prove the intermediate claim HVsub: V ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx V HTx HVTx).
An exact proof term for the current goal is (PowerI X V HVsub).
Assume HVU: V ∈ {U}.
We prove the intermediate claim HVe: V = U.
An exact proof term for the current goal is (SingE U V HVU).
rewrite the current goal using HVe (from left to right).
We prove the intermediate claim HUsub: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HUu).
An exact proof term for the current goal is (PowerI X U HUsub).
Let x be given.
Assume HxX: x ∈ X.
We will prove x ∈ ⋃ CoverX.
Apply (xm (x ∈ U)) to the current goal.
Assume HxU: x ∈ U.
An exact proof term for the current goal is (UnionI CoverX x U HxU (binunionI2 Fam {U} U (SingI U))).
Assume HxnotU: ¬ x ∈ U.
We prove the intermediate claim HxY: x ∈ Y.
rewrite the current goal using HYeq (from left to right).
An exact proof term for the current goal is (setminusI X U x HxX HxnotU).
We prove the intermediate claim HxUFam: x ∈ ⋃ Fam.
An exact proof term for the current goal is (HYcovFam x HxY).
Apply (UnionE_impred Fam x HxUFam) to the current goal.
Let V be given.
Assume HxV: x ∈ V.
Assume HVF: V ∈ Fam.
We will prove x ∈ ⋃ CoverX.
An exact proof term for the current goal is (UnionI CoverX x V HxV (binunionI1 Fam {U} V HVF)).
Let V be given.
Assume HV: V ∈ CoverX.
We will prove V ∈ Tx.
Apply (binunionE Fam {U} V HV) to the current goal.
Assume HVF: V ∈ Fam.
An exact proof term for the current goal is (HFamSub V HVF).
Assume HVU: V ∈ {U}.
We prove the intermediate claim HVe: V = U.
An exact proof term for the current goal is (SingE U V HVU).
rewrite the current goal using HVe (from left to right).
An exact proof term for the current goal is HUu.
We prove the intermediate claim HfinCoverX: has_finite_subcover X Tx CoverX.
An exact proof term for the current goal is (HsubcoverX CoverX HcoverX).
Apply HfinCoverX to the current goal.
Let G be given.
Assume HG: G ⊆ CoverX ∧ finite G ∧ X ⊆ ⋃ G.
We prove the intermediate claim HGleft: G ⊆ CoverX ∧ finite G.
An exact proof term for the current goal is (andEL (G ⊆ CoverX ∧ finite G) (X ⊆ ⋃ G) HG).
We prove the intermediate claim HGsub: G ⊆ CoverX.
An exact proof term for the current goal is (andEL (G ⊆ CoverX) (finite G) HGleft).
We prove the intermediate claim HGfin: finite G.
An exact proof term for the current goal is (andER (G ⊆ CoverX) (finite G) HGleft).
We prove the intermediate claim HGcovX: X ⊆ ⋃ G.
An exact proof term for the current goal is (andER (G ⊆ CoverX ∧ finite G) (X ⊆ ⋃ G) HG).
Set G1 to be the term G ∖ {U}.
We prove the intermediate claim HG1subG: G1 ⊆ G.
An exact proof term for the current goal is (setminus_Subq G {U}).
We prove the intermediate claim HG1fin: finite G1.
An exact proof term for the current goal is (Subq_finite G HGfin G1 HG1subG).
We prove the intermediate claim HG1subFam: G1 ⊆ Fam.
Let V be given.
Assume HVG1: V ∈ G1.
We will prove V ∈ Fam.
We prove the intermediate claim HVG: V ∈ G.
An exact proof term for the current goal is (setminusE1 G {U} V HVG1).
We prove the intermediate claim HVnotU: V ∉ {U}.
An exact proof term for the current goal is (setminusE2 G {U} V HVG1).
We prove the intermediate claim HVinCover: V ∈ CoverX.
An exact proof term for the current goal is (HGsub V HVG).
Apply (binunionE Fam {U} V HVinCover) to the current goal.
Assume HVF: V ∈ Fam.
An exact proof term for the current goal is HVF.
Assume HVU: V ∈ {U}.
We will prove V ∈ Fam.
We will prove False.
Apply HVnotU to the current goal.
An exact proof term for the current goal is HVU.
We prove the intermediate claim HYcovG1: Y ⊆ ⋃ G1.
Let y be given.
Assume HyY: y ∈ Y.
We will prove y ∈ ⋃ G1.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HYsub y HyY).
We prove the intermediate claim HyUG: y ∈ ⋃ G.
An exact proof term for the current goal is (HGcovX y HyX).
Apply (UnionE_impred G y HyUG) to the current goal.
Let V be given.
Assume HyV: y ∈ V.
Assume HVG: V ∈ G.
We will prove y ∈ ⋃ G1.
We prove the intermediate claim HVinCover: V ∈ CoverX.
An exact proof term for the current goal is (HGsub V HVG).
We prove the intermediate claim HVnotU: V ∉ {U}.
Apply (binunionE Fam {U} V HVinCover) to the current goal.
Assume HVF: V ∈ Fam.
We will prove V ∉ {U}.
Assume HVU: V ∈ {U}.
We prove the intermediate claim HVe: V = U.
An exact proof term for the current goal is (SingE U V HVU).
We prove the intermediate claim HyNotU: y ∉ U.
We prove the intermediate claim HyYU: y ∈ X ∖ U.
rewrite the current goal using HYeq (from right to left) at position 1.
An exact proof term for the current goal is HyY.
An exact proof term for the current goal is (setminusE2 X U y HyYU).
Apply HyNotU to the current goal.
rewrite the current goal using HVe (from right to left).
An exact proof term for the current goal is HyV.
Assume HVU: V ∈ {U}.
We will prove V ∉ {U}.
Assume HVU2: V ∈ {U}.
We prove the intermediate claim HVe: V = U.
An exact proof term for the current goal is (SingE U V HVU2).
We prove the intermediate claim HyNotU: y ∉ U.
We prove the intermediate claim HyYU: y ∈ X ∖ U.
rewrite the current goal using HYeq (from right to left) at position 1.
An exact proof term for the current goal is HyY.
An exact proof term for the current goal is (setminusE2 X U y HyYU).
Apply HyNotU to the current goal.
rewrite the current goal using HVe (from right to left).
An exact proof term for the current goal is HyV.
We prove the intermediate claim HVG1: V ∈ G1.
An exact proof term for the current goal is (setminusI G {U} V HVG HVnotU).
An exact proof term for the current goal is (UnionI G1 y V HyV HVG1).
We prove the intermediate claim HG1left: G1 ⊆ Fam ∧ finite G1.
Apply andI to the current goal.
An exact proof term for the current goal is HG1subFam.
An exact proof term for the current goal is HG1fin.
We prove the intermediate claim HG1triple: G1 ⊆ Fam ∧ finite G1 ∧ Y ⊆ ⋃ G1.
Apply andI to the current goal.
An exact proof term for the current goal is HG1left.
An exact proof term for the current goal is HYcovG1.
An exact proof term for the current goal is (has_finite_subcoverI Y Tx Fam G1 HG1triple).
∎