Let a be given.
Assume HaR: a ∈ R.
We will prove preimage_of R normalize01_fun (open_ray_upper R a) ∈ R_standard_topology.
Apply xm (Rlt a 0) to the current goal.
Assume Halt0: Rlt a 0.
We prove the intermediate claim HpreEq: preimage_of R normalize01_fun (open_ray_upper R a) = R.
Apply set_ext to the current goal.
Let t be given.
Assume HtPre: t ∈ preimage_of R normalize01_fun (open_ray_upper R a).
An exact proof term for the current goal is (SepE1 R (λx : set ⇒ apply_fun normalize01_fun x ∈ open_ray_upper R a) t HtPre).
Let t be given.
Assume HtR: t ∈ R.
We prove the intermediate claim HfUI: apply_fun normalize01_fun t ∈ unit_interval.
An exact proof term for the current goal is (normalize01_fun_range_in_unit_interval t HtR).
We prove the intermediate claim HfR: apply_fun normalize01_fun t ∈ R.
An exact proof term for the current goal is (normalize01_fun_value_in_R t HtR).
We prove the intermediate claim Hbounds: ¬ (Rlt (apply_fun normalize01_fun t) 0) ∧ ¬ (Rlt 1 (apply_fun normalize01_fun t)).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) (apply_fun normalize01_fun t) HfUI).
We prove the intermediate claim Hnlt0: ¬ (Rlt (apply_fun normalize01_fun t) 0).
An exact proof term for the current goal is (andEL (¬ (Rlt (apply_fun normalize01_fun t) 0)) (¬ (Rlt 1 (apply_fun normalize01_fun t))) Hbounds).
We prove the intermediate claim Hle0: Rle 0 (apply_fun normalize01_fun t).
An exact proof term for the current goal is (RleI 0 (apply_fun normalize01_fun t) real_0 HfR Hnlt0).
We prove the intermediate claim Haltf: Rlt a (apply_fun normalize01_fun t).
An exact proof term for the current goal is (Rlt_Rle_tra a 0 (apply_fun normalize01_fun t) Halt0 Hle0).
We prove the intermediate claim Hrel: order_rel R a (apply_fun normalize01_fun t).
An exact proof term for the current goal is (Rlt_implies_order_rel_R a (apply_fun normalize01_fun t) Haltf).
We prove the intermediate claim HftRay: apply_fun normalize01_fun t ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepI R (λx : set ⇒ order_rel R a x) (apply_fun normalize01_fun t) HfR Hrel).
An exact proof term for the current goal is (SepI R (λx : set ⇒ apply_fun normalize01_fun x ∈ open_ray_upper R a) t HtR HftRay).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is (topology_has_X R R_standard_topology R_standard_topology_is_topology).
Assume Hnlt0: ¬ (Rlt a 0).
Apply xm (Rlt a 1) to the current goal.
Assume Halt1: Rlt a 1.
An exact proof term for the current goal is (normalize01_fun_preimage_open_ray_upper_mid a HaR Hnlt0 Halt1).
Assume Hnlt1: ¬ (Rlt a 1).
We prove the intermediate claim HpreEq: preimage_of R normalize01_fun (open_ray_upper R a) = Empty.
Apply set_ext to the current goal.
Let t be given.
Assume HtPre: t ∈ preimage_of R normalize01_fun (open_ray_upper R a).
We will prove t ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx : set ⇒ apply_fun normalize01_fun x ∈ open_ray_upper R a) t HtPre).
We prove the intermediate claim HfUI: apply_fun normalize01_fun t ∈ unit_interval.
An exact proof term for the current goal is (normalize01_fun_range_in_unit_interval t HtR).
We prove the intermediate claim HfR: apply_fun normalize01_fun t ∈ R.
An exact proof term for the current goal is (normalize01_fun_value_in_R t HtR).
We prove the intermediate claim Hbounds: ¬ (Rlt (apply_fun normalize01_fun t) 0) ∧ ¬ (Rlt 1 (apply_fun normalize01_fun t)).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ¬ (Rlt x0 0) ∧ ¬ (Rlt 1 x0)) (apply_fun normalize01_fun t) HfUI).
We prove the intermediate claim Hnlt1f: ¬ (Rlt 1 (apply_fun normalize01_fun t)).
An exact proof term for the current goal is (andER (¬ (Rlt (apply_fun normalize01_fun t) 0)) (¬ (Rlt 1 (apply_fun normalize01_fun t))) Hbounds).
We prove the intermediate claim HfaRay: apply_fun normalize01_fun t ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ apply_fun normalize01_fun x ∈ open_ray_upper R a) t HtPre).
We prove the intermediate claim Hrel: order_rel R a (apply_fun normalize01_fun t).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R a x0) (apply_fun normalize01_fun t) HfaRay).
We prove the intermediate claim Haltf: Rlt a (apply_fun normalize01_fun t).
An exact proof term for the current goal is (order_rel_R_implies_Rlt a (apply_fun normalize01_fun t) Hrel).
We prove the intermediate claim H1leA: Rle 1 a.
An exact proof term for the current goal is (RleI 1 a real_1 HaR Hnlt1).
We prove the intermediate claim H1ltf: Rlt 1 (apply_fun normalize01_fun t).
An exact proof term for the current goal is (Rle_Rlt_tra 1 a (apply_fun normalize01_fun t) H1leA Haltf).
An exact proof term for the current goal is (Hnlt1f H1ltf).
Let t be given.
Assume HtE: t ∈ Empty.
We will prove t ∈ preimage_of R normalize01_fun (open_ray_upper R a).
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE t HtE).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is (topology_has_empty R R_standard_topology R_standard_topology_is_topology).
∎