We will prove closed_in R R_standard_topology unit_interval ∧ compact_space unit_interval unit_interval_topology.
Apply andI to the current goal.
We will prove closed_in R R_standard_topology unit_interval.
We prove the intermediate claim HT: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We will prove topology_on R R_standard_topology ∧ (unit_interval ⊆ R ∧ ∃U ∈ R_standard_topology, unit_interval = R ∖ U).
Apply andI to the current goal.
An exact proof term for the current goal is HT.
Apply andI to the current goal.
Let x be given.
Assume Hx: x ∈ unit_interval.
We will prove x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) x Hx).
Set L0 to be the term {x ∈ R|Rlt x 0}.
Set R1 to be the term {x ∈ R|Rlt 1 x}.
Set U to be the term L0 ∪ R1.
We use U to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HL0: L0 ∈ R_standard_topology.
An exact proof term for the current goal is (open_left_ray_in_R_standard_topology 0 real_0).
We prove the intermediate claim HR1: R1 ∈ R_standard_topology.
An exact proof term for the current goal is (open_ray_in_R_standard_topology 1 real_1).
An exact proof term for the current goal is (topology_binunion_closed R R_standard_topology L0 R1 HT HL0 HR1).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ unit_interval.
We will prove x ∈ R ∖ U.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) x Hx).
We prove the intermediate claim Hxprop: ¬ (Rlt x 0) ∧ ¬ (Rlt 1 x).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) x Hx).
We prove the intermediate claim Hnx0: ¬ (Rlt x 0).
An exact proof term for the current goal is (andEL (¬ (Rlt x 0)) (¬ (Rlt 1 x)) Hxprop).
We prove the intermediate claim Hn1x: ¬ (Rlt 1 x).
An exact proof term for the current goal is (andER (¬ (Rlt x 0)) (¬ (Rlt 1 x)) Hxprop).
Apply (setminusI R U x HxR) to the current goal.
Assume Hxu: x ∈ U.
Apply (binunionE L0 R1 x Hxu) to the current goal.
Assume HxL: x ∈ L0.
We prove the intermediate claim Hlt: Rlt x 0.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt x0 0) x HxL).
An exact proof term for the current goal is (Hnx0 Hlt).
Assume HxR1: x ∈ R1.
We prove the intermediate claim Hlt: Rlt 1 x.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt 1 x0) x HxR1).
An exact proof term for the current goal is (Hn1x Hlt).
Let x be given.
Assume Hx: x ∈ R ∖ U.
We will prove x ∈ unit_interval.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (setminusE1 R U x Hx).
We prove the intermediate claim HxnotU: x ∉ U.
An exact proof term for the current goal is (setminusE2 R U x Hx).
Apply (SepI R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) x HxR) to the current goal.
Apply andI to the current goal.
Assume Hlt: Rlt x 0.
We will prove False.
We prove the intermediate claim HxL0: x ∈ L0.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt x0 0) x HxR Hlt).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binunionI1 L0 R1 x HxL0).
An exact proof term for the current goal is (HxnotU HxU).
Assume Hlt: Rlt 1 x.
We will prove False.
We prove the intermediate claim HxR1: x ∈ R1.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt 1 x0) x HxR Hlt).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binunionI2 L0 R1 x HxR1).
An exact proof term for the current goal is (HxnotU HxU).
An exact proof term for the current goal is unit_interval_compact_axiom.
∎