rewrite the current goal using (power_real_omega_eq_Romega_space) (from left to right).
rewrite the current goal using (bounded_product_metric_eq_Romega_D_metric) (from left to right).
We will prove metric_on R_omega_space Romega_D_metric ∧ ∀seq : set, sequence_on seq R_omega_space → cauchy_sequence R_omega_space Romega_D_metric seq → ∃x : set, converges_to R_omega_space (metric_topology R_omega_space Romega_D_metric) seq x.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (metric_on R_omega_space Romega_D_metric) (Romega_D_metric_topology = R_omega_product_topology) Romega_D_metric_induces_product_topology).
Let seq be given.
Assume Hseq: sequence_on seq R_omega_space.
Assume Hc: cauchy_sequence R_omega_space Romega_D_metric seq.
Set g to be the term λj : set ⇒ Eps_i (λa : set ⇒ converges_to R (metric_topology R R_bounded_metric) (product_coordinate_sequence seq j) a).
Set x to be the term graph ω g.
We prove the intermediate claim HxX: x ∈ R_omega_space.
Apply (graph_omega_to_R_in_Romega_space g) to the current goal.
Let j be given.
Assume HjO: j ∈ ω.
We will prove g j ∈ R.
Set seqj to be the term product_coordinate_sequence seq j.
We prove the intermediate claim Hcj: cauchy_sequence R R_bounded_metric seqj.
An exact proof term for the current goal is (Romega_cauchy_imp_coord_cauchy_bounded seq j Hc HjO).
We prove the intermediate claim Hseqj12: metric_on R R_bounded_metric ∧ sequence_on seqj R.
An exact proof term for the current goal is (andEL (metric_on R R_bounded_metric ∧ sequence_on seqj R) (∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun R_bounded_metric (apply_fun seqj m,apply_fun seqj n)) eps) Hcj).
We prove the intermediate claim Hseqjon: sequence_on seqj R.
An exact proof term for the current goal is (andER (metric_on R R_bounded_metric) (sequence_on seqj R) Hseqj12).
We prove the intermediate claim Hcomp2: ∀s : set, sequence_on s R → cauchy_sequence R R_bounded_metric s → ∃a : set, converges_to R (metric_topology R R_bounded_metric) s a.
An exact proof term for the current goal is (andER (metric_on R R_bounded_metric) (∀s : set, sequence_on s R → cauchy_sequence R R_bounded_metric s → ∃a : set, converges_to R (metric_topology R R_bounded_metric) s a) R_bounded_metric_complete_early).
We prove the intermediate claim Hexa: ∃a : set, converges_to R (metric_topology R R_bounded_metric) seqj a.
An exact proof term for the current goal is (Hcomp2 seqj Hseqjon Hcj).
Set a to be the term g j.
We prove the intermediate claim Ha: converges_to R (metric_topology R R_bounded_metric) seqj a.
An exact proof term for the current goal is (Eps_i_ex (λu : set ⇒ converges_to R (metric_topology R R_bounded_metric) seqj u) Hexa).
An exact proof term for the current goal is (converges_to_point_in_X R (metric_topology R R_bounded_metric) seqj a Ha).
We prove the intermediate claim Hcoord: ∀j : set, j ∈ ω → converges_to (product_component (const_space_family ω R R_standard_topology) j) (product_component_topology (const_space_family ω R R_standard_topology) j) (product_coordinate_sequence seq j) (apply_fun x j).
Let j be given.
Assume HjO: j ∈ ω.
Set Xi to be the term const_space_family ω R R_standard_topology.
Set seqj to be the term product_coordinate_sequence seq j.
Set a to be the term g j.
We prove the intermediate claim HcompX: product_component Xi j = R.
rewrite the current goal using (product_component_def Xi j) (from left to right).
rewrite the current goal using (const_space_family_apply ω R R_standard_topology j HjO) (from left to right).
rewrite the current goal using (tuple_2_0_eq R R_standard_topology) (from left to right).
Use reflexivity.
We prove the intermediate claim HcompT: product_component_topology Xi j = R_standard_topology.
rewrite the current goal using (product_component_topology_def Xi j) (from left to right).
rewrite the current goal using (const_space_family_apply ω R R_standard_topology j HjO) (from left to right).
rewrite the current goal using (tuple_2_1_eq R R_standard_topology) (from left to right).
Use reflexivity.
We prove the intermediate claim Happlyx: apply_fun x j = a.
rewrite the current goal using (apply_fun_graph ω g j HjO) (from left to right).
Use reflexivity.
We prove the intermediate claim Hexa: ∃a0 : set, converges_to R (metric_topology R R_bounded_metric) seqj a0.
We prove the intermediate claim Hcj: cauchy_sequence R R_bounded_metric seqj.
An exact proof term for the current goal is (Romega_cauchy_imp_coord_cauchy_bounded seq j Hc HjO).
We prove the intermediate claim Hseqj12: metric_on R R_bounded_metric ∧ sequence_on seqj R.
An exact proof term for the current goal is (andEL (metric_on R R_bounded_metric ∧ sequence_on seqj R) (∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun R_bounded_metric (apply_fun seqj m,apply_fun seqj n)) eps) Hcj).
We prove the intermediate claim Hseqjon: sequence_on seqj R.
An exact proof term for the current goal is (andER (metric_on R R_bounded_metric) (sequence_on seqj R) Hseqj12).
We prove the intermediate claim Hcomp2: ∀s : set, sequence_on s R → cauchy_sequence R R_bounded_metric s → ∃a1 : set, converges_to R (metric_topology R R_bounded_metric) s a1.
An exact proof term for the current goal is (andER (metric_on R R_bounded_metric) (∀s : set, sequence_on s R → cauchy_sequence R R_bounded_metric s → ∃a1 : set, converges_to R (metric_topology R R_bounded_metric) s a1) R_bounded_metric_complete_early).
An exact proof term for the current goal is (Hcomp2 seqj Hseqjon Hcj).
We prove the intermediate claim Ha: converges_to R (metric_topology R R_bounded_metric) seqj a.
An exact proof term for the current goal is (Eps_i_ex (λu : set ⇒ converges_to R (metric_topology R R_bounded_metric) seqj u) Hexa).
We prove the intermediate claim HaStd: converges_to R R_standard_topology seqj a.
rewrite the current goal using metric_topology_R_bounded_metric_eq_R_standard_topology_early (from right to left).
An exact proof term for the current goal is Ha.
rewrite the current goal using HcompX (from left to right).
rewrite the current goal using HcompT (from left to right).
rewrite the current goal using Happlyx (from left to right).
An exact proof term for the current goal is HaStd.
We prove the intermediate claim HXdef: R_omega_space = product_space ω (const_space_family ω R R_standard_topology).
Use reflexivity.
We prove the intermediate claim HconvProd: converges_to R_omega_space (product_topology_full ω (const_space_family ω R R_standard_topology)) seq x.
An exact proof term for the current goal is (iffER (converges_to R_omega_space (product_topology_full ω (const_space_family ω R R_standard_topology)) seq x) (∀j : set, j ∈ ω → converges_to (product_component (const_space_family ω R R_standard_topology) j) (product_component_topology (const_space_family ω R R_standard_topology) j) (product_coordinate_sequence seq j) (apply_fun x j)) (product_sequence_convergence_iff_coordinates R_omega_space ω HXdef seq x Hseq HxX) Hcoord).
We prove the intermediate claim HtopEq: metric_topology R_omega_space Romega_D_metric = R_omega_product_topology.
We prove the intermediate claim Heq: Romega_D_metric_topology = R_omega_product_topology.
An exact proof term for the current goal is (andER (metric_on R_omega_space Romega_D_metric) (Romega_D_metric_topology = R_omega_product_topology) Romega_D_metric_induces_product_topology).
We prove the intermediate claim HdefT: Romega_D_metric_topology = metric_topology R_omega_space Romega_D_metric.
Use reflexivity.
rewrite the current goal using HdefT (from right to left).
An exact proof term for the current goal is Heq.
We prove the intermediate claim HconvMetric: converges_to R_omega_space (metric_topology R_omega_space Romega_D_metric) seq x.
rewrite the current goal using HtopEq (from left to right).
We prove the intermediate claim HdefP: R_omega_product_topology = product_topology_full ω (const_space_family ω R R_standard_topology).
Use reflexivity.
rewrite the current goal using HdefP (from left to right).
An exact proof term for the current goal is HconvProd.
We use x to witness the existential quantifier.
An exact proof term for the current goal is HconvMetric.
∎