We will prove component_of (product_space ω (const_space_family ω R R_standard_topology)) (product_topology_full ω (const_space_family ω R R_standard_topology)) (const_family ω 0) = product_space ω (const_space_family ω R R_standard_topology) ∧ component_of (product_space ω (const_space_family ω R R_standard_topology)) (box_topology ω (const_space_family ω R R_standard_topology)) (const_family ω 0) = {f ∈ product_space ω (const_space_family ω R R_standard_topology)|∃F : set, finite F ∧ ∀i : set, i ∈ ω ∖ F → apply_fun f i = 0}.
Apply andI to the current goal.
Set Xi to be the term const_space_family ω R R_standard_topology.
Set X to be the term product_space ω Xi.
Set Tx to be the term product_topology_full ω Xi.
Set f0 to be the term const_family ω 0.
We will prove component_of X Tx f0 = X.
We prove the intermediate claim Hf0X: f0 ∈ X.
We prove the intermediate claim Hf0Eq: f0 = const_fun ω 0.
Use reflexivity.
We prove the intermediate claim H0O: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim H0inUnion: 0 ∈ space_family_union ω Xi.
We prove the intermediate claim HunionDef: space_family_union ω Xi = ⋃ {space_family_set Xi i|i ∈ ω}.
Use reflexivity.
rewrite the current goal using HunionDef (from left to right).
Set S to be the term {space_family_set Xi i|i ∈ ω}.
We prove the intermediate claim HS0: space_family_set Xi 0 ∈ S.
An exact proof term for the current goal is (ReplI ω (λi0 : set ⇒ space_family_set Xi i0) 0 H0O).
We prove the intermediate claim H0inSF0: 0 ∈ space_family_set Xi 0.
rewrite the current goal using (space_family_set_const_space_family ω R R_standard_topology 0 H0O) (from left to right).
An exact proof term for the current goal is real_0.
An exact proof term for the current goal is (UnionI S 0 (space_family_set Xi 0) H0inSF0 HS0).
We prove the intermediate claim Hsub: f0 ⊆ setprod ω (space_family_union ω Xi).
Let p be given.
Assume Hp: p ∈ f0.
We will prove p ∈ setprod ω (space_family_union ω Xi).
Apply (ReplE_impred ω (λi0 : set ⇒ (i0,0)) p Hp (p ∈ setprod ω (space_family_union ω Xi))) to the current goal.
Let i be given.
Assume HiO: i ∈ ω.
Assume HpEq: p = (i,0).
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 ω (space_family_union ω Xi) i 0 HiO H0inUnion).
We prove the intermediate claim Hpow: f0 ∈ 𝒫 (setprod ω (space_family_union ω Xi)).
An exact proof term for the current goal is (PowerI (setprod ω (space_family_union ω Xi)) f0 Hsub).
We prove the intermediate claim Htot: total_function_on f0 ω (space_family_union ω Xi).
rewrite the current goal using Hf0Eq (from left to right).
An exact proof term for the current goal is (const_fun_total_function_on ω (space_family_union ω Xi) 0 H0inUnion).
We prove the intermediate claim Hfun: functional_graph f0.
An exact proof term for the current goal is (functional_graph_const_fun ω 0).
We prove the intermediate claim Hcoord: ∀i : set, i ∈ ω → apply_fun f0 i ∈ space_family_set Xi i.
Let i be given.
Assume HiO: i ∈ ω.
rewrite the current goal using Hf0Eq (from left to right).
rewrite the current goal using (const_fun_apply ω 0 i HiO) (from left to right).
rewrite the current goal using (space_family_set_const_space_family ω R R_standard_topology i HiO) (from left to right).
An exact proof term for the current goal is real_0.
We prove the intermediate claim Hpair: total_function_on f0 ω (space_family_union ω Xi) ∧ functional_graph f0.
An exact proof term for the current goal is (andI (total_function_on f0 ω (space_family_union ω Xi)) (functional_graph f0) Htot Hfun).
We prove the intermediate claim Hprop: total_function_on f0 ω (space_family_union ω Xi) ∧ functional_graph f0 ∧ ∀i : set, i ∈ ω → apply_fun f0 i ∈ space_family_set Xi i.
An exact proof term for the current goal is (andI (total_function_on f0 ω (space_family_union ω Xi) ∧ functional_graph f0) (∀i : set, i ∈ ω → apply_fun f0 i ∈ space_family_set Xi i) Hpair Hcoord).
An exact proof term for the current goal is (SepI (𝒫 (setprod ω (space_family_union ω Xi))) (λf : set ⇒ total_function_on f ω (space_family_union ω Xi) ∧ functional_graph f ∧ ∀i : set, i ∈ ω → apply_fun f i ∈ space_family_set Xi i) f0 Hpow Hprop).
An exact proof term for the current goal is (component_of_whole X Tx f0 R_omega_product_connected Hf0X).
Set Xi to be the term const_space_family ω R R_standard_topology.
Set X to be the term product_space ω Xi.
Set Tx to be the term box_topology ω Xi.
Set f0 to be the term const_family ω 0.
Set Afs to be the term {f ∈ X|∃F : set, finite F ∧ ∀i : set, i ∈ ω ∖ F → apply_fun f i = 0}.
We prove the intermediate claim HAeq: Romega_infty = Afs.
An exact proof term for the current goal is Romega_infty_eq_finite_support.
rewrite the current goal using HAeq (from right to left).
We will prove component_of X Tx f0 = Romega_infty.
Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ component_of X Tx f0.
We will prove f ∈ Romega_infty.
An exact proof term for the current goal is (component_of_Romega_box_zero_subset_Romega_infty f Hf).
Let f be given.
Assume Hf: f ∈ Romega_infty.
We will prove f ∈ component_of X Tx f0.
We prove the intermediate claim HdefC: component_of X Tx f0 = {y ∈ X|∃C : set, connected_space C (subspace_topology X Tx C) ∧ f0 ∈ C ∧ y ∈ C}.
Use reflexivity.
rewrite the current goal using HdefC (from left to right).
Apply SepI to the current goal.
We prove the intermediate claim HXeq: X = R_omega_space.
Use reflexivity.
rewrite the current goal using HXeq (from left to right).
An exact proof term for the current goal is (Romega_infty_sub_Romega f Hf).
We will prove ∃C : set, connected_space C (subspace_topology X Tx C) ∧ f0 ∈ C ∧ f ∈ C.
We use Romega_infty to witness the existential quantifier.
We will prove connected_space Romega_infty (subspace_topology X Tx Romega_infty) ∧ f0 ∈ Romega_infty ∧ f ∈ Romega_infty.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HXeq: X = R_omega_space.
Use reflexivity.
We prove the intermediate claim HTxeq: Tx = R_omega_box_topology.
Use reflexivity.
rewrite the current goal using HXeq (from left to right).
rewrite the current goal using HTxeq (from left to right).
An exact proof term for the current goal is Romega_infty_connected_box.
We prove the intermediate claim Hf0Eq: f0 = Romega_zero.
Use reflexivity.
rewrite the current goal using Hf0Eq (from left to right).
Set Fam to be the term {Romega_tilde n|n ∈ ω}.
We prove the intermediate claim Hdef: Romega_infty = ⋃ Fam.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
We prove the intermediate claim H0O: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim HZin: Romega_zero ∈ Romega_tilde 0.
An exact proof term for the current goal is (Romega_zero_in_Romega_tilde 0 H0O).
We prove the intermediate claim HFam0: Romega_tilde 0 ∈ Fam.
An exact proof term for the current goal is (ReplI ω (λn0 : set ⇒ Romega_tilde n0) 0 H0O).
An exact proof term for the current goal is (UnionI Fam Romega_zero (Romega_tilde 0) HZin HFam0).
An exact proof term for the current goal is Hf.
∎