We will prove closed_in R_omega_space R_omega_box_topology Romega_infty.
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 B to be the term box_basis ω Xi.
Set TU to be the term topology_family_union ω Xi.
We prove the intermediate claim HXeq: X = R_omega_space.
Use reflexivity.
rewrite the current goal using HXeq (from right to left).
We prove the intermediate claim HTx: topology_on X Tx.
Apply (box_topology_is_topology_on ω Xi) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
We will prove topology_on (space_family_set Xi i) (space_family_topology Xi i).
rewrite the current goal using (space_family_set_const_space_family ω R R_standard_topology i Hi) (from left to right).
rewrite the current goal using (space_family_topology_const_space_family ω R R_standard_topology i Hi) (from left to right).
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim HAsub: Romega_infty ⊆ X.
rewrite the current goal using HXeq (from left to right).
An exact proof term for the current goal is Romega_infty_sub_Romega.
Set Uc to be the term X ∖ Romega_infty.
We prove the intermediate claim HUcPow: Uc ∈ 𝒫 X.
Apply PowerI to the current goal.
Let f be given.
Assume Hf: f ∈ Uc.
An exact proof term for the current goal is (setminusE1 X Romega_infty f Hf).
We prove the intermediate claim HUcOpen: Uc ∈ Tx.
We will prove Uc ∈ generated_topology X B.
We prove the intermediate claim Hgtdef: generated_topology X B = {U ∈ 𝒫 X|∀x ∈ U, ∃b ∈ B, x ∈ b ∧ b ⊆ U}.
Use reflexivity.
rewrite the current goal using Hgtdef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HUcPow.
Let f be given.
Assume Hf: f ∈ Uc.
We will prove ∃b ∈ B, f ∈ b ∧ b ⊆ Uc.
We prove the intermediate claim HfX: f ∈ X.
An exact proof term for the current goal is (setminusE1 X Romega_infty f Hf).
We prove the intermediate claim HfNotA: f ∉ Romega_infty.
An exact proof term for the current goal is (setminusE2 X Romega_infty f Hf).
Set Rnz to be the term R ∖ {0}.
We prove the intermediate claim HRnz: Rnz ∈ R_standard_topology.
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim Hcl0: closed_in R R_standard_topology {0}.
An exact proof term for the current goal is (Hausdorff_singletons_closed R R_standard_topology 0 R_standard_topology_Hausdorff H0R).
We prove the intermediate claim Hop: open_in R R_standard_topology (R ∖ {0}).
An exact proof term for the current goal is (open_of_closed_complement R R_standard_topology {0} Hcl0).
An exact proof term for the current goal is (open_in_elem R R_standard_topology (R ∖ {0}) Hop).
Set Uf to be the term graph ω (λi : set ⇒ if apply_fun f i = 0 then R else Rnz).
Set b to be the term {g ∈ X|∀i : set, i ∈ ω → apply_fun g i ∈ apply_fun Uf i}.
We use b to witness the existential quantifier.
Apply andI to the current goal.
We will prove b ∈ B.
We prove the intermediate claim HBdef: B = {B0 ∈ 𝒫 X|∃U : set, total_function_on U ω TU ∧ functional_graph U ∧ (∀i : set, i ∈ ω → apply_fun U i ∈ space_family_topology Xi i) ∧ B0 = {g ∈ X|∀i : set, i ∈ ω → apply_fun g i ∈ apply_fun U i}}.
Use reflexivity.
rewrite the current goal using HBdef (from left to right).
Apply SepI to the current goal.
We prove the intermediate claim Hbsub: b ⊆ X.
Let g be given.
Assume Hg: g ∈ b.
An exact proof term for the current goal is (SepE1 X (λg0 : set ⇒ ∀i : set, i ∈ ω → apply_fun g0 i ∈ apply_fun Uf i) g Hg).
An exact proof term for the current goal is (PowerI X b Hbsub).
We will prove ∃U : set, total_function_on U ω TU ∧ functional_graph U ∧ (∀i : set, i ∈ ω → apply_fun U i ∈ space_family_topology Xi i) ∧ b = {g ∈ X|∀i : set, i ∈ ω → apply_fun g i ∈ apply_fun U i}.
We use Uf to witness the existential quantifier.
We will prove total_function_on Uf ω TU ∧ functional_graph Uf ∧ (∀i : set, i ∈ ω → apply_fun Uf i ∈ space_family_topology Xi i) ∧ b = {g ∈ X|∀i : set, i ∈ ω → apply_fun g i ∈ apply_fun Uf i}.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply (total_function_on_graph ω TU (λi : set ⇒ if apply_fun f i = 0 then R else Rnz)) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
We will prove (if apply_fun f i = 0 then R else Rnz) ∈ TU.
Set S to be the term {space_family_topology Xi j|j ∈ ω}.
We prove the intermediate claim HdefTU: TU = ⋃ S.
Use reflexivity.
rewrite the current goal using HdefTU (from left to right).
We prove the intermediate claim HiS: space_family_topology Xi i ∈ S.
An exact proof term for the current goal is (ReplI ω (λj : set ⇒ space_family_topology Xi j) i Hi).
We prove the intermediate claim HTi: space_family_topology Xi i = R_standard_topology.
An exact proof term for the current goal is (space_family_topology_const_space_family ω R R_standard_topology i Hi).
Apply (xm (apply_fun f i = 0)) to the current goal.
Assume Hfi0: apply_fun f i = 0.
We prove the intermediate claim Hif: (if apply_fun f i = 0 then R else Rnz) = R.
An exact proof term for the current goal is (If_i_1 (apply_fun f i = 0) R Rnz Hfi0).
rewrite the current goal using Hif (from left to right).
We prove the intermediate claim HRin: R ∈ space_family_topology Xi i.
rewrite the current goal using HTi (from left to right).
An exact proof term for the current goal is (topology_has_X R R_standard_topology R_standard_topology_is_topology_local).
An exact proof term for the current goal is (UnionI S R (space_family_topology Xi i) HRin HiS).
Assume Hfin0: apply_fun f i ≠ 0.
We prove the intermediate claim Hif: (if apply_fun f i = 0 then R else Rnz) = Rnz.
An exact proof term for the current goal is (If_i_0 (apply_fun f i = 0) R Rnz Hfin0).
rewrite the current goal using Hif (from left to right).
We prove the intermediate claim HRnzin: Rnz ∈ space_family_topology Xi i.
rewrite the current goal using HTi (from left to right).
An exact proof term for the current goal is HRnz.
An exact proof term for the current goal is (UnionI S Rnz (space_family_topology Xi i) HRnzin HiS).
An exact proof term for the current goal is (functional_graph_graph ω (λi : set ⇒ if apply_fun f i = 0 then R else Rnz)).
Let i be given.
Assume Hi: i ∈ ω.
We will prove apply_fun Uf i ∈ space_family_topology Xi i.
We prove the intermediate claim HTi: space_family_topology Xi i = R_standard_topology.
An exact proof term for the current goal is (space_family_topology_const_space_family ω R R_standard_topology i Hi).
rewrite the current goal using HTi (from left to right).
We prove the intermediate claim HUfi: apply_fun Uf i = (if apply_fun f i = 0 then R else Rnz).
An exact proof term for the current goal is (apply_fun_graph ω (λj : set ⇒ if apply_fun f j = 0 then R else Rnz) i Hi).
rewrite the current goal using HUfi (from left to right).
Apply (xm (apply_fun f i = 0)) to the current goal.
Assume Hfi0: apply_fun f i = 0.
We prove the intermediate claim Hif: (if apply_fun f i = 0 then R else Rnz) = R.
An exact proof term for the current goal is (If_i_1 (apply_fun f i = 0) R Rnz Hfi0).
rewrite the current goal using Hif (from left to right).
An exact proof term for the current goal is (topology_has_X R R_standard_topology R_standard_topology_is_topology_local).
Assume Hfin0: apply_fun f i ≠ 0.
We prove the intermediate claim Hif: (if apply_fun f i = 0 then R else Rnz) = Rnz.
An exact proof term for the current goal is (If_i_0 (apply_fun f i = 0) R Rnz Hfin0).
rewrite the current goal using Hif (from left to right).
An exact proof term for the current goal is HRnz.
Use reflexivity.
Apply andI to the current goal.
Apply SepI to the current goal.
An exact proof term for the current goal is HfX.
Let i be given.
Assume Hi: i ∈ ω.
We will prove apply_fun f i ∈ apply_fun Uf i.
We prove the intermediate claim HUfi: apply_fun Uf i = (if apply_fun f i = 0 then R else Rnz).
An exact proof term for the current goal is (apply_fun_graph ω (λj : set ⇒ if apply_fun f j = 0 then R else Rnz) i Hi).
rewrite the current goal using HUfi (from left to right).
Apply (xm (apply_fun f i = 0)) to the current goal.
Assume Hfi0: apply_fun f i = 0.
We prove the intermediate claim Hif: (if apply_fun f i = 0 then R else Rnz) = R.
An exact proof term for the current goal is (If_i_1 (apply_fun f i = 0) R Rnz Hfi0).
rewrite the current goal using Hif (from left to right).
An exact proof term for the current goal is (Romega_coord_in_R f i HfX Hi).
Assume Hfin0: apply_fun f i ≠ 0.
We prove the intermediate claim Hif: (if apply_fun f i = 0 then R else Rnz) = Rnz.
An exact proof term for the current goal is (If_i_0 (apply_fun f i = 0) R Rnz Hfin0).
rewrite the current goal using Hif (from left to right).
We prove the intermediate claim HfiR: apply_fun f i ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R f i HfX Hi).
We will prove apply_fun f i ∈ R ∖ {0}.
Apply setminusI to the current goal.
An exact proof term for the current goal is HfiR.
Assume Hfi0: apply_fun f i ∈ {0}.
We prove the intermediate claim HfiEq: apply_fun f i = 0.
An exact proof term for the current goal is (SingE 0 (apply_fun f i) Hfi0).
An exact proof term for the current goal is (Hfin0 HfiEq).
Let g be given.
Assume Hg: g ∈ b.
We will prove g ∈ Uc.
We prove the intermediate claim HgX: g ∈ X.
An exact proof term for the current goal is (SepE1 X (λg0 : set ⇒ ∀i : set, i ∈ ω → apply_fun g0 i ∈ apply_fun Uf i) g Hg).
Apply setminusI to the current goal.
An exact proof term for the current goal is HgX.
Assume HgA: g ∈ Romega_infty.
We prove the intermediate claim HAfs: ∀h : set, h ∈ Romega_infty → ∃F : set, finite F ∧ ∀i : set, i ∈ ω ∖ F → apply_fun h i = 0.
Let h be given.
Assume HhA: h ∈ Romega_infty.
We prove the intermediate claim HhAfs: h ∈ {h0 ∈ R_omega_space|∃F : set, finite F ∧ ∀i : set, i ∈ ω ∖ F → apply_fun h0 i = 0}.
rewrite the current goal using Romega_infty_eq_finite_support (from right to left).
An exact proof term for the current goal is HhA.
An exact proof term for the current goal is (SepE2 R_omega_space (λh0 : set ⇒ ∃F : set, finite F ∧ ∀i : set, i ∈ ω ∖ F → apply_fun h0 i = 0) h HhAfs).
We prove the intermediate claim HnoF: ∀F : set, finite F → ∃i : set, i ∈ ω ∖ F ∧ apply_fun f i ≠ 0.
Let F be given.
Assume HFfin: finite F.
Apply (xm (∃i : set, i ∈ ω ∖ F ∧ apply_fun f i ≠ 0)) to the current goal.
Assume Hex: ∃i : set, i ∈ ω ∖ F ∧ apply_fun f i ≠ 0.
An exact proof term for the current goal is Hex.
Assume Hnot: ¬ (∃i : set, i ∈ ω ∖ F ∧ apply_fun f i ≠ 0).
We will prove False.
We prove the intermediate claim HfRomega: f ∈ R_omega_space.
rewrite the current goal using HXeq (from right to left).
An exact proof term for the current goal is HfX.
We prove the intermediate claim Hsupp: ∀i : set, i ∈ ω ∖ F → apply_fun f i = 0.
Let i be given.
Assume Hi: i ∈ ω ∖ F.
Apply (xm (apply_fun f i = 0)) to the current goal.
Assume H0: apply_fun f i = 0.
An exact proof term for the current goal is H0.
Assume Hne0: apply_fun f i ≠ 0.
Apply FalseE to the current goal.
Apply Hnot to the current goal.
We use i to witness the existential quantifier.
An exact proof term for the current goal is (andI (i ∈ ω ∖ F) (apply_fun f i ≠ 0) Hi Hne0).
We prove the intermediate claim HfAfs: f ∈ {h0 ∈ R_omega_space|∃F0 : set, finite F0 ∧ ∀i : set, i ∈ ω ∖ F0 → apply_fun h0 i = 0}.
Apply SepI to the current goal.
An exact proof term for the current goal is HfRomega.
We will prove ∃F0 : set, finite F0 ∧ ∀i : set, i ∈ ω ∖ F0 → apply_fun f i = 0.
We use F to witness the existential quantifier.
We will prove finite F ∧ ∀i : set, i ∈ ω ∖ F → apply_fun f i = 0.
An exact proof term for the current goal is (andI (finite F) (∀i : set, i ∈ ω ∖ F → apply_fun f i = 0) HFfin Hsupp).
We prove the intermediate claim HfA: f ∈ Romega_infty.
rewrite the current goal using Romega_infty_eq_finite_support (from left to right).
An exact proof term for the current goal is HfAfs.
An exact proof term for the current goal is (HfNotA HfA).
We prove the intermediate claim HexF: ∃F : set, finite F ∧ ∀i : set, i ∈ ω ∖ F → apply_fun g i = 0.
An exact proof term for the current goal is (HAfs g HgA).
Apply HexF to the current goal.
Let F be given.
Assume HFconj.
We prove the intermediate claim HFfin: finite F.
An exact proof term for the current goal is (andEL (finite F) (∀i : set, i ∈ ω ∖ F → apply_fun g i = 0) HFconj).
We prove the intermediate claim Hg0out: ∀i : set, i ∈ ω ∖ F → apply_fun g i = 0.
An exact proof term for the current goal is (andER (finite F) (∀i : set, i ∈ ω ∖ F → apply_fun g i = 0) HFconj).
We prove the intermediate claim Hexi: ∃i : set, i ∈ ω ∖ F ∧ apply_fun f i ≠ 0.
An exact proof term for the current goal is (HnoF F HFfin).
Apply Hexi to the current goal.
Let i be given.
Assume HiConj.
We prove the intermediate claim HiOF: i ∈ ω ∖ F.
An exact proof term for the current goal is (andEL (i ∈ ω ∖ F) (apply_fun f i ≠ 0) HiConj).
We prove the intermediate claim Hfin0: apply_fun f i ≠ 0.
An exact proof term for the current goal is (andER (i ∈ ω ∖ F) (apply_fun f i ≠ 0) HiConj).
We prove the intermediate claim Hig0: apply_fun g i = 0.
An exact proof term for the current goal is (Hg0out i HiOF).
We prove the intermediate claim Hgb: ∀j : set, j ∈ ω → apply_fun g j ∈ apply_fun Uf j.
An exact proof term for the current goal is (SepE2 X (λg0 : set ⇒ ∀j : set, j ∈ ω → apply_fun g0 j ∈ apply_fun Uf j) g Hg).
We prove the intermediate claim HiO: i ∈ ω.
An exact proof term for the current goal is (setminusE1 ω F i HiOF).
We prove the intermediate claim HgUi: apply_fun g i ∈ apply_fun Uf i.
An exact proof term for the current goal is (Hgb i HiO).
We prove the intermediate claim HUfi: apply_fun Uf i = (if apply_fun f i = 0 then R else Rnz).
An exact proof term for the current goal is (apply_fun_graph ω (λj : set ⇒ if apply_fun f j = 0 then R else Rnz) i HiO).
We prove the intermediate claim HgUiIf: apply_fun g i ∈ (if apply_fun f i = 0 then R else Rnz).
rewrite the current goal using HUfi (from right to left).
An exact proof term for the current goal is HgUi.
We prove the intermediate claim Hif: (if apply_fun f i = 0 then R else Rnz) = Rnz.
An exact proof term for the current goal is (If_i_0 (apply_fun f i = 0) R Rnz Hfin0).
We prove the intermediate claim HgUiRnz: apply_fun g i ∈ Rnz.
rewrite the current goal using Hif (from right to left).
An exact proof term for the current goal is HgUiIf.
We prove the intermediate claim HRnzDef: Rnz = R ∖ {0}.
Use reflexivity.
We prove the intermediate claim HgUiRnz2: apply_fun g i ∈ R ∖ {0}.
rewrite the current goal using HRnzDef (from right to left).
An exact proof term for the current goal is HgUiRnz.
We prove the intermediate claim Hg0ne: apply_fun g i ≠ 0.
Assume Hg0: apply_fun g i = 0.
We prove the intermediate claim Hg0in: apply_fun g i ∈ {0}.
rewrite the current goal using Hg0 (from left to right).
An exact proof term for the current goal is (SingI 0).
We prove the intermediate claim Hg0not: apply_fun g i ∉ {0}.
An exact proof term for the current goal is (setminusE2 R {0} (apply_fun g i) HgUiRnz2).
An exact proof term for the current goal is (Hg0not Hg0in).
An exact proof term for the current goal is (Hg0ne Hig0).
Apply (closed_inI X Tx Romega_infty HTx HAsub) to the current goal.
We will prove ∃U ∈ Tx, Romega_infty = X ∖ U.
We use (X ∖ Romega_infty) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HUcOpen.
We will prove Romega_infty = X ∖ (X ∖ Romega_infty).
rewrite the current goal using (setminus_setminus_eq X Romega_infty HAsub) (from left to right).
Use reflexivity.
∎