Let m be given.
We will prove T1_space (euclidean_space m) (euclidean_topology m).
We prove the intermediate claim HH: Hausdorff_space (euclidean_space m) (euclidean_topology m).
An exact proof term for the current goal is (euclidean_space_Hausdorff m).
We prove the intermediate claim Htop: topology_on (euclidean_space m) (euclidean_topology m).
An exact proof term for the current goal is (andEL (topology_on (euclidean_space m) (euclidean_topology m)) (∀x1 x2 : set, x1 ∈ euclidean_space m → x2 ∈ euclidean_space m → x1 ≠ x2 → ∃U V : set, U ∈ euclidean_topology m ∧ V ∈ euclidean_topology m ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty) HH).
We will prove topology_on (euclidean_space m) (euclidean_topology m) ∧ ∀F : set, F ⊆ euclidean_space m → finite F → closed_in (euclidean_space m) (euclidean_topology m) F.
Apply andI to the current goal.
An exact proof term for the current goal is Htop.
Let F be given.
Assume HFsub: F ⊆ euclidean_space m.
Assume HFfin: finite F.
An exact proof term for the current goal is (finite_sets_closed_in_Hausdorff (euclidean_space m) (euclidean_topology m) HH F HFsub HFfin).
∎