Apply andI to the current goal.

We will prove topology_on unit_interval unit_interval_topology ∧ ∀x0 : set, x0 ∈ unit_interval → closed_in unit_interval unit_interval_topology {x0}.

Apply andI to the current goal.

An exact proof term for the current goal is unit_interval_topology_on.

Let x0 be given.

Assume Hx0I: x0 ∈ unit_interval.

An exact proof term for the current goal is (Hausdorff_singletons_closed unit_interval unit_interval_topology x0 HH Hx0I).

Let x be given.

Assume HxI: x ∈ unit_interval.

Let F be given.

Assume HFcl: closed_in unit_interval unit_interval_topology F.

Assume HxnotF: x ∉ F.

We will prove ∃f : set, continuous_map unit_interval unit_interval_topology R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1.

We prove the intermediate claim Hcomp: compact_space unit_interval unit_interval_topology.

An exact proof term for the current goal is unit_interval_compact_axiom.

We prove the intermediate claim Hnorm: normal_space unit_interval unit_interval_topology.

An exact proof term for the current goal is (compact_Hausdorff_normal unit_interval unit_interval_topology Hcomp HH).

We prove the intermediate claim Hxcl: closed_in unit_interval unit_interval_topology {x}.

An exact proof term for the current goal is (Hausdorff_singletons_closed unit_interval unit_interval_topology x HH HxI).

We prove the intermediate claim H0le1: Rle 0 1.

An exact proof term for the current goal is (Rlt_implies_Rle 0 1 Rlt_0_1).

We prove the intermediate claim Hdisj: {x} ∩ F = Empty.

Apply set_ext to the current goal.

Let z be given.

Assume Hz: z ∈ {x} ∩ F.

We will prove z ∈ Empty.

We prove the intermediate claim HzSing: z ∈ {x}.

An exact proof term for the current goal is (binintersectE1 {x} F z Hz).

We prove the intermediate claim HzF: z ∈ F.

An exact proof term for the current goal is (binintersectE2 {x} F z Hz).

We prove the intermediate claim HzEq: z = x.

An exact proof term for the current goal is (SingE x z HzSing).

We prove the intermediate claim HxF: x ∈ F.

rewrite the current goal using HzEq (from right to left).

An exact proof term for the current goal is HzF.

We prove the intermediate claim Hcontra: False.

An exact proof term for the current goal is (HxnotF HxF).

An exact proof term for the current goal is (FalseE Hcontra (z ∈ Empty)).

Let z be given.

Assume Hz: z ∈ Empty.

We will prove z ∈ {x} ∩ F.

An exact proof term for the current goal is (EmptyE z Hz (z ∈ {x} ∩ F)).

Apply (Urysohn_lemma unit_interval unit_interval_topology {x} F 0 1 H0le1 Hnorm Hxcl HFcl Hdisj) to the current goal.

Let f be given.

Assume Hfpack: continuous_map unit_interval unit_interval_topology (closed_interval 0 1) (closed_interval_topology 0 1) f ∧ (∀u : set, u ∈ {x} → apply_fun f u = 0) ∧ (∀y : set, y ∈ F → apply_fun f y = 1).

We use f to witness the existential quantifier.

We will prove continuous_map unit_interval unit_interval_topology R R_standard_topology f ∧ apply_fun f x = 0 ∧ ∀y : set, y ∈ F → apply_fun f y = 1.

We prove the intermediate claim Hpair1: continuous_map unit_interval unit_interval_topology (closed_interval 0 1) (closed_interval_topology 0 1) f ∧ (∀u : set, u ∈ {x} → apply_fun f u = 0).

An exact proof term for the current goal is (andEL (continuous_map unit_interval unit_interval_topology (closed_interval 0 1) (closed_interval_topology 0 1) f ∧ (∀u : set, u ∈ {x} → apply_fun f u = 0)) (∀y : set, y ∈ F → apply_fun f y = 1) Hfpack).

We prove the intermediate claim HcontI: continuous_map unit_interval unit_interval_topology (closed_interval 0 1) (closed_interval_topology 0 1) f.

An exact proof term for the current goal is (andEL (continuous_map unit_interval unit_interval_topology (closed_interval 0 1) (closed_interval_topology 0 1) f) (∀u : set, u ∈ {x} → apply_fun f u = 0) Hpair1).

We prove the intermediate claim HAx: ∀u : set, u ∈ {x} → apply_fun f u = 0.

An exact proof term for the current goal is (andER (continuous_map unit_interval unit_interval_topology (closed_interval 0 1) (closed_interval_topology 0 1) f) (∀u : set, u ∈ {x} → apply_fun f u = 0) Hpair1).

We prove the intermediate claim Hfx0: apply_fun f x = 0.

An exact proof term for the current goal is (HAx x (SingI x)).

We prove the intermediate claim HfF1: ∀y : set, y ∈ F → apply_fun f y = 1.

An exact proof term for the current goal is (andER (continuous_map unit_interval unit_interval_topology (closed_interval 0 1) (closed_interval_topology 0 1) f ∧ (∀u : set, u ∈ {x} → apply_fun f u = 0)) (∀y : set, y ∈ F → apply_fun f y = 1) Hfpack).

We prove the intermediate claim HISubR: closed_interval 0 1 ⊆ R.

An exact proof term for the current goal is (closed_interval_sub_R 0 1).

We prove the intermediate claim HTIeq: closed_interval_topology 0 1 = subspace_topology R R_standard_topology (closed_interval 0 1).

Use reflexivity.

We prove the intermediate claim HcontR: continuous_map unit_interval unit_interval_topology R R_standard_topology f.

An exact proof term for the current goal is (continuous_map_range_expand unit_interval unit_interval_topology (closed_interval 0 1) (closed_interval_topology 0 1) R R_standard_topology f HcontI HISubR R_standard_topology_is_topology HTIeq).

Apply andI to the current goal.

We will prove continuous_map unit_interval unit_interval_topology R R_standard_topology f ∧ apply_fun f x = 0.

Apply andI to the current goal.

An exact proof term for the current goal is HcontR.

An exact proof term for the current goal is Hfx0.

An exact proof term for the current goal is HfF1.