We will prove continuous_map unit_interval unit_interval_topology unit_interval unit_interval_topology flip_unit_interval.
Set Tx to be the term unit_interval_topology.
We prove the intermediate claim HcontR: continuous_map unit_interval Tx R R_standard_topology flip_unit_interval.
Set S to be the term open_rays_subbasis R.
We prove the intermediate claim HTx: topology_on unit_interval Tx.
An exact proof term for the current goal is unit_interval_topology_on.
We prove the intermediate claim HfunR: function_on flip_unit_interval unit_interval R.
Let t be given.
Assume Ht: t ∈ unit_interval.
An exact proof term for the current goal is (flip_unit_interval_in_R t Ht).
We prove the intermediate claim HS: subbasis_on R S.
An exact proof term for the current goal is (open_rays_subbasis_is_subbasis R).
We prove the intermediate claim Hgen: generated_topology_from_subbasis R S = R_standard_topology.
rewrite the current goal using open_rays_subbasis_for_order_topology_R (from left to right).
rewrite the current goal using standard_topology_is_order_topology (from left to right).
Use reflexivity.
rewrite the current goal using Hgen (from right to left).
We prove the intermediate claim Hflip_upper: ∀a t : set, a ∈ R → t ∈ R → (Rlt a (add_SNo 1 (minus_SNo t)) ↔ Rlt t (add_SNo 1 (minus_SNo a))).
Let a and t be given.
Assume HaR: a ∈ R.
Assume HtR: t ∈ R.
We will prove (Rlt a (add_SNo 1 (minus_SNo t)) ↔ Rlt t (add_SNo 1 (minus_SNo a))).
Apply iffI to the current goal.
Assume Hlt: Rlt a (add_SNo 1 (minus_SNo t)).
We will prove Rlt t (add_SNo 1 (minus_SNo a)).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HmaS: SNo (minus_SNo a).
An exact proof term for the current goal is (SNo_minus_SNo a HaS).
We prove the intermediate claim HmtS: SNo (minus_SNo t).
An exact proof term for the current goal is (SNo_minus_SNo t HtS).
We prove the intermediate claim HsumS: SNo (add_SNo 1 (minus_SNo t)).
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo t) SNo_1 HmtS).
We prove the intermediate claim HltS: a < add_SNo 1 (minus_SNo t).
An exact proof term for the current goal is (RltE_lt a (add_SNo 1 (minus_SNo t)) Hlt).
We prove the intermediate claim H1: add_SNo a t < add_SNo (add_SNo 1 (minus_SNo t)) t.
An exact proof term for the current goal is (add_SNo_Lt1 a t (add_SNo 1 (minus_SNo t)) HaS HtS HsumS HltS).
We prove the intermediate claim HeqR: add_SNo (add_SNo 1 (minus_SNo t)) t = 1.
rewrite the current goal using (add_SNo_assoc 1 (minus_SNo t) t SNo_1 HmtS HtS) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_linv t HtS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R 1 SNo_1).
We prove the intermediate claim H2: add_SNo a t < 1.
rewrite the current goal using HeqR (from right to left).
An exact proof term for the current goal is H1.
We prove the intermediate claim H2c: add_SNo t a < 1.
rewrite the current goal using (add_SNo_com t a HtS HaS) (from left to right).
An exact proof term for the current goal is H2.
We prove the intermediate claim Hm1S: SNo (minus_SNo a).
An exact proof term for the current goal is HmaS.
We prove the intermediate claim H3: add_SNo (add_SNo t a) (minus_SNo a) < add_SNo 1 (minus_SNo a).
An exact proof term for the current goal is (add_SNo_Lt1 (add_SNo t a) (minus_SNo a) 1 (SNo_add_SNo t a HtS HaS) Hm1S SNo_1 H2c).
We prove the intermediate claim HeqL: add_SNo (add_SNo t a) (minus_SNo a) = t.
rewrite the current goal using (add_SNo_assoc t a (minus_SNo a) HtS HaS Hm1S) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv a HaS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R t HtS).
We prove the intermediate claim H4: t < add_SNo 1 (minus_SNo a).
rewrite the current goal using HeqL (from right to left) at position 1.
An exact proof term for the current goal is H3.
We prove the intermediate claim Hflip_aR: add_SNo 1 (minus_SNo a) ∈ R.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from left to right).
We prove the intermediate claim HaReal: a ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HaR.
We prove the intermediate claim HmaReal: (minus_SNo a) ∈ real.
An exact proof term for the current goal is (real_minus_SNo a HaReal).
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo a) HmaReal).
An exact proof term for the current goal is (RltI t (add_SNo 1 (minus_SNo a)) HtR Hflip_aR H4).
Assume Hlt: Rlt t (add_SNo 1 (minus_SNo a)).
We will prove Rlt a (add_SNo 1 (minus_SNo t)).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HmaS: SNo (minus_SNo a).
An exact proof term for the current goal is (SNo_minus_SNo a HaS).
We prove the intermediate claim HmtS: SNo (minus_SNo t).
An exact proof term for the current goal is (SNo_minus_SNo t HtS).
We prove the intermediate claim Hflip_aS: SNo (add_SNo 1 (minus_SNo a)).
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo a) SNo_1 HmaS).
We prove the intermediate claim HltS: t < add_SNo 1 (minus_SNo a).
An exact proof term for the current goal is (RltE_lt t (add_SNo 1 (minus_SNo a)) Hlt).
We prove the intermediate claim H1: add_SNo t a < add_SNo (add_SNo 1 (minus_SNo a)) a.
An exact proof term for the current goal is (add_SNo_Lt1 t a (add_SNo 1 (minus_SNo a)) HtS HaS Hflip_aS HltS).
We prove the intermediate claim HeqR: add_SNo (add_SNo 1 (minus_SNo a)) a = 1.
rewrite the current goal using (add_SNo_assoc 1 (minus_SNo a) a SNo_1 HmaS HaS) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_linv a HaS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R 1 SNo_1).
We prove the intermediate claim H2: add_SNo t a < 1.
rewrite the current goal using HeqR (from right to left).
An exact proof term for the current goal is H1.
We prove the intermediate claim H2c: add_SNo a t < 1.
rewrite the current goal using (add_SNo_com a t HaS HtS) (from left to right).
An exact proof term for the current goal is H2.
We prove the intermediate claim Hm1S: SNo (minus_SNo t).
An exact proof term for the current goal is HmtS.
We prove the intermediate claim H3: add_SNo (add_SNo a t) (minus_SNo t) < add_SNo 1 (minus_SNo t).
An exact proof term for the current goal is (add_SNo_Lt1 (add_SNo a t) (minus_SNo t) 1 (SNo_add_SNo a t HaS HtS) Hm1S SNo_1 H2c).
We prove the intermediate claim HeqL: add_SNo (add_SNo a t) (minus_SNo t) = a.
rewrite the current goal using (add_SNo_assoc a t (minus_SNo t) HaS HtS Hm1S) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv t HtS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R a HaS).
We prove the intermediate claim H4: a < add_SNo 1 (minus_SNo t).
rewrite the current goal using HeqL (from right to left) at position 1.
An exact proof term for the current goal is H3.
We prove the intermediate claim Hflip_tR: add_SNo 1 (minus_SNo t) ∈ R.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from left to right).
We prove the intermediate claim HtReal: t ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HtR.
We prove the intermediate claim HmtReal: (minus_SNo t) ∈ real.
An exact proof term for the current goal is (real_minus_SNo t HtReal).
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo t) HmtReal).
An exact proof term for the current goal is (RltI a (add_SNo 1 (minus_SNo t)) HaR Hflip_tR H4).
We prove the intermediate claim Hflip_lower: ∀t b : set, t ∈ R → b ∈ R → (Rlt (add_SNo 1 (minus_SNo t)) b ↔ Rlt (add_SNo 1 (minus_SNo b)) t).
Let t and b be given.
Assume HtR: t ∈ R.
Assume HbR: b ∈ R.
We will prove (Rlt (add_SNo 1 (minus_SNo t)) b ↔ Rlt (add_SNo 1 (minus_SNo b)) t).
Apply iffI to the current goal.
Assume Hlt: Rlt (add_SNo 1 (minus_SNo t)) b.
We will prove Rlt (add_SNo 1 (minus_SNo b)) t.
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim HmtS: SNo (minus_SNo t).
An exact proof term for the current goal is (SNo_minus_SNo t HtS).
We prove the intermediate claim HmbS: SNo (minus_SNo b).
An exact proof term for the current goal is (SNo_minus_SNo b HbS).
We prove the intermediate claim HsumS: SNo (add_SNo 1 (minus_SNo t)).
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo t) SNo_1 HmtS).
We prove the intermediate claim HltS: add_SNo 1 (minus_SNo t) < b.
An exact proof term for the current goal is (RltE_lt (add_SNo 1 (minus_SNo t)) b Hlt).
We prove the intermediate claim H1: add_SNo (add_SNo 1 (minus_SNo t)) t < add_SNo b t.
An exact proof term for the current goal is (add_SNo_Lt1 (add_SNo 1 (minus_SNo t)) t b HsumS HtS HbS HltS).
We prove the intermediate claim HeqL: add_SNo (add_SNo 1 (minus_SNo t)) t = 1.
rewrite the current goal using (add_SNo_assoc 1 (minus_SNo t) t SNo_1 HmtS HtS) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_linv t HtS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R 1 SNo_1).
We prove the intermediate claim H2: 1 < add_SNo b t.
rewrite the current goal using HeqL (from right to left) at position 1.
An exact proof term for the current goal is H1.
We prove the intermediate claim H2c: 1 < add_SNo t b.
rewrite the current goal using (add_SNo_com b t HbS HtS) (from right to left).
An exact proof term for the current goal is H2.
We prove the intermediate claim Hm1S: SNo (minus_SNo b).
An exact proof term for the current goal is HmbS.
We prove the intermediate claim H3: add_SNo 1 (minus_SNo b) < add_SNo (add_SNo t b) (minus_SNo b).
An exact proof term for the current goal is (add_SNo_Lt1 1 (minus_SNo b) (add_SNo t b) SNo_1 Hm1S (SNo_add_SNo t b HtS HbS) H2c).
We prove the intermediate claim HeqR: add_SNo (add_SNo t b) (minus_SNo b) = t.
rewrite the current goal using (add_SNo_assoc t b (minus_SNo b) HtS HbS Hm1S) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv b HbS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R t HtS).
We prove the intermediate claim H4: add_SNo 1 (minus_SNo b) < t.
rewrite the current goal using HeqR (from right to left).
An exact proof term for the current goal is H3.
We prove the intermediate claim Hflip_bR: add_SNo 1 (minus_SNo b) ∈ R.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from left to right).
We prove the intermediate claim HbReal: b ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HbR.
We prove the intermediate claim HmbReal: (minus_SNo b) ∈ real.
An exact proof term for the current goal is (real_minus_SNo b HbReal).
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo b) HmbReal).
An exact proof term for the current goal is (RltI (add_SNo 1 (minus_SNo b)) t Hflip_bR HtR H4).
Assume Hlt: Rlt (add_SNo 1 (minus_SNo b)) t.
We will prove Rlt (add_SNo 1 (minus_SNo t)) b.
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim HmtS: SNo (minus_SNo t).
An exact proof term for the current goal is (SNo_minus_SNo t HtS).
We prove the intermediate claim HmbS: SNo (minus_SNo b).
An exact proof term for the current goal is (SNo_minus_SNo b HbS).
We prove the intermediate claim HsumS: SNo (add_SNo 1 (minus_SNo b)).
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo b) SNo_1 HmbS).
We prove the intermediate claim HltS: add_SNo 1 (minus_SNo b) < t.
An exact proof term for the current goal is (RltE_lt (add_SNo 1 (minus_SNo b)) t Hlt).
We prove the intermediate claim H1: add_SNo (add_SNo 1 (minus_SNo b)) b < add_SNo t b.
An exact proof term for the current goal is (add_SNo_Lt1 (add_SNo 1 (minus_SNo b)) b t HsumS HbS HtS HltS).
We prove the intermediate claim HeqL: add_SNo (add_SNo 1 (minus_SNo b)) b = 1.
rewrite the current goal using (add_SNo_assoc 1 (minus_SNo b) b SNo_1 HmbS HbS) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_linv b HbS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R 1 SNo_1).
We prove the intermediate claim H2: 1 < add_SNo t b.
rewrite the current goal using HeqL (from right to left) at position 1.
An exact proof term for the current goal is H1.
We prove the intermediate claim H2c: 1 < add_SNo b t.
rewrite the current goal using (add_SNo_com t b HtS HbS) (from right to left).
An exact proof term for the current goal is H2.
We prove the intermediate claim Hm1S: SNo (minus_SNo t).
An exact proof term for the current goal is HmtS.
We prove the intermediate claim H3: add_SNo 1 (minus_SNo t) < add_SNo (add_SNo b t) (minus_SNo t).
An exact proof term for the current goal is (add_SNo_Lt1 1 (minus_SNo t) (add_SNo b t) SNo_1 Hm1S (SNo_add_SNo b t HbS HtS) H2c).
We prove the intermediate claim HeqR: add_SNo (add_SNo b t) (minus_SNo t) = b.
rewrite the current goal using (add_SNo_assoc b t (minus_SNo t) HbS HtS Hm1S) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv t HtS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R b HbS).
We prove the intermediate claim H4: add_SNo 1 (minus_SNo t) < b.
rewrite the current goal using HeqR (from right to left).
An exact proof term for the current goal is H3.
We prove the intermediate claim Hflip_tR: add_SNo 1 (minus_SNo t) ∈ R.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from left to right).
We prove the intermediate claim HtReal: t ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HtR.
We prove the intermediate claim HmtReal: (minus_SNo t) ∈ real.
An exact proof term for the current goal is (real_minus_SNo t HtReal).
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo t) HmtReal).
An exact proof term for the current goal is (RltI (add_SNo 1 (minus_SNo t)) b Hflip_tR HbR H4).
We prove the intermediate claim HpreS: ∀s : set, s ∈ S → preimage_of unit_interval flip_unit_interval s ∈ Tx.
Let s be given.
Assume HsS: s ∈ S.
We will prove preimage_of unit_interval flip_unit_interval s ∈ Tx.
Apply (binunionE' ({I ∈ 𝒫 R|∃a ∈ R, I = open_ray_upper R a} ∪ {I ∈ 𝒫 R|∃b ∈ R, I = open_ray_lower R b}) {R} s (preimage_of unit_interval flip_unit_interval s ∈ Tx)) to the current goal.
Assume Hs0: s ∈ ({I ∈ 𝒫 R|∃a ∈ R, I = open_ray_upper R a} ∪ {I ∈ 𝒫 R|∃b ∈ R, I = open_ray_lower R b}).
Apply (binunionE' {I ∈ 𝒫 R|∃a ∈ R, I = open_ray_upper R a} {I ∈ 𝒫 R|∃b ∈ R, I = open_ray_lower R b} s (preimage_of unit_interval flip_unit_interval s ∈ Tx)) to the current goal.
Assume Hsu: s ∈ {I ∈ 𝒫 R|∃a ∈ R, I = open_ray_upper R a}.
We prove the intermediate claim Hex: ∃a ∈ R, s = open_ray_upper R a.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λI0 : set ⇒ ∃a ∈ R, I0 = open_ray_upper R a) s Hsu).
Apply Hex to the current goal.
Let a be given.
Assume Hcore.
Apply Hcore to the current goal.
Assume HaR: a ∈ R.
Assume Hseq: s = open_ray_upper R a.
rewrite the current goal using Hseq (from left to right).
Set c to be the term add_SNo 1 (minus_SNo a).
We prove the intermediate claim HcR: c ∈ R.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from left to right).
We prove the intermediate claim HaReal: a ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HaR.
We prove the intermediate claim HmaReal: (minus_SNo a) ∈ real.
An exact proof term for the current goal is (real_minus_SNo a HaReal).
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo a) HmaReal).
We prove the intermediate claim HpreEq: preimage_of unit_interval flip_unit_interval (open_ray_upper R a) = (open_ray_lower R c) ∩ unit_interval.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ preimage_of unit_interval flip_unit_interval (open_ray_upper R a).
We will prove t ∈ (open_ray_lower R c) ∩ unit_interval.
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (SepE1 unit_interval (λu : set ⇒ apply_fun flip_unit_interval u ∈ open_ray_upper R a) t Ht).
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 Himg: apply_fun flip_unit_interval t ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepE2 unit_interval (λu : set ⇒ apply_fun flip_unit_interval u ∈ open_ray_upper R a) t Ht).
We prove the intermediate claim Hrel: order_rel R a (apply_fun flip_unit_interval t).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R a x0) (apply_fun flip_unit_interval t) Himg).
We prove the intermediate claim Hrlt: Rlt a (apply_fun flip_unit_interval t).
An exact proof term for the current goal is (order_rel_R_implies_Rlt a (apply_fun flip_unit_interval t) Hrel).
We prove the intermediate claim Hrlt2: Rlt a (add_SNo 1 (minus_SNo t)).
rewrite the current goal using (flip_unit_interval_apply t HtI) (from right to left).
An exact proof term for the current goal is Hrlt.
We prove the intermediate claim Hrlt3: Rlt t c.
An exact proof term for the current goal is (iffEL (Rlt a (add_SNo 1 (minus_SNo t))) (Rlt t (add_SNo 1 (minus_SNo a))) (Hflip_upper a t HaR HtR) Hrlt2).
We prove the intermediate claim Hrel2: order_rel R t c.
An exact proof term for the current goal is (Rlt_implies_order_rel_R t c Hrlt3).
We prove the intermediate claim HtRay: t ∈ open_ray_lower R c.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R x0 c) t HtR Hrel2).
An exact proof term for the current goal is (binintersectI (open_ray_lower R c) unit_interval t HtRay HtI).
Let t be given.
Assume Ht: t ∈ (open_ray_lower R c) ∩ unit_interval.
We will prove t ∈ preimage_of unit_interval flip_unit_interval (open_ray_upper R a).
We prove the intermediate claim HtRay: t ∈ open_ray_lower R c.
An exact proof term for the current goal is (binintersectE1 (open_ray_lower R c) unit_interval t Ht).
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (binintersectE2 (open_ray_lower R c) unit_interval t Ht).
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 Hrel: order_rel R t c.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 c) t HtRay).
We prove the intermediate claim Hrlt: Rlt t c.
An exact proof term for the current goal is (order_rel_R_implies_Rlt t c Hrel).
We prove the intermediate claim Hrlt2: Rlt a (add_SNo 1 (minus_SNo t)).
An exact proof term for the current goal is (iffER (Rlt a (add_SNo 1 (minus_SNo t))) (Rlt t (add_SNo 1 (minus_SNo a))) (Hflip_upper a t HaR HtR) Hrlt).
We prove the intermediate claim Hrlt3: Rlt a (apply_fun flip_unit_interval t).
rewrite the current goal using (flip_unit_interval_apply t HtI) (from left to right).
An exact proof term for the current goal is Hrlt2.
We prove the intermediate claim Hrel2: order_rel R a (apply_fun flip_unit_interval t).
An exact proof term for the current goal is (Rlt_implies_order_rel_R a (apply_fun flip_unit_interval t) Hrlt3).
We prove the intermediate claim HimgR: apply_fun flip_unit_interval t ∈ R.
An exact proof term for the current goal is (HfunR t HtI).
We prove the intermediate claim Himg: apply_fun flip_unit_interval t ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R a x0) (apply_fun flip_unit_interval t) HimgR Hrel2).
An exact proof term for the current goal is (SepI unit_interval (λu : set ⇒ apply_fun flip_unit_interval u ∈ open_ray_upper R a) t HtI Himg).
rewrite the current goal using HpreEq (from left to right).
Set Z0 to be the term open_ray_lower R c.
We prove the intermediate claim HZ0open: Z0 ∈ R_standard_topology.
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: Z0 ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis R c HcR).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R Z0 HsRay).
We prove the intermediate claim HZ0cap: Z0 ∩ unit_interval ∈ Tx.
We will prove Z0 ∩ unit_interval ∈ {W ∈ 𝒫 unit_interval|∃Z ∈ R_standard_topology, W = Z ∩ unit_interval}.
We prove the intermediate claim Hpow: Z0 ∩ unit_interval ∈ 𝒫 unit_interval.
Apply PowerI to the current goal.
Let t be given.
Assume Ht: t ∈ Z0 ∩ unit_interval.
An exact proof term for the current goal is (binintersectE2 Z0 unit_interval t Ht).
We prove the intermediate claim Hex: ∃Z ∈ R_standard_topology, Z0 ∩ unit_interval = Z ∩ unit_interval.
We use Z0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HZ0open.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 unit_interval) (λW0 : set ⇒ ∃Z ∈ R_standard_topology, W0 = Z ∩ unit_interval) (Z0 ∩ unit_interval) Hpow Hex).
An exact proof term for the current goal is HZ0cap.
Assume Hsl: s ∈ {I ∈ 𝒫 R|∃b ∈ R, I = open_ray_lower R b}.
We prove the intermediate claim Hex: ∃b ∈ R, s = open_ray_lower R b.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λI0 : set ⇒ ∃b ∈ R, I0 = open_ray_lower R b) s Hsl).
Apply Hex to the current goal.
Let b be given.
Assume Hcore.
Apply Hcore to the current goal.
Assume HbR: b ∈ R.
Assume Hseq: s = open_ray_lower R b.
rewrite the current goal using Hseq (from left to right).
Set c to be the term add_SNo 1 (minus_SNo b).
We prove the intermediate claim HcR: c ∈ R.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from left to right).
We prove the intermediate claim HbReal: b ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HbR.
We prove the intermediate claim HmbReal: (minus_SNo b) ∈ real.
An exact proof term for the current goal is (real_minus_SNo b HbReal).
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo b) HmbReal).
We prove the intermediate claim HpreEq: preimage_of unit_interval flip_unit_interval (open_ray_lower R b) = (open_ray_upper R c) ∩ unit_interval.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ preimage_of unit_interval flip_unit_interval (open_ray_lower R b).
We will prove t ∈ (open_ray_upper R c) ∩ unit_interval.
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (SepE1 unit_interval (λu : set ⇒ apply_fun flip_unit_interval u ∈ open_ray_lower R b) t Ht).
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 Himg: apply_fun flip_unit_interval t ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepE2 unit_interval (λu : set ⇒ apply_fun flip_unit_interval u ∈ open_ray_lower R b) t Ht).
We prove the intermediate claim Hrel: order_rel R (apply_fun flip_unit_interval t) b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 b) (apply_fun flip_unit_interval t) Himg).
We prove the intermediate claim Hrlt: Rlt (apply_fun flip_unit_interval t) b.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun flip_unit_interval t) b Hrel).
We prove the intermediate claim Hrlt2: Rlt (add_SNo 1 (minus_SNo t)) b.
rewrite the current goal using (flip_unit_interval_apply t HtI) (from right to left).
An exact proof term for the current goal is Hrlt.
We prove the intermediate claim Hrlt3: Rlt c t.
An exact proof term for the current goal is (iffEL (Rlt (add_SNo 1 (minus_SNo t)) b) (Rlt (add_SNo 1 (minus_SNo b)) t) (Hflip_lower t b HtR HbR) Hrlt2).
We prove the intermediate claim Hrel2: order_rel R c t.
An exact proof term for the current goal is (Rlt_implies_order_rel_R c t Hrlt3).
We prove the intermediate claim HtRay: t ∈ open_ray_upper R c.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R c x0) t HtR Hrel2).
An exact proof term for the current goal is (binintersectI (open_ray_upper R c) unit_interval t HtRay HtI).
Let t be given.
Assume Ht: t ∈ (open_ray_upper R c) ∩ unit_interval.
We will prove t ∈ preimage_of unit_interval flip_unit_interval (open_ray_lower R b).
We prove the intermediate claim HtRay: t ∈ open_ray_upper R c.
An exact proof term for the current goal is (binintersectE1 (open_ray_upper R c) unit_interval t Ht).
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (binintersectE2 (open_ray_upper R c) unit_interval t Ht).
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 Hrel: order_rel R c t.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R c x0) t HtRay).
We prove the intermediate claim Hrlt: Rlt c t.
An exact proof term for the current goal is (order_rel_R_implies_Rlt c t Hrel).
We prove the intermediate claim Hrlt2: Rlt (add_SNo 1 (minus_SNo t)) b.
An exact proof term for the current goal is (iffER (Rlt (add_SNo 1 (minus_SNo t)) b) (Rlt (add_SNo 1 (minus_SNo b)) t) (Hflip_lower t b HtR HbR) Hrlt).
We prove the intermediate claim Hrlt3: Rlt (apply_fun flip_unit_interval t) b.
rewrite the current goal using (flip_unit_interval_apply t HtI) (from left to right).
An exact proof term for the current goal is Hrlt2.
We prove the intermediate claim Hrel2: order_rel R (apply_fun flip_unit_interval t) b.
An exact proof term for the current goal is (Rlt_implies_order_rel_R (apply_fun flip_unit_interval t) b Hrlt3).
We prove the intermediate claim HimgR: apply_fun flip_unit_interval t ∈ R.
An exact proof term for the current goal is (HfunR t HtI).
We prove the intermediate claim Himg: apply_fun flip_unit_interval t ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R x0 b) (apply_fun flip_unit_interval t) HimgR Hrel2).
An exact proof term for the current goal is (SepI unit_interval (λu : set ⇒ apply_fun flip_unit_interval u ∈ open_ray_lower R b) t HtI Himg).
rewrite the current goal using HpreEq (from left to right).
Set Z0 to be the term open_ray_upper R c.
We prove the intermediate claim HZ0open: Z0 ∈ R_standard_topology.
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: Z0 ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis R c HcR).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R Z0 HsRay).
We prove the intermediate claim HZ0cap: Z0 ∩ unit_interval ∈ Tx.
We will prove Z0 ∩ unit_interval ∈ {W ∈ 𝒫 unit_interval|∃Z ∈ R_standard_topology, W = Z ∩ unit_interval}.
We prove the intermediate claim Hpow: Z0 ∩ unit_interval ∈ 𝒫 unit_interval.
Apply PowerI to the current goal.
Let t be given.
Assume Ht: t ∈ Z0 ∩ unit_interval.
An exact proof term for the current goal is (binintersectE2 Z0 unit_interval t Ht).
We prove the intermediate claim Hex: ∃Z ∈ R_standard_topology, Z0 ∩ unit_interval = Z ∩ unit_interval.
We use Z0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HZ0open.
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 unit_interval) (λW0 : set ⇒ ∃Z ∈ R_standard_topology, W0 = Z ∩ unit_interval) (Z0 ∩ unit_interval) Hpow Hex).
An exact proof term for the current goal is HZ0cap.
An exact proof term for the current goal is Hs0.
Assume HsR: s ∈ {R}.
We prove the intermediate claim Hseq: s = R.
An exact proof term for the current goal is (SingE R s HsR).
rewrite the current goal using Hseq (from left to right).
We prove the intermediate claim Heq: preimage_of unit_interval flip_unit_interval R = unit_interval.
An exact proof term for the current goal is (preimage_of_whole unit_interval R flip_unit_interval HfunR).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (topology_has_X unit_interval Tx HTx).
An exact proof term for the current goal is HsS.
An exact proof term for the current goal is (continuous_map_from_subbasis unit_interval Tx R S flip_unit_interval HTx HfunR HS HpreS).
We prove the intermediate claim Himg: ∀t : set, t ∈ unit_interval → apply_fun flip_unit_interval t ∈ unit_interval.
Let t be given.
Assume Ht: t ∈ unit_interval.
An exact proof term for the current goal is (flip_unit_interval_function_on t Ht).
An exact proof term for the current goal is (continuous_map_range_restrict unit_interval Tx R R_standard_topology flip_unit_interval unit_interval HcontR unit_interval_sub_R Himg).
∎