Let X and Tx be given.
Assume HTx: topology_on X Tx.
We will prove compact_space Empty (subspace_topology X Tx Empty).
We will prove topology_on Empty (subspace_topology X Tx Empty) ∧ ∀Fam : set, open_cover_of Empty (subspace_topology X Tx Empty) Fam → has_finite_subcover Empty (subspace_topology X Tx Empty) Fam.
Apply andI to the current goal.
An exact proof term for the current goal is (subspace_topology_is_topology X Tx Empty HTx (Subq_Empty X)).
Let Fam be given.
Assume HFam: open_cover_of Empty (subspace_topology X Tx Empty) Fam.
Apply (has_finite_subcoverI Empty (subspace_topology X Tx Empty) Fam Empty) 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 (Subq_Empty Fam).
An exact proof term for the current goal is finite_Empty.
An exact proof term for the current goal is (Subq_Empty (⋃ Empty)).
∎