Let X and Tx be given.
Assume HTx: topology_on X Tx.
We will prove compact_space X Tx ↔ ∀N : set, net_pack_in_space X N → ∃S x : set, subnet_pack_of_in X N S ∧ net_pack_converges X Tx S x.
Apply iffI to the current goal.
Assume Hcomp: compact_space X Tx.
We will prove ∀N : set, net_pack_in_space X N → ∃S x : set, subnet_pack_of_in X N S ∧ net_pack_converges X Tx S x.
Let N be given.
Assume HN: net_pack_in_space X N.
An exact proof term for the current goal is (compact_space_implies_every_net_pack_has_convergent_subnet_pack X Tx Hcomp N HN).
Assume Hnets: ∀N : set, net_pack_in_space X N → ∃S x : set, subnet_pack_of_in X N S ∧ net_pack_converges X Tx S x.
An exact proof term for the current goal is (compact_space_of_every_net_pack_has_convergent_subnet_pack X Tx HTx Hnets).
∎