We will prove R_omega_product_topology ⊆ R_omega_box_topology.
Set Xi to be the term const_space_family ω R R_standard_topology.
Set X to be the term product_space ω Xi.
Set S to be the term product_subbasis_full ω Xi.
Set Tprod to be the term generated_topology_from_subbasis X S.
Set B to be the term box_basis ω Xi.
Set Tbox to be the term generated_topology X B.
We prove the intermediate claim HTprodEq: Tprod = R_omega_product_topology.
Use reflexivity.
We prove the intermediate claim HTboxEq: Tbox = R_omega_box_topology.
Use reflexivity.
rewrite the current goal using HTprodEq (from right to left).
rewrite the current goal using HTboxEq (from right to left).
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 HcompTop: ∀i : set, i ∈ ω → topology_on (space_family_set Xi i) (space_family_topology Xi i).
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 HSsub: S ⊆ 𝒫 X.
Let s be given.
Assume Hs: s ∈ S.
We will prove s ∈ 𝒫 X.
Apply PowerI to the current goal.
Let f be given.
Assume Hf: f ∈ s.
We will prove f ∈ X.
Set F to be the term (λi : set ⇒ {product_cylinder ω Xi i U|U ∈ space_family_topology Xi i}).
We prove the intermediate claim HsF: s ∈ (⋃i ∈ ωF i).
An exact proof term for the current goal is Hs.
Apply (famunionE_impred ω F s HsF (f ∈ X)) to the current goal.
Let i be given.
Assume HiO: i ∈ ω.
Assume HsFi: s ∈ F i.
Apply (ReplE_impred (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder ω Xi i U0) s HsFi (f ∈ X)) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ space_family_topology Xi i.
Assume Hseq: s = product_cylinder ω Xi i U0.
We prove the intermediate claim HfCyl: f ∈ product_cylinder ω Xi i U0.
rewrite the current goal using Hseq (from right to left).
An exact proof term for the current goal is Hf.
An exact proof term for the current goal is (SepE1 X (λg0 : set ⇒ i ∈ ω ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun g0 i ∈ U0) f HfCyl).
We prove the intermediate claim HUnionS: ⋃ S = X.
Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ ⋃ S.
We will prove f ∈ X.
Apply UnionE_impred S f Hf to the current goal.
Let s be given.
Assume Hfs: f ∈ s.
Assume HsS: s ∈ S.
We prove the intermediate claim HsPow: s ∈ 𝒫 X.
An exact proof term for the current goal is (HSsub s HsS).
An exact proof term for the current goal is (PowerE X s HsPow f Hfs).
Let f be given.
Assume Hf: f ∈ X.
We will prove f ∈ ⋃ S.
Set i0 to be the term 0.
Set U0 to be the term space_family_set Xi i0.
Set s0 to be the term product_cylinder ω Xi i0 U0.
We prove the intermediate claim Hi0: i0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim HTi0: topology_on (space_family_set Xi i0) (space_family_topology Xi i0).
An exact proof term for the current goal is (HcompTop i0 Hi0).
We prove the intermediate claim HU0top: U0 ∈ space_family_topology Xi i0.
An exact proof term for the current goal is (topology_has_X (space_family_set Xi i0) (space_family_topology Xi i0) HTi0).
We prove the intermediate claim Hs0S: s0 ∈ S.
Set F to be the term (λi : set ⇒ {product_cylinder ω Xi i U|U ∈ space_family_topology Xi i}).
We prove the intermediate claim Hs0Fi0: s0 ∈ F i0.
An exact proof term for the current goal is (ReplI (space_family_topology Xi i0) (λU : set ⇒ product_cylinder ω Xi i0 U) U0 HU0top).
An exact proof term for the current goal is (famunionI ω F i0 s0 Hi0 Hs0Fi0).
We will prove f ∈ ⋃ S.
Apply (UnionI S f s0) to the current goal.
We will prove f ∈ s0.
We will prove f ∈ {g ∈ X|i0 ∈ ω ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun g i0 ∈ U0}.
Apply (SepI X (λg0 : set ⇒ i0 ∈ ω ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun g0 i0 ∈ U0) f Hf) to the current goal.
We will prove i0 ∈ ω ∧ U0 ∈ space_family_topology Xi i0 ∧ apply_fun f i0 ∈ U0.
Apply andI to the current goal.
We will prove i0 ∈ ω ∧ U0 ∈ space_family_topology Xi i0.
Apply andI to the current goal.
An exact proof term for the current goal is Hi0.
An exact proof term for the current goal is HU0top.
We prove the intermediate claim Hfprop: total_function_on f ω (space_family_union ω Xi) ∧ functional_graph f ∧ ∀i : set, i ∈ ω → apply_fun f i ∈ space_family_set Xi i.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod ω (space_family_union ω Xi))) (λf0 : set ⇒ total_function_on f0 ω (space_family_union ω Xi) ∧ functional_graph f0 ∧ ∀i : set, i ∈ ω → apply_fun f0 i ∈ space_family_set Xi i) f Hf).
We prove the intermediate claim Hcoords: ∀i : set, i ∈ ω → apply_fun f i ∈ space_family_set Xi i.
An exact proof term for the current goal is (andER (total_function_on f ω (space_family_union ω Xi) ∧ functional_graph f) (∀i : set, i ∈ ω → apply_fun f i ∈ space_family_set Xi i) Hfprop).
An exact proof term for the current goal is (Hcoords i0 Hi0).
An exact proof term for the current goal is Hs0S.
We prove the intermediate claim HSsubbasis: subbasis_on X S.
We will prove S ⊆ 𝒫 X ∧ ⋃ S = X.
Apply andI to the current goal.
An exact proof term for the current goal is HSsub.
An exact proof term for the current goal is HUnionS.
We prove the intermediate claim HTboxTop: topology_on X Tbox.
An exact proof term for the current goal is (box_topology_is_topology_on ω Xi HcompTop).
We prove the intermediate claim HBasis: basis_on X B.
An exact proof term for the current goal is (box_basis_is_basis_on ω Xi HcompTop).
We prove the intermediate claim HSsubTbox: S ⊆ Tbox.
Let s be given.
Assume HsS: s ∈ S.
We will prove s ∈ Tbox.
Set F to be the term (λi : set ⇒ {product_cylinder ω Xi i U|U ∈ space_family_topology Xi i}).
We prove the intermediate claim HsF: s ∈ (⋃i ∈ ωF i).
An exact proof term for the current goal is HsS.
Apply (famunionE_impred ω F s HsF (s ∈ Tbox)) to the current goal.
Let i be given.
Assume HiO: i ∈ ω.
Assume HsFi: s ∈ F i.
Apply (ReplE_impred (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder ω Xi i U0) s HsFi (s ∈ Tbox)) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ space_family_topology Xi i.
Assume Hseq: s = product_cylinder ω Xi i U0.
rewrite the current goal using Hseq (from left to right).
Set Ufun to be the term graph ω (λj : set ⇒ if j = i then U0 else space_family_set Xi j).
Set b0 to be the term {f ∈ X|∀j : set, j ∈ ω → apply_fun f j ∈ apply_fun Ufun j}.
We prove the intermediate claim Hb0box: b0 ∈ B.
We will prove b0 ∈ box_basis ω Xi.
We prove the intermediate claim HBdef: box_basis ω Xi = {B0 ∈ 𝒫 X|∃U : set, total_function_on U ω (topology_family_union ω Xi) ∧ functional_graph U ∧ (∀j : set, j ∈ ω → apply_fun U j ∈ space_family_topology Xi j) ∧ B0 = {f ∈ X|∀j : set, j ∈ ω → apply_fun f j ∈ apply_fun U j}}.
Use reflexivity.
rewrite the current goal using HBdef (from left to right).
Apply SepI to the current goal.
We will prove b0 ∈ 𝒫 X.
Apply PowerI to the current goal.
Let f be given.
Assume Hf: f ∈ b0.
We will prove f ∈ X.
An exact proof term for the current goal is (SepE1 X (λf0 : set ⇒ ∀j : set, j ∈ ω → apply_fun f0 j ∈ apply_fun Ufun j) f Hf).
We will prove ∃U : set, total_function_on U ω (topology_family_union ω Xi) ∧ functional_graph U ∧ (∀j : set, j ∈ ω → apply_fun U j ∈ space_family_topology Xi j) ∧ b0 = {f ∈ X|∀j : set, j ∈ ω → apply_fun f j ∈ apply_fun U j}.
We use Ufun to witness the existential quantifier.
We will prove total_function_on Ufun ω (topology_family_union ω Xi) ∧ functional_graph Ufun ∧ (∀j : set, j ∈ ω → apply_fun Ufun j ∈ space_family_topology Xi j) ∧ b0 = {f ∈ X|∀j : set, j ∈ ω → apply_fun f j ∈ apply_fun Ufun j}.
Apply andI to the current goal.
We will prove (total_function_on Ufun ω (topology_family_union ω Xi) ∧ functional_graph Ufun) ∧ (∀j : set, j ∈ ω → apply_fun Ufun j ∈ space_family_topology Xi j).
Apply andI to the current goal.
We will prove total_function_on Ufun ω (topology_family_union ω Xi) ∧ functional_graph Ufun.
Apply andI to the current goal.
Apply (total_function_on_graph ω (topology_family_union ω Xi) (λj : set ⇒ if j = i then U0 else space_family_set Xi j)) to the current goal.
Let j be given.
Assume HjO: j ∈ ω.
We will prove (if j = i then U0 else space_family_set Xi j) ∈ topology_family_union ω Xi.
Apply (xm (j = i)) to the current goal.
Assume Hji: j = i.
rewrite the current goal using (If_i_1 (j = i) U0 (space_family_set Xi j) Hji) (from left to right).
Set Fam to be the term {space_family_topology Xi k|k ∈ ω}.
We prove the intermediate claim HFam: space_family_topology Xi i ∈ Fam.
An exact proof term for the current goal is (ReplI ω (λk : set ⇒ space_family_topology Xi k) i HiO).
We prove the intermediate claim HU0Fam: U0 ∈ space_family_topology Xi i.
An exact proof term for the current goal is HU0.
We prove the intermediate claim HTUdef: topology_family_union ω Xi = ⋃ Fam.
Use reflexivity.
rewrite the current goal using HTUdef (from left to right).
An exact proof term for the current goal is (UnionI Fam U0 (space_family_topology Xi i) HU0Fam HFam).
Assume Hjne: j ≠ i.
rewrite the current goal using (If_i_0 (j = i) U0 (space_family_set Xi j) Hjne) (from left to right).
We prove the intermediate claim HTj: topology_on (space_family_set Xi j) (space_family_topology Xi j).
An exact proof term for the current goal is (HcompTop j HjO).
We prove the intermediate claim Hjopen: space_family_set Xi j ∈ space_family_topology Xi j.
An exact proof term for the current goal is (topology_has_X (space_family_set Xi j) (space_family_topology Xi j) HTj).
Set Fam to be the term {space_family_topology Xi k|k ∈ ω}.
We prove the intermediate claim HFam: space_family_topology Xi j ∈ Fam.
An exact proof term for the current goal is (ReplI ω (λk : set ⇒ space_family_topology Xi k) j HjO).
We prove the intermediate claim HTUdef: topology_family_union ω Xi = ⋃ Fam.
Use reflexivity.
rewrite the current goal using HTUdef (from left to right).
An exact proof term for the current goal is (UnionI Fam (space_family_set Xi j) (space_family_topology Xi j) Hjopen HFam).
An exact proof term for the current goal is (functional_graph_graph ω (λj : set ⇒ if j = i then U0 else space_family_set Xi j)).
Let j be given.
Assume HjO: j ∈ ω.
We will prove apply_fun Ufun j ∈ space_family_topology Xi j.
Apply (xm (j = i)) to the current goal.
Assume Hji: j = i.
rewrite the current goal using (apply_fun_graph ω (λk : set ⇒ if k = i then U0 else space_family_set Xi k) j HjO) (from left to right).
rewrite the current goal using (If_i_1 (j = i) U0 (space_family_set Xi j) Hji) (from left to right).
rewrite the current goal using Hji (from left to right).
An exact proof term for the current goal is HU0.
Assume Hjne: j ≠ i.
rewrite the current goal using (apply_fun_graph ω (λk : set ⇒ if k = i then U0 else space_family_set Xi k) j HjO) (from left to right).
rewrite the current goal using (If_i_0 (j = i) U0 (space_family_set Xi j) Hjne) (from left to right).
We prove the intermediate claim HTj: topology_on (space_family_set Xi j) (space_family_topology Xi j).
An exact proof term for the current goal is (HcompTop j HjO).
An exact proof term for the current goal is (topology_has_X (space_family_set Xi j) (space_family_topology Xi j) HTj).
Use reflexivity.
We prove the intermediate claim Hb0open: b0 ∈ Tbox.
An exact proof term for the current goal is (generated_topology_contains_basis X B HBasis b0 Hb0box).
We prove the intermediate claim HcylEq: product_cylinder ω Xi i U0 = b0.
Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ product_cylinder ω Xi i U0.
We will prove f ∈ b0.
We prove the intermediate claim HfX: f ∈ X.
An exact proof term for the current goal is (SepE1 X (λg0 : set ⇒ i ∈ ω ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun g0 i ∈ U0) f Hf).
We prove the intermediate claim Hcond: i ∈ ω ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun f i ∈ U0.
An exact proof term for the current goal is (SepE2 X (λg0 : set ⇒ i ∈ ω ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun g0 i ∈ U0) f Hf).
We prove the intermediate claim HfiU0: apply_fun f i ∈ U0.
An exact proof term for the current goal is (andER (i ∈ ω ∧ U0 ∈ space_family_topology Xi i) (apply_fun f i ∈ U0) Hcond).
Apply SepI to the current goal.
An exact proof term for the current goal is HfX.
Let j be given.
Assume HjO: j ∈ ω.
We will prove apply_fun f j ∈ apply_fun Ufun j.
Apply (xm (j = i)) to the current goal.
Assume Hji: j = i.
rewrite the current goal using Hji (from left to right).
rewrite the current goal using (apply_fun_graph ω (λk : set ⇒ if k = i then U0 else space_family_set Xi k) i HiO) (from left to right).
We prove the intermediate claim Hii: i = i.
Use reflexivity.
rewrite the current goal using (If_i_1 (i = i) U0 (space_family_set Xi i) Hii) (from left to right).
An exact proof term for the current goal is HfiU0.
Assume Hjne: j ≠ i.
rewrite the current goal using (apply_fun_graph ω (λk : set ⇒ if k = i then U0 else space_family_set Xi k) j HjO) (from left to right).
rewrite the current goal using (If_i_0 (j = i) U0 (space_family_set Xi j) Hjne) (from left to right).
We prove the intermediate claim Hfprop: total_function_on f ω (space_family_union ω Xi) ∧ functional_graph f ∧ ∀k : set, k ∈ ω → apply_fun f k ∈ space_family_set Xi k.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod ω (space_family_union ω Xi))) (λf0 : set ⇒ total_function_on f0 ω (space_family_union ω Xi) ∧ functional_graph f0 ∧ ∀k : set, k ∈ ω → apply_fun f0 k ∈ space_family_set Xi k) f HfX).
We prove the intermediate claim Hcoords: ∀k : set, k ∈ ω → apply_fun f k ∈ space_family_set Xi k.
An exact proof term for the current goal is (andER (total_function_on f ω (space_family_union ω Xi) ∧ functional_graph f) (∀k : set, k ∈ ω → apply_fun f k ∈ space_family_set Xi k) Hfprop).
An exact proof term for the current goal is (Hcoords j HjO).
Let f be given.
Assume Hf: f ∈ b0.
We will prove f ∈ product_cylinder ω Xi i U0.
We prove the intermediate claim HfX: f ∈ X.
An exact proof term for the current goal is (SepE1 X (λf0 : set ⇒ ∀j : set, j ∈ ω → apply_fun f0 j ∈ apply_fun Ufun j) f Hf).
We prove the intermediate claim Hall: ∀j : set, j ∈ ω → apply_fun f j ∈ apply_fun Ufun j.
An exact proof term for the current goal is (SepE2 X (λf0 : set ⇒ ∀j : set, j ∈ ω → apply_fun f0 j ∈ apply_fun Ufun j) f Hf).
We prove the intermediate claim HCylDef: product_cylinder ω Xi i U0 = {f0 ∈ X|i ∈ ω ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U0}.
Use reflexivity.
rewrite the current goal using HCylDef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HfX.
We will prove i ∈ ω ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun f i ∈ U0.
Apply andI to the current goal.
We will prove i ∈ ω ∧ U0 ∈ space_family_topology Xi i.
Apply andI to the current goal.
An exact proof term for the current goal is HiO.
An exact proof term for the current goal is HU0.
We prove the intermediate claim Hfi: apply_fun f i ∈ apply_fun Ufun i.
An exact proof term for the current goal is (Hall i HiO).
We prove the intermediate claim HappUfun: apply_fun Ufun i = U0.
rewrite the current goal using (apply_fun_graph ω (λk : set ⇒ if k = i then U0 else space_family_set Xi k) i HiO) (from left to right).
We prove the intermediate claim Hii: i = i.
Use reflexivity.
rewrite the current goal using (If_i_1 (i = i) U0 (space_family_set Xi i) Hii) (from left to right).
Use reflexivity.
rewrite the current goal using HappUfun (from right to left).
An exact proof term for the current goal is Hfi.
rewrite the current goal using HcylEq (from left to right).
An exact proof term for the current goal is Hb0open.
An exact proof term for the current goal is (topology_generated_by_basis_is_minimal X S Tbox HSsubbasis HTboxTop HSsubTbox).
∎