Let X and d be given.
Assume Hd: metric_on X d.
We will prove (compact_space X (metric_topology X d) ↔ sequentially_compact X (metric_topology X d)).
Apply iffI to the current goal.
Assume Hcomp: compact_space X (metric_topology X d).
We will prove sequentially_compact X (metric_topology X d).
We will prove topology_on X (metric_topology X d) ∧ ∀seq : set, sequence_on seq X → ∃subseq : set, ∃x : set, subsequence_of seq subseq ∧ converges_to X (metric_topology X d) subseq x.
Apply andI to the current goal.
An exact proof term for the current goal is (compact_space_topology X (metric_topology X d) Hcomp).
Let seq be given.
Assume Hseq: sequence_on seq X.
An exact proof term for the current goal is (compact_metric_sequence_has_convergent_subsequence X d seq Hd Hcomp Hseq).
Assume Hseqc: sequentially_compact X (metric_topology X d).
We will prove compact_space X (metric_topology X d).
An exact proof term for the current goal is (sequentially_compact_metric_imp_compact X d Hd Hseqc).
∎