We will prove continuous_map unit_interval_right_half (subspace_topology unit_interval unit_interval_topology unit_interval_right_half) unit_interval unit_interval_topology double_minus_one_map_right_half.
We prove the intermediate claim HcontR: continuous_map unit_interval_right_half (subspace_topology unit_interval unit_interval_topology unit_interval_right_half) R R_standard_topology double_minus_one_map_right_half.
Set Tx to be the term subspace_topology unit_interval unit_interval_topology unit_interval_right_half.
Set S to be the term open_rays_subbasis R.
We prove the intermediate claim HTui: topology_on unit_interval unit_interval_topology.
An exact proof term for the current goal is unit_interval_topology_on.
We prove the intermediate claim HTx: topology_on unit_interval_right_half Tx.
An exact proof term for the current goal is (subspace_topology_is_topology unit_interval unit_interval_topology unit_interval_right_half HTui unit_interval_right_half_sub).
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 Hfun: function_on double_minus_one_map_right_half unit_interval_right_half R.
Let t be given.
Assume Ht: t ∈ unit_interval_right_half.
We will prove apply_fun double_minus_one_map_right_half t ∈ R.
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (unit_interval_right_half_sub 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 H2R: 2 ∈ R.
An exact proof term for the current goal is real_2.
We prove the intermediate claim Hm1R: (minus_SNo 1) ∈ R.
We prove the intermediate claim HdefR: R = real.
Use reflexivity.
rewrite the current goal using HdefR (from left to right).
An exact proof term for the current goal is (real_minus_SNo 1 real_1).
We prove the intermediate claim HmulR: mul_SNo 2 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 H2Real: 2 ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is H2R.
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.
An exact proof term for the current goal is (real_mul_SNo 2 H2Real t HtReal).
We prove the intermediate claim HaddR: add_SNo (mul_SNo 2 t) (minus_SNo 1) ∈ 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 HmulReal: mul_SNo 2 t ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HmulR.
We prove the intermediate claim Hm1Real: (minus_SNo 1) ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is Hm1R.
An exact proof term for the current goal is (real_add_SNo (mul_SNo 2 t) HmulReal (minus_SNo 1) Hm1Real).
rewrite the current goal using (double_minus_one_map_apply t Ht) (from left to right).
An exact proof term for the current goal is HaddR.
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 Haddm1L: ∀a x : set, a ∈ R → x ∈ R → (Rlt a (add_SNo x (minus_SNo 1)) ↔ Rlt (add_SNo a 1) x).
Let a and x be given.
Assume HaR: a ∈ R.
Assume HxR: x ∈ R.
We will prove (Rlt a (add_SNo x (minus_SNo 1)) ↔ Rlt (add_SNo a 1) x).
Apply iffI to the current goal.
Assume Hlt: Rlt a (add_SNo x (minus_SNo 1)).
We will prove Rlt (add_SNo a 1) x.
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 HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
We prove the intermediate claim Hx_m1S: SNo (add_SNo x (minus_SNo 1)).
An exact proof term for the current goal is (SNo_add_SNo x (minus_SNo 1) HxS Hm1S).
We prove the intermediate claim HltS: a < add_SNo x (minus_SNo 1).
An exact proof term for the current goal is (RltE_lt a (add_SNo x (minus_SNo 1)) Hlt).
We prove the intermediate claim Hstep: add_SNo a 1 < add_SNo (add_SNo x (minus_SNo 1)) 1.
An exact proof term for the current goal is (add_SNo_Lt1 a 1 (add_SNo x (minus_SNo 1)) HaS SNo_1 Hx_m1S HltS).
We prove the intermediate claim Heq: add_SNo (add_SNo x (minus_SNo 1)) 1 = x.
rewrite the current goal using (add_SNo_assoc x (minus_SNo 1) 1 HxS Hm1S SNo_1) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_linv 1 SNo_1) (from left to right).
An exact proof term for the current goal is (add_SNo_0R x HxS).
We prove the intermediate claim Hstep2: add_SNo a 1 < x.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hstep.
We prove the intermediate claim Ha1R: add_SNo a 1 ∈ 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.
An exact proof term for the current goal is (real_add_SNo a HaReal 1 real_1).
An exact proof term for the current goal is (RltI (add_SNo a 1) x Ha1R HxR Hstep2).
Assume Hlt: Rlt (add_SNo a 1) x.
We will prove Rlt a (add_SNo x (minus_SNo 1)).
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 HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
We prove the intermediate claim Ha1S: SNo (add_SNo a 1).
An exact proof term for the current goal is (SNo_add_SNo a 1 HaS SNo_1).
We prove the intermediate claim HltS: add_SNo a 1 < x.
An exact proof term for the current goal is (RltE_lt (add_SNo a 1) x Hlt).
We prove the intermediate claim Hstep: add_SNo (add_SNo a 1) (minus_SNo 1) < add_SNo x (minus_SNo 1).
An exact proof term for the current goal is (add_SNo_Lt1 (add_SNo a 1) (minus_SNo 1) x Ha1S Hm1S HxS HltS).
We prove the intermediate claim Heq: add_SNo (add_SNo a 1) (minus_SNo 1) = a.
rewrite the current goal using (add_SNo_assoc a 1 (minus_SNo 1) HaS SNo_1 Hm1S) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv 1 SNo_1) (from left to right).
An exact proof term for the current goal is (add_SNo_0R a HaS).
We prove the intermediate claim Hstep2: a < add_SNo x (minus_SNo 1).
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Hstep.
We prove the intermediate claim Hx_m1R: add_SNo x (minus_SNo 1) ∈ 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 HxReal: x ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HxR.
An exact proof term for the current goal is (real_add_SNo x HxReal (minus_SNo 1) (real_minus_SNo 1 real_1)).
An exact proof term for the current goal is (RltI a (add_SNo x (minus_SNo 1)) HaR Hx_m1R Hstep2).
We prove the intermediate claim Haddm1R: ∀x b : set, x ∈ R → b ∈ R → (Rlt (add_SNo x (minus_SNo 1)) b ↔ Rlt x (add_SNo b 1)).
Let x and b be given.
Assume HxR: x ∈ R.
Assume HbR: b ∈ R.
We will prove (Rlt (add_SNo x (minus_SNo 1)) b ↔ Rlt x (add_SNo b 1)).
Apply iffI to the current goal.
Assume Hlt: Rlt (add_SNo x (minus_SNo 1)) b.
We will prove Rlt x (add_SNo b 1).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
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 Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
We prove the intermediate claim Hx_m1S: SNo (add_SNo x (minus_SNo 1)).
An exact proof term for the current goal is (SNo_add_SNo x (minus_SNo 1) HxS Hm1S).
We prove the intermediate claim HltS: add_SNo x (minus_SNo 1) < b.
An exact proof term for the current goal is (RltE_lt (add_SNo x (minus_SNo 1)) b Hlt).
We prove the intermediate claim Hstep: add_SNo (add_SNo x (minus_SNo 1)) 1 < add_SNo b 1.
An exact proof term for the current goal is (add_SNo_Lt1 (add_SNo x (minus_SNo 1)) 1 b Hx_m1S SNo_1 HbS HltS).
We prove the intermediate claim Heq: add_SNo (add_SNo x (minus_SNo 1)) 1 = x.
rewrite the current goal using (add_SNo_assoc x (minus_SNo 1) 1 HxS Hm1S SNo_1) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_linv 1 SNo_1) (from left to right).
An exact proof term for the current goal is (add_SNo_0R x HxS).
We prove the intermediate claim Hstep2: x < add_SNo b 1.
rewrite the current goal using Heq (from right to left) at position 1.
An exact proof term for the current goal is Hstep.
We prove the intermediate claim Hb1R: add_SNo b 1 ∈ 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.
An exact proof term for the current goal is (real_add_SNo b HbReal 1 real_1).
An exact proof term for the current goal is (RltI x (add_SNo b 1) HxR Hb1R Hstep2).
Assume Hlt: Rlt x (add_SNo b 1).
We will prove Rlt (add_SNo x (minus_SNo 1)) b.
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
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 Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
We prove the intermediate claim Hb1S: SNo (add_SNo b 1).
An exact proof term for the current goal is (SNo_add_SNo b 1 HbS SNo_1).
We prove the intermediate claim HltS: x < add_SNo b 1.
An exact proof term for the current goal is (RltE_lt x (add_SNo b 1) Hlt).
We prove the intermediate claim Hstep: add_SNo x (minus_SNo 1) < add_SNo (add_SNo b 1) (minus_SNo 1).
An exact proof term for the current goal is (add_SNo_Lt1 x (minus_SNo 1) (add_SNo b 1) HxS Hm1S Hb1S HltS).
We prove the intermediate claim Heq: add_SNo (add_SNo b 1) (minus_SNo 1) = b.
rewrite the current goal using (add_SNo_assoc b 1 (minus_SNo 1) HbS SNo_1 Hm1S) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv 1 SNo_1) (from left to right).
An exact proof term for the current goal is (add_SNo_0R b HbS).
We prove the intermediate claim Hstep2: add_SNo x (minus_SNo 1) < b.
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is Hstep.
We prove the intermediate claim Hx_m1R: add_SNo x (minus_SNo 1) ∈ 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 HxReal: x ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HxR.
An exact proof term for the current goal is (real_add_SNo x HxReal (minus_SNo 1) (real_minus_SNo 1 real_1)).
An exact proof term for the current goal is (RltI (add_SNo x (minus_SNo 1)) b Hx_m1R HbR Hstep2).
We prove the intermediate claim HpreS: ∀s : set, s ∈ S → preimage_of unit_interval_right_half double_minus_one_map_right_half s ∈ Tx.
Let s be given.
Assume HsS: s ∈ S.
We will prove preimage_of unit_interval_right_half double_minus_one_map_right_half 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_right_half double_minus_one_map_right_half 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_right_half double_minus_one_map_right_half 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 d to be the term add_SNo a 1.
Set c to be the term mul_SNo (eps_ 1) d.
We prove the intermediate claim HdR: d ∈ 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.
An exact proof term for the current goal is (real_add_SNo a HaReal 1 real_1).
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 HdReal: d ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HdR.
An exact proof term for the current goal is (real_mul_SNo (eps_ 1) eps_1_in_R d HdReal).
We prove the intermediate claim HpreEq: preimage_of unit_interval_right_half double_minus_one_map_right_half (open_ray_upper R a) = (open_ray_upper R c) ∩ unit_interval_right_half.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ preimage_of unit_interval_right_half double_minus_one_map_right_half (open_ray_upper R a).
We will prove t ∈ (open_ray_upper R c) ∩ unit_interval_right_half.
We prove the intermediate claim HtRH: t ∈ unit_interval_right_half.
An exact proof term for the current goal is (SepE1 unit_interval_right_half (λu : set ⇒ apply_fun double_minus_one_map_right_half u ∈ open_ray_upper R a) t Ht).
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (unit_interval_right_half_sub t HtRH).
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 double_minus_one_map_right_half t ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepE2 unit_interval_right_half (λu : set ⇒ apply_fun double_minus_one_map_right_half u ∈ open_ray_upper R a) t Ht).
We prove the intermediate claim Hrel: order_rel R a (apply_fun double_minus_one_map_right_half t).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R a x0) (apply_fun double_minus_one_map_right_half t) Himg).
We prove the intermediate claim Hrlt: Rlt a (apply_fun double_minus_one_map_right_half t).
An exact proof term for the current goal is (order_rel_R_implies_Rlt a (apply_fun double_minus_one_map_right_half t) Hrel).
We prove the intermediate claim Hrlt2: Rlt a (add_SNo (mul_SNo 2 t) (minus_SNo 1)).
rewrite the current goal using (double_minus_one_map_apply t HtRH) (from right to left).
An exact proof term for the current goal is Hrlt.
We prove the intermediate claim H2tR: mul_SNo 2 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 H2Real: 2 ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is real_2.
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.
An exact proof term for the current goal is (real_mul_SNo 2 H2Real t HtReal).
We prove the intermediate claim Hrlt3: Rlt d (mul_SNo 2 t).
An exact proof term for the current goal is (iffEL (Rlt a (add_SNo (mul_SNo 2 t) (minus_SNo 1))) (Rlt (add_SNo a 1) (mul_SNo 2 t)) (Haddm1L a (mul_SNo 2 t) HaR H2tR) Hrlt2).
We prove the intermediate claim Hrlt4: Rlt c t.
An exact proof term for the current goal is (iffEL (Rlt d (mul_SNo 2 t)) (Rlt (mul_SNo (eps_ 1) d) t) (Rlt_mul2_left_iff d t HdR HtR) Hrlt3).
We prove the intermediate claim HcRel: order_rel R c t.
An exact proof term for the current goal is (Rlt_implies_order_rel_R c t Hrlt4).
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 HcRel).
An exact proof term for the current goal is (binintersectI (open_ray_upper R c) unit_interval_right_half t HtRay HtRH).
Let t be given.
Assume Ht: t ∈ (open_ray_upper R c) ∩ unit_interval_right_half.
We will prove t ∈ preimage_of unit_interval_right_half double_minus_one_map_right_half (open_ray_upper R a).
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_right_half t Ht).
We prove the intermediate claim HtRH: t ∈ unit_interval_right_half.
An exact proof term for the current goal is (binintersectE2 (open_ray_upper R c) unit_interval_right_half t Ht).
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (unit_interval_right_half_sub t HtRH).
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 d (mul_SNo 2 t).
An exact proof term for the current goal is (iffER (Rlt d (mul_SNo 2 t)) (Rlt (mul_SNo (eps_ 1) d) t) (Rlt_mul2_left_iff d t HdR HtR) Hrlt).
We prove the intermediate claim H2tR: mul_SNo 2 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 H2Real: 2 ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is real_2.
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.
An exact proof term for the current goal is (real_mul_SNo 2 H2Real t HtReal).
We prove the intermediate claim Hrlt3: Rlt a (add_SNo (mul_SNo 2 t) (minus_SNo 1)).
An exact proof term for the current goal is (iffER (Rlt a (add_SNo (mul_SNo 2 t) (minus_SNo 1))) (Rlt (add_SNo a 1) (mul_SNo 2 t)) (Haddm1L a (mul_SNo 2 t) HaR H2tR) Hrlt2).
We prove the intermediate claim Hrlt4: Rlt a (apply_fun double_minus_one_map_right_half t).
rewrite the current goal using (double_minus_one_map_apply t HtRH) (from left to right).
An exact proof term for the current goal is Hrlt3.
We prove the intermediate claim Hrel2: order_rel R a (apply_fun double_minus_one_map_right_half t).
An exact proof term for the current goal is (Rlt_implies_order_rel_R a (apply_fun double_minus_one_map_right_half t) Hrlt4).
We prove the intermediate claim HimgR: apply_fun double_minus_one_map_right_half t ∈ R.
An exact proof term for the current goal is (Hfun t HtRH).
We prove the intermediate claim Himg: apply_fun double_minus_one_map_right_half 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 double_minus_one_map_right_half t) HimgR Hrel2).
An exact proof term for the current goal is (SepI unit_interval_right_half (λu : set ⇒ apply_fun double_minus_one_map_right_half u ∈ open_ray_upper R a) t HtRH Himg).
rewrite the current goal using HpreEq (from left to right).
We will prove (open_ray_upper R c) ∩ unit_interval_right_half ∈ Tx.
We will prove (open_ray_upper R c) ∩ unit_interval_right_half ∈ {W ∈ 𝒫 unit_interval_right_half|∃Z ∈ unit_interval_topology, W = Z ∩ unit_interval_right_half}.
We prove the intermediate claim Hpow: (open_ray_upper R c) ∩ unit_interval_right_half ∈ 𝒫 unit_interval_right_half.
Apply PowerI to the current goal.
Let t be given.
Assume Ht: t ∈ (open_ray_upper R c) ∩ unit_interval_right_half.
An exact proof term for the current goal is (binintersectE2 (open_ray_upper R c) unit_interval_right_half t Ht).
Set Z0 to be the term (open_ray_upper R c) ∩ unit_interval.
We prove the intermediate claim HZ0: Z0 ∈ unit_interval_topology.
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 will prove Z0 ∈ {W ∈ 𝒫 unit_interval|∃Z ∈ R_standard_topology, W = Z ∩ unit_interval}.
We prove the intermediate claim HZ0pow: Z0 ∈ 𝒫 unit_interval.
Apply PowerI to the current goal.
Let t be given.
Assume Ht: t ∈ Z0.
An exact proof term for the current goal is (binintersectE2 (open_ray_upper R c) unit_interval t Ht).
We prove the intermediate claim HopenR: open_ray_upper R c ∈ R_standard_topology.
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: open_ray_upper R c ∈ 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 (open_ray_upper R c) HsRay).
We prove the intermediate claim Hex: ∃Z ∈ R_standard_topology, Z0 = Z ∩ unit_interval.
We use (open_ray_upper R c) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HopenR.
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 HZ0pow Hex).
We prove the intermediate claim Heq: (open_ray_upper R c) ∩ unit_interval_right_half = Z0 ∩ unit_interval_right_half.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ (open_ray_upper R c) ∩ unit_interval_right_half.
We will prove t ∈ Z0 ∩ unit_interval_right_half.
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_right_half t Ht).
We prove the intermediate claim HtRH: t ∈ unit_interval_right_half.
An exact proof term for the current goal is (binintersectE2 (open_ray_upper R c) unit_interval_right_half t Ht).
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (unit_interval_right_half_sub t HtRH).
We prove the intermediate claim HtZ0: t ∈ Z0.
An exact proof term for the current goal is (binintersectI (open_ray_upper R c) unit_interval t HtRay HtI).
An exact proof term for the current goal is (binintersectI Z0 unit_interval_right_half t HtZ0 HtRH).
Let t be given.
Assume Ht: t ∈ Z0 ∩ unit_interval_right_half.
We will prove t ∈ (open_ray_upper R c) ∩ unit_interval_right_half.
We prove the intermediate claim HtZ0: t ∈ Z0.
An exact proof term for the current goal is (binintersectE1 Z0 unit_interval_right_half t Ht).
We prove the intermediate claim HtRH: t ∈ unit_interval_right_half.
An exact proof term for the current goal is (binintersectE2 Z0 unit_interval_right_half t Ht).
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 HtZ0).
An exact proof term for the current goal is (binintersectI (open_ray_upper R c) unit_interval_right_half t HtRay HtRH).
We prove the intermediate claim Hex: ∃Z ∈ unit_interval_topology, (open_ray_upper R c) ∩ unit_interval_right_half = Z ∩ unit_interval_right_half.
We use Z0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HZ0.
rewrite the current goal using Heq (from right to left).
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 unit_interval_right_half) (λW0 : set ⇒ ∃Z ∈ unit_interval_topology, W0 = Z ∩ unit_interval_right_half) ((open_ray_upper R c) ∩ unit_interval_right_half) Hpow Hex).
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 d to be the term add_SNo b 1.
Set c to be the term mul_SNo (eps_ 1) d.
We prove the intermediate claim HdR: d ∈ 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.
An exact proof term for the current goal is (real_add_SNo b HbReal 1 real_1).
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 HdReal: d ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is HdR.
An exact proof term for the current goal is (real_mul_SNo (eps_ 1) eps_1_in_R d HdReal).
We prove the intermediate claim HpreEq: preimage_of unit_interval_right_half double_minus_one_map_right_half (open_ray_lower R b) = (open_ray_lower R c) ∩ unit_interval_right_half.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ preimage_of unit_interval_right_half double_minus_one_map_right_half (open_ray_lower R b).
We will prove t ∈ (open_ray_lower R c) ∩ unit_interval_right_half.
We prove the intermediate claim HtRH: t ∈ unit_interval_right_half.
An exact proof term for the current goal is (SepE1 unit_interval_right_half (λu : set ⇒ apply_fun double_minus_one_map_right_half u ∈ open_ray_lower R b) t Ht).
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (unit_interval_right_half_sub t HtRH).
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 double_minus_one_map_right_half t ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepE2 unit_interval_right_half (λu : set ⇒ apply_fun double_minus_one_map_right_half u ∈ open_ray_lower R b) t Ht).
We prove the intermediate claim Hrel: order_rel R (apply_fun double_minus_one_map_right_half t) b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 b) (apply_fun double_minus_one_map_right_half t) Himg).
We prove the intermediate claim Hrlt: Rlt (apply_fun double_minus_one_map_right_half t) b.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun double_minus_one_map_right_half t) b Hrel).
We prove the intermediate claim Hrlt2: Rlt (add_SNo (mul_SNo 2 t) (minus_SNo 1)) b.
rewrite the current goal using (double_minus_one_map_apply t HtRH) (from right to left).
An exact proof term for the current goal is Hrlt.
We prove the intermediate claim H2tR: mul_SNo 2 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 H2Real: 2 ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is real_2.
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.
An exact proof term for the current goal is (real_mul_SNo 2 H2Real t HtReal).
We prove the intermediate claim Hrlt3: Rlt (mul_SNo 2 t) d.
An exact proof term for the current goal is (iffEL (Rlt (add_SNo (mul_SNo 2 t) (minus_SNo 1)) b) (Rlt (mul_SNo 2 t) (add_SNo b 1)) (Haddm1R (mul_SNo 2 t) b H2tR HbR) Hrlt2).
We prove the intermediate claim Hrlt4: Rlt t c.
An exact proof term for the current goal is (iffEL (Rlt (mul_SNo 2 t) d) (Rlt t (mul_SNo (eps_ 1) d)) (Rlt_mul2_right_iff t d HtR HdR) Hrlt3).
We prove the intermediate claim HcRel: order_rel R t c.
An exact proof term for the current goal is (Rlt_implies_order_rel_R t c Hrlt4).
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 HcRel).
An exact proof term for the current goal is (binintersectI (open_ray_lower R c) unit_interval_right_half t HtRay HtRH).
Let t be given.
Assume Ht: t ∈ (open_ray_lower R c) ∩ unit_interval_right_half.
We will prove t ∈ preimage_of unit_interval_right_half double_minus_one_map_right_half (open_ray_lower R b).
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_right_half t Ht).
We prove the intermediate claim HtRH: t ∈ unit_interval_right_half.
An exact proof term for the current goal is (binintersectE2 (open_ray_lower R c) unit_interval_right_half t Ht).
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (unit_interval_right_half_sub t HtRH).
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 (mul_SNo 2 t) d.
An exact proof term for the current goal is (iffER (Rlt (mul_SNo 2 t) d) (Rlt t (mul_SNo (eps_ 1) d)) (Rlt_mul2_right_iff t d HtR HdR) Hrlt).
We prove the intermediate claim H2tR: mul_SNo 2 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 H2Real: 2 ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is real_2.
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.
An exact proof term for the current goal is (real_mul_SNo 2 H2Real t HtReal).
We prove the intermediate claim Hrlt3: Rlt (add_SNo (mul_SNo 2 t) (minus_SNo 1)) b.
An exact proof term for the current goal is (iffER (Rlt (add_SNo (mul_SNo 2 t) (minus_SNo 1)) b) (Rlt (mul_SNo 2 t) (add_SNo b 1)) (Haddm1R (mul_SNo 2 t) b H2tR HbR) Hrlt2).
We prove the intermediate claim Hrlt4: Rlt (apply_fun double_minus_one_map_right_half t) b.
rewrite the current goal using (double_minus_one_map_apply t HtRH) (from left to right).
An exact proof term for the current goal is Hrlt3.
We prove the intermediate claim Hrel2: order_rel R (apply_fun double_minus_one_map_right_half t) b.
An exact proof term for the current goal is (Rlt_implies_order_rel_R (apply_fun double_minus_one_map_right_half t) b Hrlt4).
We prove the intermediate claim HimgR: apply_fun double_minus_one_map_right_half t ∈ R.
An exact proof term for the current goal is (Hfun t HtRH).
We prove the intermediate claim Himg: apply_fun double_minus_one_map_right_half 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 double_minus_one_map_right_half t) HimgR Hrel2).
An exact proof term for the current goal is (SepI unit_interval_right_half (λu : set ⇒ apply_fun double_minus_one_map_right_half u ∈ open_ray_lower R b) t HtRH Himg).
rewrite the current goal using HpreEq (from left to right).
We will prove (open_ray_lower R c) ∩ unit_interval_right_half ∈ Tx.
We will prove (open_ray_lower R c) ∩ unit_interval_right_half ∈ {W ∈ 𝒫 unit_interval_right_half|∃Z ∈ unit_interval_topology, W = Z ∩ unit_interval_right_half}.
We prove the intermediate claim Hpow: (open_ray_lower R c) ∩ unit_interval_right_half ∈ 𝒫 unit_interval_right_half.
Apply PowerI to the current goal.
Let t be given.
Assume Ht: t ∈ (open_ray_lower R c) ∩ unit_interval_right_half.
An exact proof term for the current goal is (binintersectE2 (open_ray_lower R c) unit_interval_right_half t Ht).
Set Z0 to be the term (open_ray_lower R c) ∩ unit_interval.
We prove the intermediate claim HZ0: Z0 ∈ unit_interval_topology.
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 will prove Z0 ∈ {W ∈ 𝒫 unit_interval|∃Z ∈ R_standard_topology, W = Z ∩ unit_interval}.
We prove the intermediate claim HZ0pow: Z0 ∈ 𝒫 unit_interval.
Apply PowerI to the current goal.
Let t be given.
Assume Ht: t ∈ Z0.
An exact proof term for the current goal is (binintersectE2 (open_ray_lower R c) unit_interval t Ht).
We prove the intermediate claim HopenR: open_ray_lower R c ∈ R_standard_topology.
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: open_ray_lower R c ∈ 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 (open_ray_lower R c) HsRay).
We prove the intermediate claim Hex: ∃Z ∈ R_standard_topology, Z0 = Z ∩ unit_interval.
We use (open_ray_lower R c) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HopenR.
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 HZ0pow Hex).
We prove the intermediate claim Heq: (open_ray_lower R c) ∩ unit_interval_right_half = Z0 ∩ unit_interval_right_half.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ (open_ray_lower R c) ∩ unit_interval_right_half.
We will prove t ∈ Z0 ∩ unit_interval_right_half.
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_right_half t Ht).
We prove the intermediate claim HtRH: t ∈ unit_interval_right_half.
An exact proof term for the current goal is (binintersectE2 (open_ray_lower R c) unit_interval_right_half t Ht).
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (unit_interval_right_half_sub t HtRH).
We prove the intermediate claim HtZ0: t ∈ Z0.
An exact proof term for the current goal is (binintersectI (open_ray_lower R c) unit_interval t HtRay HtI).
An exact proof term for the current goal is (binintersectI Z0 unit_interval_right_half t HtZ0 HtRH).
Let t be given.
Assume Ht: t ∈ Z0 ∩ unit_interval_right_half.
We will prove t ∈ (open_ray_lower R c) ∩ unit_interval_right_half.
We prove the intermediate claim HtZ0: t ∈ Z0.
An exact proof term for the current goal is (binintersectE1 Z0 unit_interval_right_half t Ht).
We prove the intermediate claim HtRH: t ∈ unit_interval_right_half.
An exact proof term for the current goal is (binintersectE2 Z0 unit_interval_right_half t Ht).
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 HtZ0).
An exact proof term for the current goal is (binintersectI (open_ray_lower R c) unit_interval_right_half t HtRay HtRH).
We prove the intermediate claim Hex: ∃Z ∈ unit_interval_topology, (open_ray_lower R c) ∩ unit_interval_right_half = Z ∩ unit_interval_right_half.
We use Z0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HZ0.
rewrite the current goal using Heq (from right to left).
Use reflexivity.
An exact proof term for the current goal is (SepI (𝒫 unit_interval_right_half) (λW0 : set ⇒ ∃Z ∈ unit_interval_topology, W0 = Z ∩ unit_interval_right_half) ((open_ray_lower R c) ∩ unit_interval_right_half) Hpow Hex).
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_right_half double_minus_one_map_right_half R = unit_interval_right_half.
An exact proof term for the current goal is (preimage_of_whole unit_interval_right_half R double_minus_one_map_right_half Hfun).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (topology_has_X unit_interval_right_half 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_right_half Tx R S double_minus_one_map_right_half HTx Hfun HS HpreS).
We prove the intermediate claim Himg: ∀t : set, t ∈ unit_interval_right_half → apply_fun double_minus_one_map_right_half t ∈ unit_interval.
Let t be given.
Assume Ht: t ∈ unit_interval_right_half.
An exact proof term for the current goal is (double_minus_one_map_function_on t Ht).
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).
An exact proof term for the current goal is (continuous_map_range_restrict unit_interval_right_half (subspace_topology unit_interval unit_interval_topology unit_interval_right_half) R R_standard_topology double_minus_one_map_right_half unit_interval HcontR unit_interval_sub_R Himg).
∎