We will prove compact_space unit_interval unit_interval_topology.

We will prove topology_on unit_interval unit_interval_topology ∧ ∀Fam : set, open_cover_of unit_interval unit_interval_topology Fam → has_finite_subcover unit_interval unit_interval_topology Fam.

Apply andI to the current goal.

An exact proof term for the current goal is unit_interval_topology_on.

Let Fam be given.

Assume Hcover: open_cover_of unit_interval unit_interval_topology Fam.

We will prove has_finite_subcover unit_interval unit_interval_topology Fam.

An exact proof term for the current goal is (unit_interval_has_finite_subcover Fam Hcover).

∎