Let b be given.
Assume HbR: b ∈ R.
We will prove preimage_of R normalize01_fun (open_ray_lower R b) ∈ R_standard_topology.
Apply xm (Rlt 1 b) to the current goal.
Assume H1ltb: Rlt 1 b.
We prove the intermediate claim HpreEq: preimage_of R normalize01_fun (open_ray_lower R b) = R.
Apply set_ext to the current goal.
Let t be given.
Assume HtPre: t ∈ preimage_of R normalize01_fun (open_ray_lower R b).
An exact proof term for the current goal is (SepE1 R (λx : set ⇒ apply_fun normalize01_fun x ∈ open_ray_lower R b) 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 Hnlt1: ¬ (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 Hle: Rle (apply_fun normalize01_fun t) 1.
An exact proof term for the current goal is (RleI (apply_fun normalize01_fun t) 1 HfR real_1 Hnlt1).
We prove the intermediate claim Hlt: Rlt (apply_fun normalize01_fun t) b.
An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun normalize01_fun t) 1 b Hle H1ltb).
We prove the intermediate claim Hrel: order_rel R (apply_fun normalize01_fun t) b.
An exact proof term for the current goal is (Rlt_implies_order_rel_R (apply_fun normalize01_fun t) b Hlt).
We prove the intermediate claim HftRay: apply_fun normalize01_fun t ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepI R (λx : set ⇒ order_rel R x b) (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_lower R b) 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 Hnlt1: ¬ (Rlt 1 b).
Apply xm (Rlt 0 b) to the current goal.
Assume H0ltb: Rlt 0 b.
An exact proof term for the current goal is (normalize01_fun_preimage_open_ray_lower_mid b HbR Hnlt1 H0ltb).
Assume Hnlt0: ¬ (Rlt 0 b).
We prove the intermediate claim HpreEq: preimage_of R normalize01_fun (open_ray_lower R b) = Empty.
Apply set_ext to the current goal.
Let t be given.
Assume HtPre: t ∈ preimage_of R normalize01_fun (open_ray_lower R b).
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_lower R b) 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 Hnltf0: ¬ (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 HfaRay: apply_fun normalize01_fun t ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ apply_fun normalize01_fun x ∈ open_ray_lower R b) t HtPre).
We prove the intermediate claim Hrel: order_rel R (apply_fun normalize01_fun t) b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 b) (apply_fun normalize01_fun t) HfaRay).
We prove the intermediate claim Hlt: Rlt (apply_fun normalize01_fun t) b.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun normalize01_fun t) b Hrel).
We prove the intermediate claim Hb0: Rle b 0.
An exact proof term for the current goal is (RleI b 0 HbR real_0 Hnlt0).
We prove the intermediate claim Hlt0: Rlt (apply_fun normalize01_fun t) 0.
An exact proof term for the current goal is (Rlt_Rle_tra (apply_fun normalize01_fun t) b 0 Hlt Hb0).
An exact proof term for the current goal is (Hnltf0 Hlt0).
Let t be given.
Assume HtE: t ∈ Empty.
We will prove t ∈ preimage_of R normalize01_fun (open_ray_lower R b).
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).
∎