We will prove closed_in unit_interval unit_interval_topology unit_interval_left_half ∧ closed_in unit_interval unit_interval_topology unit_interval_right_half.
Apply andI to the current goal.
Apply (closed_inI unit_interval unit_interval_topology unit_interval_left_half) to the current goal.
An exact proof term for the current goal is unit_interval_topology_on.
An exact proof term for the current goal is unit_interval_left_half_sub.
Set V to be the term {x ∈ R|Rlt (eps_ 1) x}.
Set U to be the term V ∩ unit_interval.
We use U to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim Hut: unit_interval_topology = subspace_topology R R_standard_topology unit_interval.
Use reflexivity.
rewrite the current goal using Hut (from left to right).
We prove the intermediate claim HUpow: U ∈ 𝒫 unit_interval.
An exact proof term for the current goal is (PowerI unit_interval U (binintersect_Subq_2 V unit_interval)).
We prove the intermediate claim Hex: ∃W ∈ R_standard_topology, U = W ∩ unit_interval.
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (open_ray_in_R_standard_topology (eps_ 1) eps_1_in_R).
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 unit_interval) (λU0 : set ⇒ ∃W ∈ R_standard_topology, U0 = W ∩ unit_interval) U HUpow Hex).
We will prove unit_interval_left_half = unit_interval ∖ U.
Apply set_ext to the current goal.
Let t be given.
Assume HtL: t ∈ unit_interval_left_half.
We will prove t ∈ unit_interval ∖ U.
Apply setminusI to the current goal.
An exact proof term for the current goal is (unit_interval_left_half_sub t HtL).
Assume HtU: t ∈ U.
We will prove False.
We prove the intermediate claim HtV: t ∈ V.
An exact proof term for the current goal is (binintersectE1 V unit_interval t HtU).
We prove the intermediate claim Hnlt: ¬ (Rlt (eps_ 1) t).
An exact proof term for the current goal is (SepE2 unit_interval (λt0 : set ⇒ ¬ (Rlt (eps_ 1) t0)) t HtL).
We prove the intermediate claim Hlt: Rlt (eps_ 1) t.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt (eps_ 1) x0) t HtV).
An exact proof term for the current goal is (Hnlt Hlt).
Let t be given.
Assume Ht: t ∈ unit_interval ∖ U.
We will prove t ∈ unit_interval_left_half.
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (setminusE1 unit_interval U t Ht).
Apply (SepI unit_interval (λt0 : set ⇒ ¬ (Rlt (eps_ 1) t0)) t HtI) to the current goal.
We will prove ¬ (Rlt (eps_ 1) t).
Assume Hlt: Rlt (eps_ 1) t.
We will prove False.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R t HtI).
We prove the intermediate claim HtV: t ∈ V.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt (eps_ 1) x0) t HtR Hlt).
We prove the intermediate claim HtU2: t ∈ U.
An exact proof term for the current goal is (binintersectI V unit_interval t HtV HtI).
We prove the intermediate claim HnotU: t ∉ U.
An exact proof term for the current goal is (setminusE2 unit_interval U t Ht).
An exact proof term for the current goal is (HnotU HtU2).
Apply (closed_inI unit_interval unit_interval_topology unit_interval_right_half) to the current goal.
An exact proof term for the current goal is unit_interval_topology_on.
An exact proof term for the current goal is unit_interval_right_half_sub.
Set V to be the term {x ∈ R|Rlt x (eps_ 1)}.
Set U to be the term V ∩ unit_interval.
We use U to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim Hut: unit_interval_topology = subspace_topology R R_standard_topology unit_interval.
Use reflexivity.
rewrite the current goal using Hut (from left to right).
We prove the intermediate claim HUpow: U ∈ 𝒫 unit_interval.
An exact proof term for the current goal is (PowerI unit_interval U (binintersect_Subq_2 V unit_interval)).
We prove the intermediate claim Hex: ∃W ∈ R_standard_topology, U = W ∩ unit_interval.
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (open_left_ray_in_R_standard_topology (eps_ 1) eps_1_in_R).
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 unit_interval) (λU0 : set ⇒ ∃W ∈ R_standard_topology, U0 = W ∩ unit_interval) U HUpow Hex).
We will prove unit_interval_right_half = unit_interval ∖ U.
Apply set_ext to the current goal.
Let t be given.
Assume HtR: t ∈ unit_interval_right_half.
We will prove t ∈ unit_interval ∖ U.
Apply setminusI to the current goal.
An exact proof term for the current goal is (unit_interval_right_half_sub t HtR).
Assume HtU: t ∈ U.
We will prove False.
We prove the intermediate claim HtV: t ∈ V.
An exact proof term for the current goal is (binintersectE1 V unit_interval t HtU).
We prove the intermediate claim Hnlt: ¬ (Rlt t (eps_ 1)).
An exact proof term for the current goal is (SepE2 unit_interval (λt0 : set ⇒ ¬ (Rlt t0 (eps_ 1))) t HtR).
We prove the intermediate claim Hlt: Rlt t (eps_ 1).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt x0 (eps_ 1)) t HtV).
An exact proof term for the current goal is (Hnlt Hlt).
Let t be given.
Assume Ht: t ∈ unit_interval ∖ U.
We will prove t ∈ unit_interval_right_half.
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (setminusE1 unit_interval U t Ht).
Apply (SepI unit_interval (λt0 : set ⇒ ¬ (Rlt t0 (eps_ 1))) t HtI) to the current goal.
We will prove ¬ (Rlt t (eps_ 1)).
Assume Hlt: Rlt t (eps_ 1).
We will prove False.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (unit_interval_sub_R t HtI).
We prove the intermediate claim HtV: t ∈ V.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt x0 (eps_ 1)) t HtR Hlt).
We prove the intermediate claim HtU2: t ∈ U.
An exact proof term for the current goal is (binintersectI V unit_interval t HtV HtI).
We prove the intermediate claim HnotU: t ∉ U.
An exact proof term for the current goal is (setminusE2 unit_interval U t Ht).
An exact proof term for the current goal is (HnotU HtU2).
∎