We will prove continuous_map unit_interval_left_half (subspace_topology unit_interval unit_interval_topology unit_interval_left_half) unit_interval unit_interval_topology double_map_left_half.
We prove the intermediate claim HcontR: continuous_map unit_interval_left_half (subspace_topology unit_interval unit_interval_topology unit_interval_left_half) R R_standard_topology double_map_left_half.
Set Tx to be the term subspace_topology unit_interval unit_interval_topology unit_interval_left_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_left_half Tx.
An exact proof term for the current goal is (subspace_topology_is_topology unit_interval unit_interval_topology unit_interval_left_half HTui unit_interval_left_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_map_left_half unit_interval_left_half R.
Let t be given.
Assume Ht: t ∈ unit_interval_left_half.
We will prove apply_fun double_map_left_half t ∈ R.
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (unit_interval_left_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 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).
rewrite the current goal using (double_map_apply t Ht) (from left to right).
An exact proof term for the current goal is HmulR.
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 HpreS: ∀s : set, s ∈ S → preimage_of unit_interval_left_half double_map_left_half s ∈ Tx.
Let s be given.
Assume HsS: s ∈ S.
We will prove preimage_of unit_interval_left_half double_map_left_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_left_half double_map_left_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_left_half double_map_left_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 c to be the term mul_SNo (eps_ 1) 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 He1Real: (eps_ 1) ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is eps_1_in_R.
An exact proof term for the current goal is (real_mul_SNo (eps_ 1) He1Real a HaReal).
We prove the intermediate claim HpreEq: preimage_of unit_interval_left_half double_map_left_half (open_ray_upper R a) = (open_ray_upper R c) ∩ unit_interval_left_half.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ preimage_of unit_interval_left_half double_map_left_half (open_ray_upper R a).
We will prove t ∈ (open_ray_upper R c) ∩ unit_interval_left_half.
We prove the intermediate claim HtLH: t ∈ unit_interval_left_half.
An exact proof term for the current goal is (SepE1 unit_interval_left_half (λu : set ⇒ apply_fun double_map_left_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_left_half_sub t HtLH).
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_map_left_half t ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepE2 unit_interval_left_half (λu : set ⇒ apply_fun double_map_left_half u ∈ open_ray_upper R a) t Ht).
We prove the intermediate claim Hrel: order_rel R a (apply_fun double_map_left_half t).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R a x0) (apply_fun double_map_left_half t) Himg).
We prove the intermediate claim Hrlt: Rlt a (apply_fun double_map_left_half t).
An exact proof term for the current goal is (order_rel_R_implies_Rlt a (apply_fun double_map_left_half t) Hrel).
We prove the intermediate claim Hrlt2: Rlt a (mul_SNo 2 t).
rewrite the current goal using (double_map_apply t HtLH) (from right to left).
An exact proof term for the current goal is Hrlt.
We prove the intermediate claim Hrltc: Rlt c t.
An exact proof term for the current goal is (iffEL (Rlt a (mul_SNo 2 t)) (Rlt (mul_SNo (eps_ 1) a) t) (Rlt_mul2_left_iff a t HaR HtR) Hrlt2).
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 Hrltc).
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_left_half t HtRay HtLH).
Let t be given.
Assume Ht: t ∈ (open_ray_upper R c) ∩ unit_interval_left_half.
We will prove t ∈ preimage_of unit_interval_left_half double_map_left_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_left_half t Ht).
We prove the intermediate claim HtLH: t ∈ unit_interval_left_half.
An exact proof term for the current goal is (binintersectE2 (open_ray_upper R c) unit_interval_left_half t Ht).
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (unit_interval_left_half_sub t HtLH).
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 a (mul_SNo 2 t).
An exact proof term for the current goal is (iffER (Rlt a (mul_SNo 2 t)) (Rlt (mul_SNo (eps_ 1) a) t) (Rlt_mul2_left_iff a t HaR HtR) Hrlt).
We prove the intermediate claim Hrlt3: Rlt a (apply_fun double_map_left_half t).
rewrite the current goal using (double_map_apply t HtLH) (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 double_map_left_half t).
An exact proof term for the current goal is (Rlt_implies_order_rel_R a (apply_fun double_map_left_half t) Hrlt3).
We prove the intermediate claim HimgR: apply_fun double_map_left_half t ∈ R.
An exact proof term for the current goal is (Hfun t HtLH).
We prove the intermediate claim Himg: apply_fun double_map_left_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_map_left_half t) HimgR Hrel2).
An exact proof term for the current goal is (SepI unit_interval_left_half (λu : set ⇒ apply_fun double_map_left_half u ∈ open_ray_upper R a) t HtLH Himg).
rewrite the current goal using HpreEq (from left to right).
We will prove (open_ray_upper R c) ∩ unit_interval_left_half ∈ Tx.
We will prove (open_ray_upper R c) ∩ unit_interval_left_half ∈ {W ∈ 𝒫 unit_interval_left_half|∃Z ∈ unit_interval_topology, W = Z ∩ unit_interval_left_half}.
We prove the intermediate claim Hpow: (open_ray_upper R c) ∩ unit_interval_left_half ∈ 𝒫 unit_interval_left_half.
Apply PowerI to the current goal.
Let t be given.
Assume Ht: t ∈ (open_ray_upper R c) ∩ unit_interval_left_half.
An exact proof term for the current goal is (binintersectE2 (open_ray_upper R c) unit_interval_left_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 HcS: c ∈ R.
An exact proof term for the current goal is HcR.
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 HcS).
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_left_half = Z0 ∩ unit_interval_left_half.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ (open_ray_upper R c) ∩ unit_interval_left_half.
We will prove t ∈ Z0 ∩ unit_interval_left_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_left_half t Ht).
We prove the intermediate claim HtLH: t ∈ unit_interval_left_half.
An exact proof term for the current goal is (binintersectE2 (open_ray_upper R c) unit_interval_left_half t Ht).
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (unit_interval_left_half_sub t HtLH).
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_left_half t HtZ0 HtLH).
Let t be given.
Assume Ht: t ∈ Z0 ∩ unit_interval_left_half.
We will prove t ∈ (open_ray_upper R c) ∩ unit_interval_left_half.
We prove the intermediate claim HtZ0: t ∈ Z0.
An exact proof term for the current goal is (binintersectE1 Z0 unit_interval_left_half t Ht).
We prove the intermediate claim HtLH: t ∈ unit_interval_left_half.
An exact proof term for the current goal is (binintersectE2 Z0 unit_interval_left_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_left_half t HtRay HtLH).
We prove the intermediate claim Hex: ∃Z ∈ unit_interval_topology, (open_ray_upper R c) ∩ unit_interval_left_half = Z ∩ unit_interval_left_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_left_half) (λW0 : set ⇒ ∃Z ∈ unit_interval_topology, W0 = Z ∩ unit_interval_left_half) ((open_ray_upper R c) ∩ unit_interval_left_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 c to be the term mul_SNo (eps_ 1) 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 He1Real: (eps_ 1) ∈ real.
rewrite the current goal using HdefR (from right to left).
An exact proof term for the current goal is eps_1_in_R.
An exact proof term for the current goal is (real_mul_SNo (eps_ 1) He1Real b HbReal).
We prove the intermediate claim HpreEq: preimage_of unit_interval_left_half double_map_left_half (open_ray_lower R b) = (open_ray_lower R c) ∩ unit_interval_left_half.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ preimage_of unit_interval_left_half double_map_left_half (open_ray_lower R b).
We will prove t ∈ (open_ray_lower R c) ∩ unit_interval_left_half.
We prove the intermediate claim HtLH: t ∈ unit_interval_left_half.
An exact proof term for the current goal is (SepE1 unit_interval_left_half (λu : set ⇒ apply_fun double_map_left_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_left_half_sub t HtLH).
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_map_left_half t ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepE2 unit_interval_left_half (λu : set ⇒ apply_fun double_map_left_half u ∈ open_ray_lower R b) t Ht).
We prove the intermediate claim Hrel: order_rel R (apply_fun double_map_left_half t) b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 b) (apply_fun double_map_left_half t) Himg).
We prove the intermediate claim Hrlt: Rlt (apply_fun double_map_left_half t) b.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun double_map_left_half t) b Hrel).
We prove the intermediate claim Hrlt2: Rlt (mul_SNo 2 t) b.
rewrite the current goal using (double_map_apply t HtLH) (from right to left) at position 1.
An exact proof term for the current goal is Hrlt.
We prove the intermediate claim Hrltc: Rlt t c.
An exact proof term for the current goal is (iffEL (Rlt (mul_SNo 2 t) b) (Rlt t (mul_SNo (eps_ 1) b)) (Rlt_mul2_right_iff t b HtR HbR) Hrlt2).
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 Hrltc).
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_left_half t HtRay HtLH).
Let t be given.
Assume Ht: t ∈ (open_ray_lower R c) ∩ unit_interval_left_half.
We will prove t ∈ preimage_of unit_interval_left_half double_map_left_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_left_half t Ht).
We prove the intermediate claim HtLH: t ∈ unit_interval_left_half.
An exact proof term for the current goal is (binintersectE2 (open_ray_lower R c) unit_interval_left_half t Ht).
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (unit_interval_left_half_sub t HtLH).
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) b.
An exact proof term for the current goal is (iffER (Rlt (mul_SNo 2 t) b) (Rlt t (mul_SNo (eps_ 1) b)) (Rlt_mul2_right_iff t b HtR HbR) Hrlt).
We prove the intermediate claim Hrlt3: Rlt (apply_fun double_map_left_half t) b.
rewrite the current goal using (double_map_apply t HtLH) (from left to right) at position 1.
An exact proof term for the current goal is Hrlt2.
We prove the intermediate claim Hrel2: order_rel R (apply_fun double_map_left_half t) b.
An exact proof term for the current goal is (Rlt_implies_order_rel_R (apply_fun double_map_left_half t) b Hrlt3).
We prove the intermediate claim HimgR: apply_fun double_map_left_half t ∈ R.
An exact proof term for the current goal is (Hfun t HtLH).
We prove the intermediate claim Himg: apply_fun double_map_left_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_map_left_half t) HimgR Hrel2).
An exact proof term for the current goal is (SepI unit_interval_left_half (λu : set ⇒ apply_fun double_map_left_half u ∈ open_ray_lower R b) t HtLH Himg).
rewrite the current goal using HpreEq (from left to right).
We will prove (open_ray_lower R c) ∩ unit_interval_left_half ∈ Tx.
We will prove (open_ray_lower R c) ∩ unit_interval_left_half ∈ {W ∈ 𝒫 unit_interval_left_half|∃Z ∈ unit_interval_topology, W = Z ∩ unit_interval_left_half}.
We prove the intermediate claim Hpow: (open_ray_lower R c) ∩ unit_interval_left_half ∈ 𝒫 unit_interval_left_half.
Apply PowerI to the current goal.
Let t be given.
Assume Ht: t ∈ (open_ray_lower R c) ∩ unit_interval_left_half.
An exact proof term for the current goal is (binintersectE2 (open_ray_lower R c) unit_interval_left_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 HcS: c ∈ R.
An exact proof term for the current goal is HcR.
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 HcS).
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_left_half = Z0 ∩ unit_interval_left_half.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ (open_ray_lower R c) ∩ unit_interval_left_half.
We will prove t ∈ Z0 ∩ unit_interval_left_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_left_half t Ht).
We prove the intermediate claim HtLH: t ∈ unit_interval_left_half.
An exact proof term for the current goal is (binintersectE2 (open_ray_lower R c) unit_interval_left_half t Ht).
We prove the intermediate claim HtI: t ∈ unit_interval.
An exact proof term for the current goal is (unit_interval_left_half_sub t HtLH).
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_left_half t HtZ0 HtLH).
Let t be given.
Assume Ht: t ∈ Z0 ∩ unit_interval_left_half.
We will prove t ∈ (open_ray_lower R c) ∩ unit_interval_left_half.
We prove the intermediate claim HtZ0: t ∈ Z0.
An exact proof term for the current goal is (binintersectE1 Z0 unit_interval_left_half t Ht).
We prove the intermediate claim HtLH: t ∈ unit_interval_left_half.
An exact proof term for the current goal is (binintersectE2 Z0 unit_interval_left_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_left_half t HtRay HtLH).
We prove the intermediate claim Hex: ∃Z ∈ unit_interval_topology, (open_ray_lower R c) ∩ unit_interval_left_half = Z ∩ unit_interval_left_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_left_half) (λW0 : set ⇒ ∃Z ∈ unit_interval_topology, W0 = Z ∩ unit_interval_left_half) ((open_ray_lower R c) ∩ unit_interval_left_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_left_half double_map_left_half R = unit_interval_left_half.
An exact proof term for the current goal is (preimage_of_whole unit_interval_left_half R double_map_left_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_left_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_left_half Tx R S double_map_left_half HTx Hfun HS HpreS).
We prove the intermediate claim Himg: ∀t : set, t ∈ unit_interval_left_half → apply_fun double_map_left_half t ∈ unit_interval.
Let t be given.
Assume Ht: t ∈ unit_interval_left_half.
An exact proof term for the current goal is (double_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_left_half (subspace_topology unit_interval unit_interval_topology unit_interval_left_half) R R_standard_topology double_map_left_half unit_interval HcontR unit_interval_sub_R Himg).
∎