Let k be given.
Assume HkO: k ∈ ω.
We will prove complete_metric_space (euclidean_space k) (euclidean_metric k).
We will prove metric_on (euclidean_space k) (euclidean_metric k) ∧ ∀seq : set, sequence_on seq (euclidean_space k) → cauchy_sequence (euclidean_space k) (euclidean_metric k) seq → ∃x : set, converges_to (euclidean_space k) (metric_topology (euclidean_space k) (euclidean_metric k)) seq x.
Apply andI to the current goal.
An exact proof term for the current goal is (euclidean_metric_is_metric_on k HkO).
Let seq be given.
Assume Hseq: sequence_on seq (euclidean_space k).
Assume Hc: cauchy_sequence (euclidean_space k) (euclidean_metric k) seq.
Set extseq to be the term graph ω (λn : set ⇒ euclidean_space_extend_to_Romega k (apply_fun seq n)).
We prove the intermediate claim Hextseq_on: sequence_on extseq R_omega_space.
Let n be given.
Assume HnO: n ∈ ω.
We will prove apply_fun extseq n ∈ R_omega_space.
We prove the intermediate claim Hseqn: apply_fun seq n ∈ euclidean_space k.
An exact proof term for the current goal is (Hseq n HnO).
rewrite the current goal using (apply_fun_graph ω (λm : set ⇒ euclidean_space_extend_to_Romega k (apply_fun seq m)) n HnO) (from left to right).
An exact proof term for the current goal is (euclidean_space_extend_to_Romega_in_Romega_space k (apply_fun seq n) Hseqn).
We prove the intermediate claim HmD: metric_on R_omega_space Romega_D_metric.
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).
We prove the intermediate claim Hcauch: ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun (euclidean_metric k) (apply_fun seq m,apply_fun seq n)) eps.
An exact proof term for the current goal is (andER (metric_on (euclidean_space k) (euclidean_metric k) ∧ sequence_on seq (euclidean_space k)) (∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun (euclidean_metric k) (apply_fun seq m,apply_fun seq n)) eps) Hc).
We prove the intermediate claim Hextseq_cauchy: cauchy_sequence R_omega_space Romega_D_metric extseq.
We will prove metric_on R_omega_space Romega_D_metric ∧ sequence_on extseq R_omega_space ∧ ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun Romega_D_metric (apply_fun extseq m,apply_fun extseq n)) eps.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HmD.
An exact proof term for the current goal is Hextseq_on.
Let eps be given.
Assume Heps: eps ∈ R ∧ Rlt 0 eps.
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ ∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun (euclidean_metric k) (apply_fun seq m,apply_fun seq n)) eps.
An exact proof term for the current goal is (Hcauch eps Heps).
Apply HexN to the current goal.
Let N be given.
Assume HNpack.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (N ∈ ω) (∀m n : set, m ∈ ω → n ∈ ω → N ⊆ m → N ⊆ n → Rlt (apply_fun (euclidean_metric k) (apply_fun seq m,apply_fun seq n)) eps) HNpack).
Let m and n be given.
Assume HmO: m ∈ ω.
Assume HnO: n ∈ ω.
Assume HNm: N ⊆ m.
Assume HNn: N ⊆ n.
We prove the intermediate claim Hlt: Rlt (apply_fun (euclidean_metric k) (apply_fun seq m,apply_fun seq n)) eps.
An exact proof term for the current goal is (andER (N ∈ ω) (∀m0 n0 : set, m0 ∈ ω → n0 ∈ ω → N ⊆ m0 → N ⊆ n0 → Rlt (apply_fun (euclidean_metric k) (apply_fun seq m0,apply_fun seq n0)) eps) HNpack m n HmO HnO HNm HNn).
We prove the intermediate claim Hseqm: apply_fun seq m ∈ euclidean_space k.
An exact proof term for the current goal is (Hseq m HmO).
We prove the intermediate claim Hseqn: apply_fun seq n ∈ euclidean_space k.
An exact proof term for the current goal is (Hseq n HnO).
We prove the intermediate claim Hextm: apply_fun extseq m = euclidean_space_extend_to_Romega k (apply_fun seq m).
rewrite the current goal using (apply_fun_graph ω (λt : set ⇒ euclidean_space_extend_to_Romega k (apply_fun seq t)) m HmO) (from left to right).
Use reflexivity.
We prove the intermediate claim Hextn: apply_fun extseq n = euclidean_space_extend_to_Romega k (apply_fun seq n).
rewrite the current goal using (apply_fun_graph ω (λt : set ⇒ euclidean_space_extend_to_Romega k (apply_fun seq t)) n HnO) (from left to right).
Use reflexivity.
We prove the intermediate claim HmR: apply_fun extseq m ∈ R_omega_space.
An exact proof term for the current goal is (Hextseq_on m HmO).
We prove the intermediate claim HnR: apply_fun extseq n ∈ R_omega_space.
An exact proof term for the current goal is (Hextseq_on n HnO).
We prove the intermediate claim Hpair: (apply_fun extseq m,apply_fun extseq n) ∈ 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 (apply_fun extseq m) (apply_fun extseq n) HmR HnR).
We prove the intermediate claim HappD: apply_fun Romega_D_metric (apply_fun extseq m,apply_fun extseq n) = Romega_D_metric_value (apply_fun extseq m) (apply_fun extseq n).
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)) (apply_fun extseq m,apply_fun extseq n) Hpair) (from left to right).
rewrite the current goal using (tuple_2_0_eq (apply_fun extseq m) (apply_fun extseq n)) (from left to right).
rewrite the current goal using (tuple_2_1_eq (apply_fun extseq m) (apply_fun extseq n)) (from left to right).
Use reflexivity.
We prove the intermediate claim Hdk: apply_fun (euclidean_metric k) (apply_fun seq m,apply_fun seq n) = Romega_D_metric_value (euclidean_space_extend_to_Romega k (apply_fun seq m)) (euclidean_space_extend_to_Romega k (apply_fun seq n)).
An exact proof term for the current goal is (euclidean_metric_apply k (apply_fun seq m) (apply_fun seq n) Hseqm Hseqn).
rewrite the current goal using HappD (from left to right).
rewrite the current goal using Hextm (from left to right).
rewrite the current goal using Hextn (from left to right).
rewrite the current goal using Hdk (from right to left).
An exact proof term for the current goal is Hlt.
We prove the intermediate claim Hexx: ∃x : set, converges_to R_omega_space (metric_topology R_omega_space Romega_D_metric) extseq x.
We prove the intermediate claim HRconv: ∀seq0 : set, sequence_on seq0 R_omega_space → cauchy_sequence R_omega_space Romega_D_metric seq0 → ∃x0 : set, converges_to R_omega_space (metric_topology R_omega_space Romega_D_metric) seq0 x0.
An exact proof term for the current goal is (andER (metric_on R_omega_space Romega_D_metric) (∀seq0 : set, sequence_on seq0 R_omega_space → cauchy_sequence R_omega_space Romega_D_metric seq0 → ∃x0 : set, converges_to R_omega_space (metric_topology R_omega_space Romega_D_metric) seq0 x0) Romega_D_metric_complete).
An exact proof term for the current goal is (HRconv extseq Hextseq_on Hextseq_cauchy).
Apply Hexx to the current goal.
Let x be given.
Assume Hxconv: converges_to R_omega_space (metric_topology R_omega_space Romega_D_metric) extseq x.
We prove the intermediate claim HxX: x ∈ R_omega_space.
An exact proof term for the current goal is (converges_to_point_in_X R_omega_space (metric_topology R_omega_space Romega_D_metric) extseq x Hxconv).
We prove the intermediate claim Hexy: ∃y : set, y ∈ euclidean_space k ∧ euclidean_space_extend_to_Romega k y = x.
Set XiO to be the term const_space_family ω R R_standard_topology.
Set U0 to be the term space_family_union ω XiO.
We prove the intermediate claim HtopEq0: 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 HtopDef0: Romega_D_metric_topology = metric_topology R_omega_space Romega_D_metric.
Use reflexivity.
We prove the intermediate claim HMTprod: metric_topology R_omega_space Romega_D_metric = R_omega_product_topology.
rewrite the current goal using HtopDef0 (from right to left) at position 1.
An exact proof term for the current goal is HtopEq0.
We prove the intermediate claim HconvProd: converges_to R_omega_space R_omega_product_topology extseq x.
We will prove converges_to R_omega_space R_omega_product_topology extseq x.
rewrite the current goal using HMTprod (from right to left).
An exact proof term for the current goal is Hxconv.
We prove the intermediate claim HxPR: x ∈ power_real ω.
We will prove x ∈ power_real ω.
rewrite the current goal using (power_real_omega_eq_Romega_space) (from left to right).
An exact proof term for the current goal is HxX.
We prove the intermediate claim HxProp: total_function_on x ω U0 ∧ functional_graph x ∧ ∀j : set, j ∈ ω → apply_fun x j ∈ space_family_set XiO 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 XiO j) x HxPR).
We prove the intermediate claim HxAB: 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 XiO j) HxProp).
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) HxAB).
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) HxAB).
We prove the intermediate claim HxCoordSF: ∀j : set, j ∈ ω → apply_fun x j ∈ space_family_set XiO j.
An exact proof term for the current goal is (andER (total_function_on x ω U0 ∧ functional_graph x) (∀j : set, j ∈ ω → apply_fun x j ∈ space_family_set XiO j) HxProp).
We prove the intermediate claim HxcoordR: ∀j : set, j ∈ ω → apply_fun x j ∈ R.
Let j be given.
Assume HjO: j ∈ ω.
We will prove apply_fun x j ∈ R.
rewrite the current goal using (space_family_set_const_Romega j HjO) (from right to left).
An exact proof term for the current goal is (HxCoordSF j HjO).
We prove the intermediate claim HxOut0: ∀i : set, i ∈ ω → ¬ (i ∈ k) → apply_fun x i = 0.
Let i be given.
Assume HiO: i ∈ ω.
Assume Hnin: ¬ (i ∈ k).
Set pi to be the term Romega_coord_map i.
We prove the intermediate claim Hcont: continuous_map R_omega_space R_omega_product_topology R R_standard_topology pi.
An exact proof term for the current goal is (Romega_coord_map_continuous_in_Romega_product i HiO).
We prove the intermediate claim HtopX: topology_on R_omega_space R_omega_product_topology.
An exact proof term for the current goal is Romega_product_topology_is_topology.
We prove the intermediate claim HtopR: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology.
We prove the intermediate claim Hseqon: sequence_on extseq R_omega_space.
An exact proof term for the current goal is Hextseq_on.
We prove the intermediate claim Hconvpi: converges_to R R_standard_topology (map_sequence pi extseq) (apply_fun pi x).
An exact proof term for the current goal is ((first_countable_sequences_detect_continuity R_omega_space R_omega_product_topology R R_standard_topology pi HtopX HtopR Hcont) x extseq Hseqon HconvProd).
We prove the intermediate claim Happx: apply_fun pi x = apply_fun x i.
An exact proof term for the current goal is (Romega_coord_map_apply i x HiO HxX).
We prove the intermediate claim Hconv1: converges_to R R_standard_topology (map_sequence pi extseq) (apply_fun x i).
rewrite the current goal using Happx (from right to left).
An exact proof term for the current goal is Hconvpi.
We prove the intermediate claim Hconv0: converges_to R R_standard_topology (map_sequence pi extseq) 0.
We will prove topology_on R R_standard_topology ∧ sequence_on (map_sequence pi extseq) R ∧ 0 ∈ R ∧ ∀U : set, U ∈ R_standard_topology → 0 ∈ U → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun (map_sequence pi extseq) n ∈ U.
Apply and4I to the current goal.
An exact proof term for the current goal is HtopR.
We will prove sequence_on (map_sequence pi extseq) R.
Let n be given.
Assume HnO: n ∈ ω.
We will prove apply_fun (map_sequence pi extseq) n ∈ R.
We prove the intermediate claim Hseqn: apply_fun extseq n ∈ R_omega_space.
An exact proof term for the current goal is (Hextseq_on n HnO).
We prove the intermediate claim Happ: apply_fun (map_sequence pi extseq) n = apply_fun pi (apply_fun extseq n).
An exact proof term for the current goal is (compose_fun_apply ω extseq pi n HnO).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim HpiFun: function_on pi R_omega_space R.
An exact proof term for the current goal is (Romega_coord_map_function_on i HiO).
An exact proof term for the current goal is (HpiFun (apply_fun extseq n) Hseqn).
An exact proof term for the current goal is real_0.
Let U be given.
Assume HU: U ∈ R_standard_topology.
Assume H0U: 0 ∈ U.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
Let n be given.
Assume HnO: n ∈ ω.
Assume H0n: 0 ⊆ n.
We will prove apply_fun (map_sequence pi extseq) n ∈ U.
We prove the intermediate claim Happ: apply_fun (map_sequence pi extseq) n = apply_fun pi (apply_fun extseq n).
An exact proof term for the current goal is (compose_fun_apply ω extseq pi n HnO).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hextn: apply_fun extseq n = euclidean_space_extend_to_Romega k (apply_fun seq n).
rewrite the current goal using (apply_fun_graph ω (λm : set ⇒ euclidean_space_extend_to_Romega k (apply_fun seq m)) n HnO) (from left to right).
Use reflexivity.
rewrite the current goal using Hextn (from left to right).
We prove the intermediate claim Hseqn: apply_fun seq n ∈ euclidean_space k.
An exact proof term for the current goal is (Hseq n HnO).
We prove the intermediate claim HextnX: euclidean_space_extend_to_Romega k (apply_fun seq n) ∈ R_omega_space.
An exact proof term for the current goal is (euclidean_space_extend_to_Romega_in_Romega_space k (apply_fun seq n) Hseqn).
We prove the intermediate claim HappPi: apply_fun pi (euclidean_space_extend_to_Romega k (apply_fun seq n)) = apply_fun (euclidean_space_extend_to_Romega k (apply_fun seq n)) i.
An exact proof term for the current goal is (Romega_coord_map_apply i (euclidean_space_extend_to_Romega k (apply_fun seq n)) HiO HextnX).
rewrite the current goal using HappPi (from left to right).
rewrite the current goal using (euclidean_space_extend_to_Romega_apply k (apply_fun seq n) i HiO) (from left to right).
rewrite the current goal using (If_i_0 (i ∈ k) (apply_fun (apply_fun seq n) i) 0 Hnin) (from left to right).
An exact proof term for the current goal is H0U.
Apply xm (apply_fun x i = 0) to the current goal.
Assume Heq: apply_fun x i = 0.
An exact proof term for the current goal is Heq.
Assume Hneq: ¬ (apply_fun x i = 0).
Apply FalseE to the current goal.
Apply (Hausdorff_unique_limits R R_standard_topology (map_sequence pi extseq) (apply_fun x i) 0 R_standard_topology_Hausdorff (converges_to_point_in_X R R_standard_topology (map_sequence pi extseq) (apply_fun x i) Hconv1) real_0 Hneq (converges_to_sequence_on R R_standard_topology (map_sequence pi extseq) (apply_fun x i) Hconv1) (converges_to_neighborhoods R R_standard_topology (map_sequence pi extseq) (apply_fun x i) Hconv1) (converges_to_neighborhoods R R_standard_topology (map_sequence pi extseq) 0 Hconv0)) to the current goal.
Set y to be the term graph k (λj : set ⇒ apply_fun x j).
We use y to witness the existential quantifier.
Apply andI to the current goal.
Set XiK to be the term const_space_family k R R_standard_topology.
Set UK to be the term space_family_union k XiK.
We will prove y ∈ product_space k XiK.
We will prove y ∈ {f ∈ 𝒫 (setprod k UK)|total_function_on f k UK ∧ functional_graph f ∧ ∀i : set, i ∈ k → apply_fun f i ∈ space_family_set XiK i}.
Apply SepI to the current goal.
Apply PowerI to the current goal.
Let p be given.
Assume Hp: p ∈ y.
We will prove p ∈ setprod k UK.
Apply (ReplE_impred k (λj : set ⇒ (j,apply_fun x j)) p Hp (p ∈ setprod k UK)) to the current goal.
Let j be given.
Assume Hj: j ∈ k.
Assume Hpeq: p = (j,apply_fun x j).
We prove the intermediate claim HjO: j ∈ ω.
We prove the intermediate claim Hsub: k ⊆ ω.
An exact proof term for the current goal is (omega_TransSet k HkO).
An exact proof term for the current goal is (Hsub j Hj).
We prove the intermediate claim HxjR: apply_fun x j ∈ R.
An exact proof term for the current goal is (HxcoordR j HjO).
We prove the intermediate claim Hset: space_family_set XiK j = R.
rewrite the current goal using (product_component_def XiK j) (from left to right) at position 1.
We prove the intermediate claim HXi: apply_fun XiK j = (R,R_standard_topology).
An exact proof term for the current goal is (const_space_family_apply k R R_standard_topology j Hj).
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 HxjU: apply_fun x j ∈ UK.
Set S to be the term {space_family_set XiK i|i ∈ k}.
We prove the intermediate claim HUdef: UK = ⋃ S.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
We prove the intermediate claim HSj: space_family_set XiK j ∈ S.
An exact proof term for the current goal is (ReplI k (λi : set ⇒ space_family_set XiK i) j Hj).
We prove the intermediate claim HxjSF: apply_fun x j ∈ space_family_set XiK j.
We will prove apply_fun x j ∈ space_family_set XiK j.
rewrite the current goal using Hset (from left to right).
An exact proof term for the current goal is HxjR.
An exact proof term for the current goal is (UnionI S (apply_fun x j) (space_family_set XiK j) HxjSF HSj).
rewrite the current goal using Hpeq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma k UK j (apply_fun x j) Hj HxjU).
We will prove total_function_on y k UK ∧ functional_graph y ∧ ∀i : set, i ∈ k → apply_fun y i ∈ space_family_set XiK i.
Apply andI to the current goal.
Apply andI to the current goal.
Apply (total_function_on_graph k UK (λj : set ⇒ apply_fun x j)) to the current goal.
Let j be given.
Assume Hj: j ∈ k.
We prove the intermediate claim HjO: j ∈ ω.
We prove the intermediate claim Hsub: k ⊆ ω.
An exact proof term for the current goal is (omega_TransSet k HkO).
An exact proof term for the current goal is (Hsub j Hj).
We prove the intermediate claim HxjR: apply_fun x j ∈ R.
An exact proof term for the current goal is (HxcoordR j HjO).
Set S to be the term {space_family_set XiK i|i ∈ k}.
We prove the intermediate claim HUdef: UK = ⋃ S.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
We prove the intermediate claim HSj: space_family_set XiK j ∈ S.
An exact proof term for the current goal is (ReplI k (λi : set ⇒ space_family_set XiK i) j Hj).
We prove the intermediate claim Hset: space_family_set XiK j = R.
We prove the intermediate claim Hsf: space_family_set XiK j = (apply_fun XiK j) 0.
Use reflexivity.
rewrite the current goal using Hsf (from left to right) at position 1.
rewrite the current goal using (const_space_family_apply k R R_standard_topology j Hj) (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 HxjSF: apply_fun x j ∈ space_family_set XiK j.
We will prove apply_fun x j ∈ space_family_set XiK j.
rewrite the current goal using Hset (from left to right).
An exact proof term for the current goal is HxjR.
An exact proof term for the current goal is (UnionI S (apply_fun x j) (space_family_set XiK j) HxjSF HSj).
An exact proof term for the current goal is (functional_graph_graph k (λj : set ⇒ apply_fun x j)).
Let i be given.
Assume Hi: i ∈ k.
We will prove apply_fun y i ∈ space_family_set XiK i.
We prove the intermediate claim HiO: i ∈ ω.
We prove the intermediate claim Hsub: k ⊆ ω.
An exact proof term for the current goal is (omega_TransSet k HkO).
An exact proof term for the current goal is (Hsub i Hi).
We prove the intermediate claim Happ: apply_fun y i = apply_fun x i.
rewrite the current goal using (apply_fun_graph k (λj : set ⇒ apply_fun x j) i Hi) (from left to right).
Use reflexivity.
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim HxiR: apply_fun x i ∈ R.
An exact proof term for the current goal is (HxcoordR i HiO).
We prove the intermediate claim Hset: space_family_set XiK i = R.
We prove the intermediate claim Hsf: space_family_set XiK i = (apply_fun XiK i) 0.
Use reflexivity.
rewrite the current goal using Hsf (from left to right) at position 1.
rewrite the current goal using (const_space_family_apply k R R_standard_topology i Hi) (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq R R_standard_topology).
rewrite the current goal using Hset (from left to right).
An exact proof term for the current goal is HxiR.
We will prove euclidean_space_extend_to_Romega k y = x.
Set h to be the term (λi : set ⇒ If_i (i ∈ k) (apply_fun y i) 0).
We prove the intermediate claim HdefExt: euclidean_space_extend_to_Romega k y = graph ω h.
Use reflexivity.
rewrite the current goal using HdefExt (from left to right).
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ graph ω h.
We will prove p ∈ x.
Apply (ReplE_impred ω (λi : set ⇒ (i,h i)) p Hp (p ∈ x)) to the current goal.
Let i be given.
Assume HiO: i ∈ ω.
Assume Hpeq: p = (i,h i).
We prove the intermediate claim Hxpair: (i,apply_fun x i) ∈ x.
An exact proof term for the current goal is (total_function_on_apply_fun_in_graph x ω U0 i HxTot HiO).
We prove the intermediate claim Heqh: h i = apply_fun x i.
Apply xm (i ∈ k) to the current goal.
Assume Hik: i ∈ k.
We prove the intermediate claim Hdefhi: h i = If_i (i ∈ k) (apply_fun y i) 0.
Use reflexivity.
rewrite the current goal using Hdefhi (from left to right).
rewrite the current goal using (If_i_1 (i ∈ k) (apply_fun y i) 0 Hik) (from left to right).
rewrite the current goal using (apply_fun_graph k (λj : set ⇒ apply_fun x j) i Hik) (from left to right).
Use reflexivity.
Assume Hnik: ¬ (i ∈ k).
We prove the intermediate claim Hdefhi: h i = If_i (i ∈ k) (apply_fun y i) 0.
Use reflexivity.
rewrite the current goal using Hdefhi (from left to right).
rewrite the current goal using (If_i_0 (i ∈ k) (apply_fun y i) 0 Hnik) (from left to right).
rewrite the current goal using (HxOut0 i HiO Hnik) (from left to right).
Use reflexivity.
rewrite the current goal using Hpeq (from left to right).
rewrite the current goal using Heqh (from left to right).
An exact proof term for the current goal is Hxpair.
Let p be given.
Assume Hp: p ∈ x.
We will prove p ∈ graph ω h.
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 XiO j) x HxPR).
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 HpProd: p ∈ setprod ω U0.
An exact proof term for the current goal is (HxSub p Hp).
We prove the intermediate claim HiO: (p 0) ∈ ω.
An exact proof term for the current goal is (ap0_Sigma ω (λ_ : set ⇒ U0) p HpProd).
We prove the intermediate claim Htupeq: (p 0,p 1) = p.
Apply (Sigma_E ω (λ_ : set ⇒ U0) p HpProd) to the current goal.
Let n be given.
Assume Hn_pair.
Apply Hn_pair to the current goal.
Assume Hn: n ∈ ω.
Assume Hrest.
Apply Hrest to the current goal.
Let y0 be given.
Assume Hy_pair.
Apply Hy_pair to the current goal.
Assume Hy0: y0 ∈ U0.
Assume Hpdef.
rewrite the current goal using Hpdef (from left to right).
rewrite the current goal using (pair_ap_0 n y0) (from left to right).
rewrite the current goal using (pair_ap_1 n y0) (from left to right).
rewrite the current goal using (tuple_pair n y0) (from left to right).
Use reflexivity.
We prove the intermediate claim Hpair: (p 0,p 1) ∈ x.
We will prove (p 0,p 1) ∈ x.
rewrite the current goal using Htupeq (from left to right).
An exact proof term for the current goal is Hp.
We prove the intermediate claim Happ: 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 Heqh: h (p 0) = p 1.
rewrite the current goal using Happ (from right to left).
Apply xm ((p 0) ∈ k) to the current goal.
Assume Hik: (p 0) ∈ k.
We prove the intermediate claim Hdefh0: h (p 0) = If_i ((p 0) ∈ k) (apply_fun y (p 0)) 0.
Use reflexivity.
rewrite the current goal using Hdefh0 (from left to right).
rewrite the current goal using (If_i_1 ((p 0) ∈ k) (apply_fun y (p 0)) 0 Hik) (from left to right).
rewrite the current goal using (apply_fun_graph k (λj : set ⇒ apply_fun x j) (p 0) Hik) (from left to right).
Use reflexivity.
Assume Hnik: ¬ ((p 0) ∈ k).
We prove the intermediate claim Hdefh0: h (p 0) = If_i ((p 0) ∈ k) (apply_fun y (p 0)) 0.
Use reflexivity.
rewrite the current goal using Hdefh0 (from left to right).
rewrite the current goal using (If_i_0 ((p 0) ∈ k) (apply_fun y (p 0)) 0 Hnik) (from left to right).
rewrite the current goal using (HxOut0 (p 0) HiO Hnik) (from left to right).
Use reflexivity.
rewrite the current goal using Htupeq (from right to left) at position 1.
rewrite the current goal using Heqh (from right to left) at position 1.
An exact proof term for the current goal is (ReplI ω (λi : set ⇒ (i,h i)) (p 0) HiO).
Apply Hexy to the current goal.
Let y be given.
Assume Hypack.
We use y to witness the existential quantifier.
We prove the intermediate claim HyE: y ∈ euclidean_space k.
An exact proof term for the current goal is (andEL (y ∈ euclidean_space k) (euclidean_space_extend_to_Romega k y = x) Hypack).
We prove the intermediate claim Hyext: euclidean_space_extend_to_Romega k y = x.
An exact proof term for the current goal is (andER (y ∈ euclidean_space k) (euclidean_space_extend_to_Romega k y = x) Hypack).
We prove the intermediate claim HmE: metric_on (euclidean_space k) (euclidean_metric k).
An exact proof term for the current goal is (euclidean_metric_is_metric_on k HkO).
We prove the intermediate claim Hseqconv: sequence_converges_metric (euclidean_space k) (euclidean_metric k) seq y.
We will prove metric_on (euclidean_space k) (euclidean_metric k) ∧ sequence_on seq (euclidean_space k) ∧ y ∈ euclidean_space k ∧ ∀eps : set, eps ∈ R ∧ Rlt 0 eps → ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → Rlt (apply_fun (euclidean_metric k) (apply_fun seq n,y)) eps.
Apply and4I to the current goal.
An exact proof term for the current goal is HmE.
An exact proof term for the current goal is Hseq.
An exact proof term for the current goal is HyE.
Let eps be given.
Assume Heps: eps ∈ R ∧ Rlt 0 eps.
Set X0 to be the term R_omega_space.
Set d0 to be the term Romega_D_metric.
We prove the intermediate claim Hm0: metric_on X0 d0.
An exact proof term for the current goal is HmD.
We prove the intermediate claim HballOpen: open_ball X0 d0 x eps ∈ metric_topology X0 d0.
We prove the intermediate claim HepsR: eps ∈ R.
An exact proof term for the current goal is (andEL (eps ∈ R) (Rlt 0 eps) Heps).
We prove the intermediate claim Hepspos: Rlt 0 eps.
An exact proof term for the current goal is (andER (eps ∈ R) (Rlt 0 eps) Heps).
An exact proof term for the current goal is (open_ball_in_metric_topology X0 d0 x eps Hm0 HxX Hepspos).
We prove the intermediate claim Hcenter: x ∈ open_ball X0 d0 x eps.
We prove the intermediate claim Hepspos: Rlt 0 eps.
An exact proof term for the current goal is (andER (eps ∈ R) (Rlt 0 eps) Heps).
An exact proof term for the current goal is (center_in_open_ball X0 d0 x eps Hm0 HxX Hepspos).
We prove the intermediate claim HexN: ∃N : set, N ∈ ω ∧ ∀n : set, n ∈ ω → N ⊆ n → apply_fun extseq n ∈ open_ball X0 d0 x eps.
An exact proof term for the current goal is (converges_to_neighborhoods X0 (metric_topology X0 d0) extseq x Hxconv (open_ball X0 d0 x eps) HballOpen Hcenter).
Apply HexN to the current goal.
Let N be given.
Assume HNpack.
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (N ∈ ω) (∀n : set, n ∈ ω → N ⊆ n → apply_fun extseq n ∈ open_ball X0 d0 x eps) HNpack).
Let n be given.
Assume HnO: n ∈ ω.
Assume HNn: N ⊆ n.
We prove the intermediate claim HextnIn: apply_fun extseq n ∈ open_ball X0 d0 x eps.
An exact proof term for the current goal is (andER (N ∈ ω) (∀n0 : set, n0 ∈ ω → N ⊆ n0 → apply_fun extseq n0 ∈ open_ball X0 d0 x eps) HNpack n HnO HNn).
We prove the intermediate claim HextnX: apply_fun extseq n ∈ X0.
An exact proof term for the current goal is (open_ballE1 X0 d0 x eps (apply_fun extseq n) HextnIn).
We prove the intermediate claim Hlt0: Rlt (apply_fun d0 (x,apply_fun extseq n)) eps.
An exact proof term for the current goal is (open_ballE2 X0 d0 x eps (apply_fun extseq n) HextnIn).
We prove the intermediate claim Hsym0: apply_fun d0 (apply_fun extseq n,x) = apply_fun d0 (x,apply_fun extseq n).
An exact proof term for the current goal is (metric_on_symmetric X0 d0 (apply_fun extseq n) x Hm0 HextnX HxX).
We prove the intermediate claim Hlt1: Rlt (apply_fun d0 (apply_fun extseq n,x)) eps.
rewrite the current goal using Hsym0 (from left to right).
An exact proof term for the current goal is Hlt0.
We prove the intermediate claim Hseqn: apply_fun seq n ∈ euclidean_space k.
An exact proof term for the current goal is (Hseq n HnO).
We prove the intermediate claim HextnEq: apply_fun extseq n = euclidean_space_extend_to_Romega k (apply_fun seq n).
rewrite the current goal using (apply_fun_graph ω (λt : set ⇒ euclidean_space_extend_to_Romega k (apply_fun seq t)) n HnO) (from left to right).
Use reflexivity.
We prove the intermediate claim Hpair0: (apply_fun extseq n,x) ∈ setprod X0 X0.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X0 X0 (apply_fun extseq n) x HextnX HxX).
We prove the intermediate claim Happ0: apply_fun d0 (apply_fun extseq n,x) = Romega_D_metric_value (apply_fun extseq n) x.
rewrite the current goal using (apply_fun_graph (setprod X0 X0) (λp : set ⇒ Romega_D_metric_value (p 0) (p 1)) (apply_fun extseq n,x) Hpair0) (from left to right).
rewrite the current goal using (tuple_2_0_eq (apply_fun extseq n) x) (from left to right).
rewrite the current goal using (tuple_2_1_eq (apply_fun extseq n) x) (from left to right).
Use reflexivity.
We prove the intermediate claim Hdk: apply_fun (euclidean_metric k) (apply_fun seq n,y) = Romega_D_metric_value (euclidean_space_extend_to_Romega k (apply_fun seq n)) (euclidean_space_extend_to_Romega k y).
An exact proof term for the current goal is (euclidean_metric_apply k (apply_fun seq n) y Hseqn HyE).
rewrite the current goal using Hdk (from left to right).
rewrite the current goal using Hyext (from left to right).
rewrite the current goal using HextnEq (from right to left).
rewrite the current goal using Happ0 (from right to left).
An exact proof term for the current goal is Hlt1.
We prove the intermediate claim Htop: converges_to (euclidean_space k) (metric_topology (euclidean_space k) (euclidean_metric k)) seq y.
An exact proof term for the current goal is (sequence_converges_metric_imp_converges_to_metric_topology (euclidean_space k) (euclidean_metric k) seq y Hseqconv).
An exact proof term for the current goal is Htop.
∎