We will prove metric_on R_omega_space Romega_D_metric ∧ Romega_D_metric_topology = R_omega_product_topology.
We prove the intermediate claim Hm: metric_on R_omega_space Romega_D_metric.
We will prove metric_on R_omega_space Romega_D_metric.
We will prove ((((function_on Romega_D_metric (setprod R_omega_space R_omega_space) R ∧ (∀x y : set, x ∈ R_omega_space → y ∈ R_omega_space → apply_fun Romega_D_metric (x,y) = apply_fun Romega_D_metric (y,x))) ∧ (∀x : set, x ∈ R_omega_space → apply_fun Romega_D_metric (x,x) = 0)) ∧ (∀x y : set, x ∈ R_omega_space → y ∈ R_omega_space → ¬ (Rlt (apply_fun Romega_D_metric (x,y)) 0) ∧ (apply_fun Romega_D_metric (x,y) = 0 → x = y))) ∧ (∀x y z : set, x ∈ R_omega_space → y ∈ R_omega_space → z ∈ R_omega_space → ¬ (Rlt (add_SNo (apply_fun Romega_D_metric (x,y)) (apply_fun Romega_D_metric (y,z))) (apply_fun Romega_D_metric (x,z))))).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Romega_D_metric_function_on.
Let x and y be given.
Assume Hx: x ∈ R_omega_space.
Assume Hy: y ∈ R_omega_space.
We prove the intermediate claim Hxyprod: (x,y) ∈ setprod R_omega_space R_omega_space.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R_omega_space R_omega_space x y Hx Hy).
We prove the intermediate claim Hyxprod: (y,x) ∈ setprod R_omega_space R_omega_space.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R_omega_space R_omega_space y x Hy Hx).
rewrite the current goal using (apply_fun_graph (setprod R_omega_space R_omega_space) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)) (x,y) Hxyprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
rewrite the current goal using (apply_fun_graph (setprod R_omega_space R_omega_space) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)) (y,x) Hyxprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq y x) (from left to right).
rewrite the current goal using (tuple_2_1_eq y x) (from left to right).
An exact proof term for the current goal is (Romega_D_metric_value_sym x y Hx Hy).
Let x be given.
Assume Hx: x ∈ R_omega_space.
We prove the intermediate claim Hxxprod: (x,x) ∈ setprod R_omega_space R_omega_space.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R_omega_space R_omega_space x x Hx Hx).
rewrite the current goal using (apply_fun_graph (setprod R_omega_space R_omega_space) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)) (x,x) Hxxprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x x) (from left to right).
rewrite the current goal using (tuple_2_1_eq x x) (from left to right).
An exact proof term for the current goal is (Romega_D_metric_value_self_zero x Hx).
Let x and y be given.
Assume Hx: x ∈ R_omega_space.
Assume Hy: y ∈ R_omega_space.
Apply andI to the current goal.
We prove the intermediate claim Hxyprod: (x,y) ∈ setprod R_omega_space R_omega_space.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R_omega_space R_omega_space x y Hx Hy).
rewrite the current goal using (apply_fun_graph (setprod R_omega_space R_omega_space) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)) (x,y) Hxyprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
An exact proof term for the current goal is (Romega_D_metric_value_nonneg x y Hx Hy).
Assume H0: apply_fun Romega_D_metric (x,y) = 0.
We prove the intermediate claim Hxyprod: (x,y) ∈ setprod R_omega_space R_omega_space.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R_omega_space R_omega_space x y Hx Hy).
We prove the intermediate claim Happ: apply_fun Romega_D_metric (x,y) = Romega_D_metric_value x y.
rewrite the current goal using (apply_fun_graph (setprod R_omega_space R_omega_space) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)) (x,y) Hxyprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
Use reflexivity.
We prove the intermediate claim Hval0: Romega_D_metric_value x y = 0.
rewrite the current goal using Happ (from right to left).
An exact proof term for the current goal is H0.
We prove the intermediate claim Hcoord: ∀i : set, i ∈ ω → apply_fun x i = apply_fun y i.
Let i be given.
Assume HiO: i ∈ ω.
An exact proof term for the current goal is (Romega_D_metric_value_eq0_coord_eq x y Hx Hy Hval0 i HiO).
We will prove x = y.
Set Xi0 to be the term const_space_family ω R R_standard_topology.
Set U0 to be the term space_family_union ω Xi0.
We prove the intermediate claim HxPow: x ∈ 𝒫 (setprod ω U0).
An exact proof term for the current goal is (SepE1 (𝒫 (setprod ω U0)) (λf0 : set ⇒ (total_function_on f0 ω U0 ∧ functional_graph f0) ∧ ∀j : set, j ∈ ω → apply_fun f0 j ∈ space_family_set Xi0 j) x Hx).
We prove the intermediate claim HyPow: y ∈ 𝒫 (setprod ω U0).
An exact proof term for the current goal is (SepE1 (𝒫 (setprod ω U0)) (λf0 : set ⇒ (total_function_on f0 ω U0 ∧ functional_graph f0) ∧ ∀j : set, j ∈ ω → apply_fun f0 j ∈ space_family_set Xi0 j) y Hy).
We prove the intermediate claim HxSub: x ⊆ setprod ω U0.
An exact proof term for the current goal is (PowerE (setprod ω U0) x HxPow).
We prove the intermediate claim HySub: y ⊆ setprod ω U0.
An exact proof term for the current goal is (PowerE (setprod ω U0) y HyPow).
We prove the intermediate claim HxPack: (total_function_on x ω U0 ∧ functional_graph x) ∧ ∀j : set, j ∈ ω → apply_fun x j ∈ space_family_set Xi0 j.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod ω U0)) (λf0 : set ⇒ (total_function_on f0 ω U0 ∧ functional_graph f0) ∧ ∀j : set, j ∈ ω → apply_fun f0 j ∈ space_family_set Xi0 j) x Hx).
We prove the intermediate claim HyPack: (total_function_on y ω U0 ∧ functional_graph y) ∧ ∀j : set, j ∈ ω → apply_fun y j ∈ space_family_set Xi0 j.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod ω U0)) (λf0 : set ⇒ (total_function_on f0 ω U0 ∧ functional_graph f0) ∧ ∀j : set, j ∈ ω → apply_fun f0 j ∈ space_family_set Xi0 j) y Hy).
We prove the intermediate claim HxCore: total_function_on x ω U0 ∧ functional_graph x.
An exact proof term for the current goal is (andEL (total_function_on x ω U0 ∧ functional_graph x) (∀j : set, j ∈ ω → apply_fun x j ∈ space_family_set Xi0 j) HxPack).
We prove the intermediate claim HyCore: total_function_on y ω U0 ∧ functional_graph y.
An exact proof term for the current goal is (andEL (total_function_on y ω U0 ∧ functional_graph y) (∀j : set, j ∈ ω → apply_fun y j ∈ space_family_set Xi0 j) HyPack).
We prove the intermediate claim HxTot: total_function_on x ω U0.
An exact proof term for the current goal is (andEL (total_function_on x ω U0) (functional_graph x) HxCore).
We prove the intermediate claim HxFG: functional_graph x.
An exact proof term for the current goal is (andER (total_function_on x ω U0) (functional_graph x) HxCore).
We prove the intermediate claim HyTot: total_function_on y ω U0.
An exact proof term for the current goal is (andEL (total_function_on y ω U0) (functional_graph y) HyCore).
We prove the intermediate claim HyFG: functional_graph y.
An exact proof term for the current goal is (andER (total_function_on y ω U0) (functional_graph y) HyCore).
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ x.
We will prove p ∈ y.
We prove the intermediate claim HpXY: p ∈ setprod ω U0.
An exact proof term for the current goal is (HxSub p Hp).
We prove the intermediate claim Heta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta ω U0 p HpXY).
We prove the intermediate claim Hp0: p 0 ∈ ω.
An exact proof term for the current goal is (ap0_Sigma ω (λ_ : set ⇒ U0) p HpXY).
We prove the intermediate claim Hp1: p 1 ∈ U0.
An exact proof term for the current goal is (ap1_Sigma ω (λ_ : set ⇒ U0) p HpXY).
We prove the intermediate claim Hpair: (p 0,p 1) ∈ x.
rewrite the current goal using Heta (from right to left).
An exact proof term for the current goal is Hp.
We prove the intermediate claim Happx: apply_fun x (p 0) = (p 1).
An exact proof term for the current goal is (functional_graph_apply_fun_eq x (p 0) (p 1) HxFG Hpair).
We prove the intermediate claim Hxy: apply_fun y (p 0) = apply_fun x (p 0).
Use symmetry.
An exact proof term for the current goal is (Hcoord (p 0) Hp0).
We prove the intermediate claim Happy: apply_fun y (p 0) = (p 1).
rewrite the current goal using Hxy (from left to right).
An exact proof term for the current goal is Happx.
We prove the intermediate claim Hypair: (p 0,apply_fun y (p 0)) ∈ y.
An exact proof term for the current goal is (total_function_on_apply_fun_in_graph y ω U0 (p 0) HyTot Hp0).
We prove the intermediate claim Hpeq: (p 0,apply_fun y (p 0)) = (p 0,p 1).
rewrite the current goal using Happy (from left to right).
Use reflexivity.
rewrite the current goal using Heta (from left to right).
rewrite the current goal using Hpeq (from right to left).
An exact proof term for the current goal is Hypair.
Let p be given.
Assume Hp: p ∈ y.
We will prove p ∈ x.
We prove the intermediate claim HpXY: p ∈ setprod ω U0.
An exact proof term for the current goal is (HySub p Hp).
We prove the intermediate claim Heta: p = (p 0,p 1).
An exact proof term for the current goal is (setprod_eta ω U0 p HpXY).
We prove the intermediate claim Hp0: p 0 ∈ ω.
An exact proof term for the current goal is (ap0_Sigma ω (λ_ : set ⇒ U0) p HpXY).
We prove the intermediate claim Hp1: p 1 ∈ U0.
An exact proof term for the current goal is (ap1_Sigma ω (λ_ : set ⇒ U0) p HpXY).
We prove the intermediate claim Hpair: (p 0,p 1) ∈ y.
rewrite the current goal using Heta (from right to left).
An exact proof term for the current goal is Hp.
We prove the intermediate claim Happy: apply_fun y (p 0) = (p 1).
An exact proof term for the current goal is (functional_graph_apply_fun_eq y (p 0) (p 1) HyFG Hpair).
We prove the intermediate claim Hyx: apply_fun x (p 0) = apply_fun y (p 0).
An exact proof term for the current goal is (Hcoord (p 0) Hp0).
We prove the intermediate claim Happx: apply_fun x (p 0) = (p 1).
rewrite the current goal using Hyx (from left to right).
An exact proof term for the current goal is Happy.
We prove the intermediate claim Hxpair: (p 0,apply_fun x (p 0)) ∈ x.
An exact proof term for the current goal is (total_function_on_apply_fun_in_graph x ω U0 (p 0) HxTot Hp0).
We prove the intermediate claim Hpeq: (p 0,apply_fun x (p 0)) = (p 0,p 1).
rewrite the current goal using Happx (from left to right).
Use reflexivity.
rewrite the current goal using Heta (from left to right).
rewrite the current goal using Hpeq (from right to left).
An exact proof term for the current goal is Hxpair.
Let x, y and z be given.
Assume Hx: x ∈ R_omega_space.
Assume Hy: y ∈ R_omega_space.
Assume Hz: z ∈ R_omega_space.
We prove the intermediate claim Hxyprod: (x,y) ∈ setprod R_omega_space R_omega_space.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R_omega_space R_omega_space x y Hx Hy).
We prove the intermediate claim Hyzprod: (y,z) ∈ setprod R_omega_space R_omega_space.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R_omega_space R_omega_space y z Hy Hz).
We prove the intermediate claim Hxzprod: (x,z) ∈ setprod R_omega_space R_omega_space.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R_omega_space R_omega_space x z Hx Hz).
rewrite the current goal using (apply_fun_graph (setprod R_omega_space R_omega_space) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)) (x,y) Hxyprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x y) (from left to right).
rewrite the current goal using (tuple_2_1_eq x y) (from left to right).
rewrite the current goal using (apply_fun_graph (setprod R_omega_space R_omega_space) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)) (y,z) Hyzprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq y z) (from left to right).
rewrite the current goal using (tuple_2_1_eq y z) (from left to right).
rewrite the current goal using (apply_fun_graph (setprod R_omega_space R_omega_space) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)) (x,z) Hxzprod) (from left to right).
rewrite the current goal using (tuple_2_0_eq x z) (from left to right).
rewrite the current goal using (tuple_2_1_eq x z) (from left to right).
An exact proof term for the current goal is (Romega_D_metric_value_triangle x y z Hx Hy Hz).
Apply andI to the current goal.
An exact proof term for the current goal is Hm.
We will prove Romega_D_metric_topology = R_omega_product_topology.
Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ Romega_D_metric_topology.
We will prove U ∈ R_omega_product_topology.
Set X to be the term R_omega_space.
Set d to be the term Romega_D_metric.
Set B to be the term famunion X (λx0 : set ⇒ {open_ball X d x0 r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim HTprod: topology_on X R_omega_product_topology.
An exact proof term for the current goal is Romega_product_topology_is_topology.
We prove the intermediate claim Hballsub: ∀b ∈ B, b ∈ R_omega_product_topology.
Let b be given.
Assume HbB: b ∈ B.
Apply (famunionE_impred X (λx0 : set ⇒ {open_ball X d x0 r|r ∈ R, Rlt 0 r}) b HbB (b ∈ R_omega_product_topology)) to the current goal.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Assume HbIn: b ∈ {open_ball X d x0 r|r ∈ R, Rlt 0 r}.
Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d x0 r0) b HbIn (b ∈ R_omega_product_topology)) to the current goal.
Let r0 be given.
Assume Hr0R: r0 ∈ R.
Assume Hr0pos: Rlt 0 r0.
Assume Hbeq: b = open_ball X d x0 r0.
rewrite the current goal using Hbeq (from left to right).
An exact proof term for the current goal is (Romega_D_metric_open_ball_in_product_topology x0 r0 Hm Hx0X Hr0R Hr0pos).
We prove the intermediate claim Hfiner: finer_than R_omega_product_topology (generated_topology X B).
An exact proof term for the current goal is (generated_topology_finer_weak X B R_omega_product_topology HTprod Hballsub).
We prove the intermediate claim Hinc: generated_topology X B ⊆ R_omega_product_topology.
An exact proof term for the current goal is Hfiner.
We prove the intermediate claim Hdef: Romega_D_metric_topology = generated_topology X B.
Use reflexivity.
We prove the intermediate claim HUgen: U ∈ generated_topology X B.
rewrite the current goal using Hdef (from right to left).
An exact proof term for the current goal is HU.
An exact proof term for the current goal is (Hinc U HUgen).
Let U be given.
Assume HU: U ∈ R_omega_product_topology.
We will prove U ∈ Romega_D_metric_topology.
Set X to be the term R_omega_space.
Set d to be the term Romega_D_metric.
Set Xi0 to be the term const_space_family ω R R_standard_topology.
Set S to be the term product_subbasis_full ω Xi0.
We prove the intermediate claim HdefProd: R_omega_product_topology = generated_topology_from_subbasis X S.
Use reflexivity.
We prove the intermediate claim Hone: ω ≠ Empty.
We prove the intermediate claim H0o: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
An exact proof term for the current goal is (elem_implies_nonempty ω 0 H0o).
We prove the intermediate claim Hcomp: ∀i : set, i ∈ ω → topology_on (space_family_set Xi0 i) (space_family_topology Xi0 i).
Let i be given.
Assume Hi: i ∈ ω.
We prove the intermediate claim HXi: apply_fun Xi0 i = (R,R_standard_topology).
An exact proof term for the current goal is (const_space_family_apply ω R R_standard_topology i Hi).
We prove the intermediate claim Hset: space_family_set Xi0 i = R.
We prove the intermediate claim Hdef: space_family_set Xi0 i = (apply_fun Xi0 i) 0.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using HXi (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq R R_standard_topology).
We prove the intermediate claim Htop: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology.
rewrite the current goal using Hset (from left to right).
We prove the intermediate claim HtopEq: space_family_topology Xi0 i = R_standard_topology.
We prove the intermediate claim Hdef: space_family_topology Xi0 i = (apply_fun Xi0 i) 1.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using HXi (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq R R_standard_topology).
rewrite the current goal using HtopEq (from left to right).
An exact proof term for the current goal is Htop.
We prove the intermediate claim HSsub: subbasis_on X S.
An exact proof term for the current goal is (product_subbasis_full_subbasis_on ω Xi0 Hone Hcomp).
We prove the intermediate claim HTm: topology_on X Romega_D_metric_topology.
An exact proof term for the current goal is (metric_topology_is_topology X d Hm).
We prove the intermediate claim HSc: S ⊆ Romega_D_metric_topology.
Let s be given.
Assume HsS: s ∈ S.
We will prove s ∈ Romega_D_metric_topology.
Apply (famunionE_impred ω (λi : set ⇒ {product_cylinder ω Xi0 i U|U ∈ space_family_topology Xi0 i}) s HsS (s ∈ Romega_D_metric_topology)) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
Assume Hsi: s ∈ {product_cylinder ω Xi0 i U|U ∈ space_family_topology Xi0 i}.
Apply (ReplE_impred (space_family_topology Xi0 i) (λU0 : set ⇒ product_cylinder ω Xi0 i U0) s Hsi) to the current goal.
Let U0 be given.
Assume HU0Top: U0 ∈ space_family_topology Xi0 i.
Assume Hseq: s = product_cylinder ω Xi0 i U0.
rewrite the current goal using Hseq (from left to right).
We prove the intermediate claim HtopEq: space_family_topology Xi0 i = R_standard_topology.
We prove the intermediate claim HXi: apply_fun Xi0 i = (R,R_standard_topology).
An exact proof term for the current goal is (const_space_family_apply ω R R_standard_topology i Hi).
We prove the intermediate claim Hdef: space_family_topology Xi0 i = (apply_fun Xi0 i) 1.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using HXi (from left to right).
An exact proof term for the current goal is (tuple_2_1_eq R R_standard_topology).
We prove the intermediate claim HU0std: U0 ∈ R_standard_topology.
rewrite the current goal using HtopEq (from right to left).
An exact proof term for the current goal is HU0Top.
An exact proof term for the current goal is (Romega_product_cylinder_in_D_metric_topology i U0 Hm Hi HU0std).
We prove the intermediate claim Hmin: finer_than Romega_D_metric_topology (generated_topology_from_subbasis X S).
An exact proof term for the current goal is (topology_generated_by_basis_is_minimal X S Romega_D_metric_topology HSsub HTm HSc).
We prove the intermediate claim Hinc: generated_topology_from_subbasis X S ⊆ Romega_D_metric_topology.
An exact proof term for the current goal is Hmin.
We prove the intermediate claim HUgen: U ∈ generated_topology_from_subbasis X S.
rewrite the current goal using HdefProd (from right to left).
An exact proof term for the current goal is HU.
An exact proof term for the current goal is (Hinc U HUgen).
∎