Let Y and d be given.
Assume Hd: metric_on_total Y d.
Set Ty to be the term metric_topology Y d.
Set Tprod to be the term product_topology Y Ty Y Ty.
We prove the intermediate claim Hm: metric_on Y d.
An exact proof term for the current goal is (metric_on_total_imp_metric_on Y d Hd).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (metric_topology_is_topology Y d Hm).
We prove the intermediate claim HTprod: topology_on (setprod Y Y) Tprod.
An exact proof term for the current goal is (product_topology_is_topology Y Ty Y Ty HTy HTy).
We prove the intermediate claim Hfun: function_on d (setprod Y Y) R.
An exact proof term for the current goal is (metric_on_function_on Y d Hm).
Set S to be the term open_rays_subbasis R.
We prove the intermediate claim HeqTop: 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 HeqTop (from right to left).
Apply (continuous_map_from_subbasis (setprod Y Y) Tprod R S d) to the current goal.
An exact proof term for the current goal is HTprod.
An exact proof term for the current goal is Hfun.
An exact proof term for the current goal is (open_rays_subbasis_is_subbasis R).
Let s be given.
Assume HsS: s ∈ S.
We will prove preimage_of (setprod Y Y) d s ∈ Tprod.
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 (setprod Y Y) d s ∈ Tprod)) 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 (setprod Y Y) d s ∈ Tprod)) 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).
An exact proof term for the current goal is (metric_distance_preimage_open_ray_upper Y d a Hd HaR).
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).
An exact proof term for the current goal is (metric_distance_preimage_open_ray_lower Y d b Hd HbR).
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).
rewrite the current goal using (preimage_of_whole (setprod Y Y) R d Hfun) (from left to right).
An exact proof term for the current goal is (topology_has_X (setprod Y Y) Tprod HTprod).
An exact proof term for the current goal is HsS.
∎