Let n be given.
Assume Hn: n ∈ ω.
We will prove second_countable_space (euclidean_space n) (euclidean_topology n).
Set Xi to be the term const_space_family n R R_standard_topology.
Set Xprod to be the term product_space n Xi.
Set Tfull to be the term countable_product_topology_subbasis n Xi.
Set B0 to be the term rational_open_intervals_basis.
Set Ssmall to be the term ⋃i ∈ n{product_cylinder n Xi i U|U ∈ B0}.
We prove the intermediate claim HXeq: euclidean_space n = Xprod.
Use reflexivity.
We prove the intermediate claim HTeq: euclidean_topology n = Tfull.
Use reflexivity.
rewrite the current goal using HXeq (from left to right).
rewrite the current goal using HTeq (from left to right).
Apply (xm (n = Empty)) to the current goal.
Assume Hn0: n = Empty.
rewrite the current goal using Hn0 (from left to right).
Set Xi0 to be the term const_space_family Empty R R_standard_topology.
Set X0 to be the term product_space Empty Xi0.
Set T0 to be the term countable_product_topology_subbasis Empty Xi0.
We will prove second_countable_space X0 T0.
We will prove topology_on X0 T0 ∧ ∃B : set, basis_on X0 B ∧ countable_set B ∧ basis_generates X0 B T0.
Apply andI to the current goal.
An exact proof term for the current goal is (countable_product_topology_subbasis_empty_is_topology Xi0).
We use (Sing X0) to witness the existential quantifier.
We will prove basis_on X0 (Sing X0) ∧ countable_set (Sing X0) ∧ basis_generates X0 (Sing X0) T0.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (basis_on_singleton X0).
An exact proof term for the current goal is (finite_countable (Sing X0) (Sing_finite X0)).
We will prove basis_generates X0 (Sing X0) T0.
We will prove basis_on X0 (Sing X0) ∧ generated_topology X0 (Sing X0) = T0.
Apply andI to the current goal.
An exact proof term for the current goal is (basis_on_singleton X0).
We prove the intermediate claim HTdef: T0 = generated_topology_from_subbasis X0 (product_subbasis_full Empty Xi0).
Use reflexivity.
rewrite the current goal using HTdef (from left to right).
We prove the intermediate claim HS0: product_subbasis_full Empty Xi0 = Empty.
An exact proof term for the current goal is (famunion_Empty (λi : set ⇒ {product_cylinder Empty Xi0 i U|U ∈ space_family_topology Xi0 i})).
rewrite the current goal using HS0 (from left to right).
We prove the intermediate claim HTsub0: generated_topology_from_subbasis X0 Empty = generated_topology X0 (basis_of_subbasis X0 Empty).
Use reflexivity.
rewrite the current goal using HTsub0 (from left to right).
We prove the intermediate claim HB0: basis_of_subbasis X0 Empty = {X0}.
We prove the intermediate claim HX0ne: X0 ≠ Empty.
Assume HX0E: X0 = Empty.
We prove the intermediate claim HX0eq: X0 = {Empty}.
An exact proof term for the current goal is (product_space_empty_index Xi0).
We prove the intermediate claim Hem: Empty ∈ X0.
rewrite the current goal using HX0eq (from left to right).
An exact proof term for the current goal is (SingI Empty).
We prove the intermediate claim HemE: Empty ∈ Empty.
rewrite the current goal using HX0E (from right to left) at position 2.
An exact proof term for the current goal is Hem.
An exact proof term for the current goal is (EmptyE Empty HemE False).
An exact proof term for the current goal is (basis_of_subbasis_empty_eq X0 HX0ne).
rewrite the current goal using HB0 (from left to right).
We prove the intermediate claim HSing: (Sing X0) = {X0}.
Use reflexivity.
rewrite the current goal using HSing (from left to right).
Use reflexivity.
Assume HnNe: ¬ (n = Empty).
We prove the intermediate claim HnSub: n ⊆ ω.
An exact proof term for the current goal is (omega_TransSet n Hn).
We prove the intermediate claim HnCount: countable_set n.
An exact proof term for the current goal is (Subq_atleastp n ω HnSub).
We prove the intermediate claim HcompTop: ∀i : set, i ∈ n → topology_on (space_family_set Xi i) (space_family_topology Xi i).
Let i be given.
Assume Hi: i ∈ n.
We prove the intermediate claim HXi: apply_fun Xi i = (R,R_standard_topology).
An exact proof term for the current goal is (const_space_family_apply n R R_standard_topology i Hi).
We prove the intermediate claim HXset: space_family_set Xi i = R.
We prove the intermediate claim HXset_def: space_family_set Xi i = (apply_fun Xi i) 0.
Use reflexivity.
rewrite the current goal using HXset_def (from left to right).
rewrite the current goal using HXi (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 HXtop: space_family_topology Xi i = R_standard_topology.
We prove the intermediate claim HXtop_def: space_family_topology Xi i = (apply_fun Xi i) 1.
Use reflexivity.
rewrite the current goal using HXtop_def (from left to right).
rewrite the current goal using HXi (from left to right).
rewrite the current goal using (tuple_2_1_eq R R_standard_topology) (from left to right).
Use reflexivity.
rewrite the current goal using HXset (from left to right).
rewrite the current goal using HXtop (from left to right).
An exact proof term for the current goal is R_standard_topology_is_topology.
We prove the intermediate claim HSsmall: subbasis_on Xprod Ssmall.
We will prove Ssmall ⊆ 𝒫 Xprod ∧ ⋃ Ssmall = Xprod.
Apply andI to the current goal.
Let s be given.
Assume Hs: s ∈ Ssmall.
We will prove s ∈ 𝒫 Xprod.
Apply PowerI to the current goal.
Let f be given.
Assume Hf: f ∈ s.
We will prove f ∈ Xprod.
Set F to be the term (λi : set ⇒ {product_cylinder n Xi i U|U ∈ B0}).
We prove the intermediate claim HsF: s ∈ (⋃i ∈ nF i).
An exact proof term for the current goal is Hs.
Apply (famunionE_impred n F s HsF (f ∈ Xprod)) to the current goal.
Let i be given.
Assume HiN: i ∈ n.
Assume HsFi: s ∈ F i.
We prove the intermediate claim HexU: ∃U ∈ B0, s = product_cylinder n Xi i U.
An exact proof term for the current goal is (ReplE B0 (λU0 : set ⇒ product_cylinder n Xi i U0) s HsFi).
Apply HexU to the current goal.
Let U be given.
Assume HUand: U ∈ B0 ∧ s = product_cylinder n Xi i U.
We prove the intermediate claim Hseq: s = product_cylinder n Xi i U.
An exact proof term for the current goal is (andER (U ∈ B0) (s = product_cylinder n Xi i U) HUand).
We prove the intermediate claim HfCyl: f ∈ product_cylinder n Xi i U.
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 (product_space n Xi) (λf0 : set ⇒ i ∈ n ∧ U ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U) f HfCyl).
Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ ⋃ Ssmall.
We will prove f ∈ Xprod.
Apply (UnionE_impred Ssmall f Hf) to the current goal.
Let s be given.
Assume Hfs: f ∈ s.
Assume HsS: s ∈ Ssmall.
Set F to be the term (λi : set ⇒ {product_cylinder n Xi i U|U ∈ B0}).
We prove the intermediate claim HsF: s ∈ (⋃i ∈ nF i).
An exact proof term for the current goal is HsS.
Apply (famunionE_impred n F s HsF (f ∈ Xprod)) to the current goal.
Let i be given.
Assume HiN: i ∈ n.
Assume HsFi: s ∈ F i.
We prove the intermediate claim HexU: ∃U ∈ B0, s = product_cylinder n Xi i U.
An exact proof term for the current goal is (ReplE B0 (λU0 : set ⇒ product_cylinder n Xi i U0) s HsFi).
Apply HexU to the current goal.
Let U be given.
Assume HUand: U ∈ B0 ∧ s = product_cylinder n Xi i U.
We prove the intermediate claim HsEq: s = product_cylinder n Xi i U.
An exact proof term for the current goal is (andER (U ∈ B0) (s = product_cylinder n Xi i U) HUand).
We prove the intermediate claim HfCyl: f ∈ product_cylinder n Xi i U.
rewrite the current goal using HsEq (from right to left).
An exact proof term for the current goal is Hfs.
An exact proof term for the current goal is (SepE1 (product_space n Xi) (λf0 : set ⇒ i ∈ n ∧ U ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U) f HfCyl).
Let f be given.
Assume Hf: f ∈ Xprod.
We will prove f ∈ ⋃ Ssmall.
We prove the intermediate claim Hexi0: ∃i0 : set, i0 ∈ n.
An exact proof term for the current goal is (nonempty_has_element n HnNe).
Apply Hexi0 to the current goal.
Let i0 be given.
Assume Hi0: i0 ∈ n.
Set x0 to be the term apply_fun f i0.
We prove the intermediate claim Hx0R: x0 ∈ space_family_set Xi i0.
We prove the intermediate claim Hfpack: (total_function_on f n (space_family_union n Xi) ∧ functional_graph f) ∧ ∀i : set, i ∈ n → apply_fun f i ∈ space_family_set Xi i.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod n (space_family_union n Xi))) (λf0 : set ⇒ (total_function_on f0 n (space_family_union n Xi) ∧ functional_graph f0) ∧ ∀i : set, i ∈ n → apply_fun f0 i ∈ space_family_set Xi i) f Hf).
We prove the intermediate claim Hcoords: ∀i : set, i ∈ n → apply_fun f i ∈ space_family_set Xi i.
An exact proof term for the current goal is (andER (total_function_on f n (space_family_union n Xi) ∧ functional_graph f) (∀i : set, i ∈ n → apply_fun f i ∈ space_family_set Xi i) Hfpack).
An exact proof term for the current goal is (Hcoords i0 Hi0).
We prove the intermediate claim HXi0: apply_fun Xi i0 = (R,R_standard_topology).
An exact proof term for the current goal is (const_space_family_apply n R R_standard_topology i0 Hi0).
We prove the intermediate claim HXset0: space_family_set Xi i0 = R.
We prove the intermediate claim HXset_def: space_family_set Xi i0 = (apply_fun Xi i0) 0.
Use reflexivity.
rewrite the current goal using HXset_def (from left to right).
rewrite the current goal using HXi0 (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 Hx0Rstd: x0 ∈ R.
rewrite the current goal using HXset0 (from right to left).
An exact proof term for the current goal is Hx0R.
We prove the intermediate claim HB0cover: ∀x ∈ R, ∃b ∈ B0, x ∈ b.
We prove the intermediate claim HBasisStd: basis_on R B0 ∧ generated_topology R B0 = R_standard_topology.
An exact proof term for the current goal is ex13_8a_rational_intervals_basis_standard.
We prove the intermediate claim HBasis0: basis_on R B0.
An exact proof term for the current goal is (andEL (basis_on R B0) (generated_topology R B0 = R_standard_topology) HBasisStd).
An exact proof term for the current goal is (basis_on_cover R B0 HBasis0).
We prove the intermediate claim Hexb: ∃b ∈ B0, x0 ∈ b.
An exact proof term for the current goal is (HB0cover x0 Hx0Rstd).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair: b ∈ B0 ∧ x0 ∈ b.
We prove the intermediate claim HbB0: b ∈ B0.
An exact proof term for the current goal is (andEL (b ∈ B0) (x0 ∈ b) Hbpair).
We prove the intermediate claim Hx0b: x0 ∈ b.
An exact proof term for the current goal is (andER (b ∈ B0) (x0 ∈ b) Hbpair).
Set s0 to be the term product_cylinder n Xi i0 b.
We prove the intermediate claim Hs0S: s0 ∈ Ssmall.
Set F to be the term (λi : set ⇒ {product_cylinder n Xi i U|U ∈ B0}).
We will prove s0 ∈ (⋃i ∈ nF i).
An exact proof term for the current goal is (famunionI n F i0 s0 Hi0 (ReplI B0 (λU0 : set ⇒ product_cylinder n Xi i0 U0) b HbB0)).
We will prove f ∈ ⋃ Ssmall.
Apply (UnionI Ssmall f s0) to the current goal.
We will prove f ∈ product_cylinder n Xi i0 b.
We prove the intermediate claim Hcyl_def: product_cylinder n Xi i0 b = {f0 ∈ product_space n Xi|i0 ∈ n ∧ b ∈ space_family_topology Xi i0 ∧ apply_fun f0 i0 ∈ b}.
Use reflexivity.
rewrite the current goal using Hcyl_def (from left to right).
Apply (SepI (product_space n Xi) (λf0 : set ⇒ i0 ∈ n ∧ b ∈ space_family_topology Xi i0 ∧ apply_fun f0 i0 ∈ b) f Hf) to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hi0.
We prove the intermediate claim HBasisStd: basis_on R B0 ∧ generated_topology R B0 = R_standard_topology.
An exact proof term for the current goal is ex13_8a_rational_intervals_basis_standard.
We prove the intermediate claim HbInStd: b ∈ R_standard_topology.
rewrite the current goal using (andER (basis_on R B0) (generated_topology R B0 = R_standard_topology) HBasisStd) (from right to left).
We prove the intermediate claim HBasis0: basis_on R B0.
An exact proof term for the current goal is (andEL (basis_on R B0) (generated_topology R B0 = R_standard_topology) HBasisStd).
An exact proof term for the current goal is (generated_topology_contains_basis R B0 HBasis0 b HbB0).
We prove the intermediate claim HXtop0: space_family_topology Xi i0 = R_standard_topology.
We prove the intermediate claim HXtop_def: space_family_topology Xi i0 = (apply_fun Xi i0) 1.
Use reflexivity.
rewrite the current goal using HXtop_def (from left to right).
rewrite the current goal using HXi0 (from left to right).
rewrite the current goal using (tuple_2_1_eq R R_standard_topology) (from left to right).
Use reflexivity.
rewrite the current goal using HXtop0 (from left to right).
An exact proof term for the current goal is HbInStd.
An exact proof term for the current goal is Hx0b.
An exact proof term for the current goal is Hs0S.
We prove the intermediate claim HSsmall_count: countable_set Ssmall.
We will prove countable_set Ssmall.
Set Bsel to be the term λ_ : set ⇒ B0 of type set → set.
We prove the intermediate claim HB0count: countable_set B0.
An exact proof term for the current goal is rational_open_intervals_basis_countable.
We prove the intermediate claim HSigma: countable (∑i ∈ n, Bsel i).
Apply (Sigma_countable n HnCount Bsel) to the current goal.
Let i be given.
Assume Hi: i ∈ n.
An exact proof term for the current goal is HB0count.
Set Fp to be the term λp : set ⇒ product_cylinder n Xi (p 0) (p 1) of type set → set.
We prove the intermediate claim Himg: countable_set {Fp p|p ∈ ∑i ∈ n, Bsel i}.
An exact proof term for the current goal is (countable_image (∑i ∈ n, Bsel i) HSigma Fp).
We prove the intermediate claim Hsub: Ssmall ⊆ {Fp p|p ∈ ∑i ∈ n, Bsel i}.
Let s be given.
Assume Hs: s ∈ Ssmall.
We will prove s ∈ {Fp p|p ∈ ∑i ∈ n, Bsel i}.
Set Fam to be the term (λi : set ⇒ {product_cylinder n Xi i U|U ∈ B0}).
We prove the intermediate claim HsFam: s ∈ (⋃i ∈ nFam i).
An exact proof term for the current goal is Hs.
Apply (famunionE_impred n Fam s HsFam (s ∈ {Fp p|p ∈ ∑i ∈ n, Bsel i})) to the current goal.
Let i be given.
Assume Hi: i ∈ n.
Assume HsFi: s ∈ Fam i.
We prove the intermediate claim HexU: ∃U ∈ B0, s = product_cylinder n Xi i U.
An exact proof term for the current goal is (ReplE B0 (λU0 : set ⇒ product_cylinder n Xi i U0) s HsFi).
Apply HexU to the current goal.
Let U be given.
Assume HUand: U ∈ B0 ∧ s = product_cylinder n Xi i U.
We prove the intermediate claim HU: U ∈ B0.
An exact proof term for the current goal is (andEL (U ∈ B0) (s = product_cylinder n Xi i U) HUand).
We prove the intermediate claim HsEq: s = product_cylinder n Xi i U.
An exact proof term for the current goal is (andER (U ∈ B0) (s = product_cylinder n Xi i U) HUand).
We prove the intermediate claim HpSig: (i,U) ∈ ∑i0 ∈ n, Bsel i0.
An exact proof term for the current goal is (tuple_2_Sigma n Bsel i Hi U HU).
We prove the intermediate claim HFp: Fp (i,U) = product_cylinder n Xi i U.
We prove the intermediate claim HFdef: Fp (i,U) = product_cylinder n Xi ((i,U) 0) ((i,U) 1).
Use reflexivity.
rewrite the current goal using HFdef (from left to right).
rewrite the current goal using (tuple_2_0_eq i U) (from left to right).
rewrite the current goal using (tuple_2_1_eq i U) (from left to right).
Use reflexivity.
rewrite the current goal using HsEq (from left to right).
rewrite the current goal using HFp (from right to left).
An exact proof term for the current goal is (ReplI (∑i0 ∈ n, Bsel i0) Fp (i,U) HpSig).
An exact proof term for the current goal is (Subq_countable Ssmall {Fp p|p ∈ ∑i ∈ n, Bsel i} Himg Hsub).
We prove the intermediate claim HTfull_top: topology_on Xprod Tfull.
An exact proof term for the current goal is (topology_from_subbasis_is_topology Xprod (product_subbasis_full n Xi) (product_subbasis_full_subbasis_on n Xi HnNe HcompTop)).
We prove the intermediate claim HTeq2: generated_topology_from_subbasis Xprod Ssmall = Tfull.
Apply set_ext to the current goal.
Let U be given.
Assume HU: U ∈ generated_topology_from_subbasis Xprod Ssmall.
We will prove U ∈ Tfull.
We prove the intermediate claim HSfull: subbasis_on Xprod (product_subbasis_full n Xi).
An exact proof term for the current goal is (product_subbasis_full_subbasis_on n Xi HnNe HcompTop).
We prove the intermediate claim HSsmall_sub: Ssmall ⊆ product_subbasis_full n Xi.
Let s be given.
Assume Hs: s ∈ Ssmall.
We will prove s ∈ product_subbasis_full n Xi.
Set Fam to be the term (λi : set ⇒ {product_cylinder n Xi i U0|U0 ∈ B0}).
We prove the intermediate claim HsFam: s ∈ (⋃i ∈ nFam i).
An exact proof term for the current goal is Hs.
Apply (famunionE_impred n Fam s HsFam (s ∈ product_subbasis_full n Xi)) to the current goal.
Let i be given.
Assume Hi: i ∈ n.
Assume HsFi: s ∈ Fam i.
We prove the intermediate claim HexU: ∃U0 ∈ B0, s = product_cylinder n Xi i U0.
An exact proof term for the current goal is (ReplE B0 (λU0 : set ⇒ product_cylinder n Xi i U0) s HsFi).
Apply HexU to the current goal.
Let U0 be given.
Assume HUand: U0 ∈ B0 ∧ s = product_cylinder n Xi i U0.
We prove the intermediate claim HU0: U0 ∈ B0.
An exact proof term for the current goal is (andEL (U0 ∈ B0) (s = product_cylinder n Xi i U0) HUand).
We prove the intermediate claim HsEq: s = product_cylinder n Xi i U0.
An exact proof term for the current goal is (andER (U0 ∈ B0) (s = product_cylinder n Xi i U0) HUand).
rewrite the current goal using HsEq (from left to right).
We prove the intermediate claim HBasisStd: basis_on R B0 ∧ generated_topology R B0 = R_standard_topology.
An exact proof term for the current goal is ex13_8a_rational_intervals_basis_standard.
We prove the intermediate claim HBasis0: basis_on R B0.
An exact proof term for the current goal is (andEL (basis_on R B0) (generated_topology R B0 = R_standard_topology) HBasisStd).
We prove the intermediate claim HU0std: U0 ∈ R_standard_topology.
rewrite the current goal using (andER (basis_on R B0) (generated_topology R B0 = R_standard_topology) HBasisStd) (from right to left).
An exact proof term for the current goal is (generated_topology_contains_basis R B0 HBasis0 U0 HU0).
We prove the intermediate claim HXi_i: apply_fun Xi i = (R,R_standard_topology).
An exact proof term for the current goal is (const_space_family_apply n R R_standard_topology i Hi).
We prove the intermediate claim HXtopi: space_family_topology Xi i = R_standard_topology.
We prove the intermediate claim HXtop_def: space_family_topology Xi i = (apply_fun Xi i) 1.
Use reflexivity.
rewrite the current goal using HXtop_def (from left to right).
rewrite the current goal using HXi_i (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 HU0top: U0 ∈ space_family_topology Xi i.
rewrite the current goal using HXtopi (from left to right).
An exact proof term for the current goal is HU0std.
Set Ffull to be the term (λj : set ⇒ {product_cylinder n Xi j Uj|Uj ∈ space_family_topology Xi j}).
We will prove product_cylinder n Xi i U0 ∈ (⋃j ∈ nFfull j).
An exact proof term for the current goal is (famunionI n Ffull i (product_cylinder n Xi i U0) Hi (ReplI (space_family_topology Xi i) (λUj : set ⇒ product_cylinder n Xi i Uj) U0 HU0top)).
We prove the intermediate claim HTsub: topology_on Xprod Tfull.
An exact proof term for the current goal is HTfull_top.
We prove the intermediate claim HSsmall_in_Tfull: Ssmall ⊆ Tfull.
Let s be given.
Assume Hs: s ∈ Ssmall.
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis Xprod (product_subbasis_full n Xi) s (product_subbasis_full_subbasis_on n Xi HnNe HcompTop) (HSsmall_sub s Hs)).
We prove the intermediate claim Hinc: generated_topology_from_subbasis Xprod Ssmall ⊆ Tfull.
An exact proof term for the current goal is (topology_generated_by_basis_is_minimal Xprod Ssmall Tfull HSsmall HTsub HSsmall_in_Tfull).
An exact proof term for the current goal is (Hinc U HU).
Let U be given.
Assume HU: U ∈ Tfull.
We will prove U ∈ generated_topology_from_subbasis Xprod Ssmall.
Set Tsmall to be the term generated_topology_from_subbasis Xprod Ssmall.
We prove the intermediate claim HTsmall: topology_on Xprod Tsmall.
An exact proof term for the current goal is (topology_from_subbasis_is_topology Xprod Ssmall HSsmall).
We prove the intermediate claim HSfull: subbasis_on Xprod (product_subbasis_full n Xi).
An exact proof term for the current goal is (product_subbasis_full_subbasis_on n Xi HnNe HcompTop).
We prove the intermediate claim HSubFull: product_subbasis_full n Xi ⊆ Tsmall.
Let s be given.
Assume Hs: s ∈ product_subbasis_full n Xi.
We will prove s ∈ Tsmall.
Set Ffull to be the term (λi : set ⇒ {product_cylinder n Xi i U0|U0 ∈ space_family_topology Xi i}).
We prove the intermediate claim HsF: s ∈ (⋃i ∈ nFfull i).
An exact proof term for the current goal is Hs.
Apply (famunionE_impred n Ffull s HsF (s ∈ Tsmall)) to the current goal.
Let i be given.
Assume Hi: i ∈ n.
Assume HsFi: s ∈ Ffull i.
We prove the intermediate claim HexU0: ∃U0 ∈ space_family_topology Xi i, s = product_cylinder n Xi i U0.
An exact proof term for the current goal is (ReplE (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder n Xi i U0) s HsFi).
Apply HexU0 to the current goal.
Let U0 be given.
Assume HU0and: U0 ∈ space_family_topology Xi i ∧ s = product_cylinder n Xi i U0.
We prove the intermediate claim HU0top: U0 ∈ space_family_topology Xi i.
An exact proof term for the current goal is (andEL (U0 ∈ space_family_topology Xi i) (s = product_cylinder n Xi i U0) HU0and).
We prove the intermediate claim HsEq: s = product_cylinder n Xi i U0.
An exact proof term for the current goal is (andER (U0 ∈ space_family_topology Xi i) (s = product_cylinder n Xi i U0) HU0and).
rewrite the current goal using HsEq (from left to right).
Set Fam to be the term {b ∈ B0|b ⊆ U0}.
Set UFam to be the term {product_cylinder n Xi i b|b ∈ Fam}.
We prove the intermediate claim HUFamSub: UFam ⊆ Tsmall.
Let c be given.
Assume Hc: c ∈ UFam.
We will prove c ∈ Tsmall.
We prove the intermediate claim Hexb: ∃b ∈ Fam, c = product_cylinder n Xi i b.
An exact proof term for the current goal is (ReplE Fam (λb0 : set ⇒ product_cylinder n Xi i b0) c Hc).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbFam: b ∈ Fam.
An exact proof term for the current goal is (andEL (b ∈ Fam) (c = product_cylinder n Xi i b) Hbpair).
We prove the intermediate claim HcEq: c = product_cylinder n Xi i b.
An exact proof term for the current goal is (andER (b ∈ Fam) (c = product_cylinder n Xi i b) Hbpair).
rewrite the current goal using HcEq (from left to right).
We prove the intermediate claim HbB0: b ∈ B0.
An exact proof term for the current goal is (SepE1 B0 (λb0 : set ⇒ b0 ⊆ U0) b HbFam).
We prove the intermediate claim HcSsmall: product_cylinder n Xi i b ∈ Ssmall.
Set F to be the term (λj : set ⇒ {product_cylinder n Xi j Uj|Uj ∈ B0}).
We will prove product_cylinder n Xi i b ∈ (⋃j ∈ nF j).
An exact proof term for the current goal is (famunionI n F i (product_cylinder n Xi i b) Hi (ReplI B0 (λUj : set ⇒ product_cylinder n Xi i Uj) b HbB0)).
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis Xprod Ssmall (product_cylinder n Xi i b) HSsmall HcSsmall).
We prove the intermediate claim HcylEq: product_cylinder n Xi i U0 = ⋃ UFam.
Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ product_cylinder n Xi i U0.
We will prove f ∈ ⋃ UFam.
We prove the intermediate claim HfX: f ∈ Xprod.
An exact proof term for the current goal is (SepE1 Xprod (λf0 : set ⇒ i ∈ n ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U0) f Hf).
We prove the intermediate claim Hpred: (i ∈ n ∧ U0 ∈ space_family_topology Xi i) ∧ apply_fun f i ∈ U0.
An exact proof term for the current goal is (SepE2 Xprod (λf0 : set ⇒ i ∈ n ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U0) f Hf).
We prove the intermediate claim Hiu: i ∈ n ∧ U0 ∈ space_family_topology Xi i.
An exact proof term for the current goal is (andEL (i ∈ n ∧ U0 ∈ space_family_topology Xi i) (apply_fun f i ∈ U0) Hpred).
We prove the intermediate claim HiN: i ∈ n.
An exact proof term for the current goal is (andEL (i ∈ n) (U0 ∈ space_family_topology Xi i) Hiu).
We prove the intermediate claim HU0top2: U0 ∈ space_family_topology Xi i.
An exact proof term for the current goal is (andER (i ∈ n) (U0 ∈ space_family_topology Xi i) Hiu).
We prove the intermediate claim HfiU0: apply_fun f i ∈ U0.
An exact proof term for the current goal is (andER (i ∈ n ∧ U0 ∈ space_family_topology Xi i) (apply_fun f i ∈ U0) Hpred).
We prove the intermediate claim HXi_i: apply_fun Xi i = (R,R_standard_topology).
An exact proof term for the current goal is (const_space_family_apply n R R_standard_topology i HiN).
We prove the intermediate claim HXtopi: space_family_topology Xi i = R_standard_topology.
We prove the intermediate claim HXtop_def: space_family_topology Xi i = (apply_fun Xi i) 1.
Use reflexivity.
rewrite the current goal using HXtop_def (from left to right).
rewrite the current goal using HXi_i (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 HU0std: U0 ∈ R_standard_topology.
rewrite the current goal using HXtopi (from right to left).
An exact proof term for the current goal is HU0top2.
We prove the intermediate claim HBasisStd: basis_on R B0 ∧ generated_topology R B0 = R_standard_topology.
An exact proof term for the current goal is ex13_8a_rational_intervals_basis_standard.
We prove the intermediate claim HU0gen: U0 ∈ generated_topology R B0.
rewrite the current goal using (andER (basis_on R B0) (generated_topology R B0 = R_standard_topology) HBasisStd) (from left to right).
An exact proof term for the current goal is HU0std.
We prove the intermediate claim HU0loc: ∀x ∈ U0, ∃b ∈ B0, x ∈ b ∧ b ⊆ U0.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU : set ⇒ ∀x0 ∈ U, ∃b ∈ B0, x0 ∈ b ∧ b ⊆ U) U0 HU0gen).
We prove the intermediate claim Hexb: ∃b ∈ B0, apply_fun f i ∈ b ∧ b ⊆ U0.
An exact proof term for the current goal is (HU0loc (apply_fun f i) HfiU0).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbB0: b ∈ B0.
An exact proof term for the current goal is (andEL (b ∈ B0) (apply_fun f i ∈ b ∧ b ⊆ U0) Hbpair).
We prove the intermediate claim Hbib: apply_fun f i ∈ b ∧ b ⊆ U0.
An exact proof term for the current goal is (andER (b ∈ B0) (apply_fun f i ∈ b ∧ b ⊆ U0) Hbpair).
We prove the intermediate claim Hfib: apply_fun f i ∈ b.
An exact proof term for the current goal is (andEL (apply_fun f i ∈ b) (b ⊆ U0) Hbib).
We prove the intermediate claim HbSub: b ⊆ U0.
An exact proof term for the current goal is (andER (apply_fun f i ∈ b) (b ⊆ U0) Hbib).
We prove the intermediate claim HbFam: b ∈ Fam.
An exact proof term for the current goal is (SepI B0 (λb0 : set ⇒ b0 ⊆ U0) b HbB0 HbSub).
Set c to be the term product_cylinder n Xi i b.
We prove the intermediate claim HcUFam: c ∈ UFam.
An exact proof term for the current goal is (ReplI Fam (λb0 : set ⇒ product_cylinder n Xi i b0) b HbFam).
Apply (UnionI UFam f c) to the current goal.
We will prove f ∈ product_cylinder n Xi i b.
We prove the intermediate claim Hcyl_def: product_cylinder n Xi i b = {f0 ∈ Xprod|i ∈ n ∧ b ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ b}.
Use reflexivity.
rewrite the current goal using Hcyl_def (from left to right).
Apply (SepI Xprod (λf0 : set ⇒ i ∈ n ∧ b ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ b) f HfX) to the current goal.
We prove the intermediate claim Hleft: i ∈ n ∧ b ∈ space_family_topology Xi i.
We prove the intermediate claim HbStd: b ∈ R_standard_topology.
rewrite the current goal using (andER (basis_on R B0) (generated_topology R B0 = R_standard_topology) HBasisStd) (from right to left).
We prove the intermediate claim HBasis0: basis_on R B0.
An exact proof term for the current goal is (andEL (basis_on R B0) (generated_topology R B0 = R_standard_topology) HBasisStd).
An exact proof term for the current goal is (generated_topology_contains_basis R B0 HBasis0 b HbB0).
We prove the intermediate claim HbTop: b ∈ space_family_topology Xi i.
rewrite the current goal using HXtopi (from left to right).
An exact proof term for the current goal is HbStd.
An exact proof term for the current goal is (andI (i ∈ n) (b ∈ space_family_topology Xi i) HiN HbTop).
An exact proof term for the current goal is (andI (i ∈ n ∧ b ∈ space_family_topology Xi i) (apply_fun f i ∈ b) Hleft Hfib).
An exact proof term for the current goal is HcUFam.
Let f be given.
Assume Hf: f ∈ ⋃ UFam.
We will prove f ∈ product_cylinder n Xi i U0.
Apply (UnionE_impred UFam f Hf) to the current goal.
Let c be given.
Assume Hfc: f ∈ c.
Assume Hc: c ∈ UFam.
We prove the intermediate claim Hexb: ∃b ∈ Fam, c = product_cylinder n Xi i b.
An exact proof term for the current goal is (ReplE Fam (λb0 : set ⇒ product_cylinder n Xi i b0) c Hc).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbFam: b ∈ Fam.
An exact proof term for the current goal is (andEL (b ∈ Fam) (c = product_cylinder n Xi i b) Hbpair).
We prove the intermediate claim HcEq: c = product_cylinder n Xi i b.
An exact proof term for the current goal is (andER (b ∈ Fam) (c = product_cylinder n Xi i b) Hbpair).
We prove the intermediate claim HbSub: b ⊆ U0.
An exact proof term for the current goal is (SepE2 B0 (λb0 : set ⇒ b0 ⊆ U0) b HbFam).
We prove the intermediate claim HfCyl: f ∈ product_cylinder n Xi i b.
rewrite the current goal using HcEq (from right to left).
An exact proof term for the current goal is Hfc.
We prove the intermediate claim Hpredb: (i ∈ n ∧ b ∈ space_family_topology Xi i) ∧ apply_fun f i ∈ b.
An exact proof term for the current goal is (SepE2 Xprod (λf0 : set ⇒ i ∈ n ∧ b ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ b) f HfCyl).
We prove the intermediate claim Hiu: i ∈ n ∧ b ∈ space_family_topology Xi i.
An exact proof term for the current goal is (andEL (i ∈ n ∧ b ∈ space_family_topology Xi i) (apply_fun f i ∈ b) Hpredb).
We prove the intermediate claim HiN: i ∈ n.
An exact proof term for the current goal is (andEL (i ∈ n) (b ∈ space_family_topology Xi i) Hiu).
We prove the intermediate claim Hfib: apply_fun f i ∈ b.
An exact proof term for the current goal is (andER (i ∈ n ∧ b ∈ space_family_topology Xi i) (apply_fun f i ∈ b) Hpredb).
We prove the intermediate claim HfiU0: apply_fun f i ∈ U0.
An exact proof term for the current goal is (HbSub (apply_fun f i) Hfib).
We prove the intermediate claim HfX: f ∈ Xprod.
An exact proof term for the current goal is (SepE1 Xprod (λf0 : set ⇒ i ∈ n ∧ b ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ b) f HfCyl).
We prove the intermediate claim HcylU0_def: product_cylinder n Xi i U0 = {f0 ∈ Xprod|i ∈ n ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U0}.
Use reflexivity.
rewrite the current goal using HcylU0_def (from left to right).
Apply (SepI Xprod (λf0 : set ⇒ i ∈ n ∧ U0 ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U0) f HfX) to the current goal.
We prove the intermediate claim Hleft: i ∈ n ∧ U0 ∈ space_family_topology Xi i.
An exact proof term for the current goal is (andI (i ∈ n) (U0 ∈ space_family_topology Xi i) HiN HU0top).
An exact proof term for the current goal is (andI (i ∈ n ∧ U0 ∈ space_family_topology Xi i) (apply_fun f i ∈ U0) Hleft HfiU0).
We prove the intermediate claim HUFamSub2: UFam ⊆ Tsmall.
Let c be given.
Assume Hc: c ∈ UFam.
An exact proof term for the current goal is (HUFamSub c Hc).
We prove the intermediate claim HUnionOpen: ⋃ UFam ∈ Tsmall.
An exact proof term for the current goal is (topology_union_closed Xprod Tsmall UFam HTsmall HUFamSub2).
rewrite the current goal using HcylEq (from left to right).
An exact proof term for the current goal is HUnionOpen.
We prove the intermediate claim Hinc: generated_topology_from_subbasis Xprod (product_subbasis_full n Xi) ⊆ Tsmall.
An exact proof term for the current goal is (topology_generated_by_basis_is_minimal Xprod (product_subbasis_full n Xi) Tsmall HSfull HTsmall HSubFull).
An exact proof term for the current goal is (Hinc U HU).
We will prove topology_on Xprod Tfull ∧ ∃B : set, basis_on Xprod B ∧ countable_set B ∧ basis_generates Xprod B Tfull.
Apply andI to the current goal.
An exact proof term for the current goal is HTfull_top.
We use (basis_of_subbasis Xprod Ssmall) to witness the existential quantifier.
We will prove basis_on Xprod (basis_of_subbasis Xprod Ssmall) ∧ countable_set (basis_of_subbasis Xprod Ssmall) ∧ basis_generates Xprod (basis_of_subbasis Xprod Ssmall) Tfull.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (finite_intersections_basis_of_subbasis Xprod Ssmall HSsmall).
An exact proof term for the current goal is (basis_of_subbasis_countable Xprod Ssmall HSsmall_count).
We will prove basis_generates Xprod (basis_of_subbasis Xprod Ssmall) Tfull.
We will prove basis_on Xprod (basis_of_subbasis Xprod Ssmall) ∧ generated_topology Xprod (basis_of_subbasis Xprod Ssmall) = Tfull.
Apply andI to the current goal.
An exact proof term for the current goal is (finite_intersections_basis_of_subbasis Xprod Ssmall HSsmall).
We prove the intermediate claim HTsub: generated_topology_from_subbasis Xprod Ssmall = generated_topology Xprod (basis_of_subbasis Xprod Ssmall).
Use reflexivity.
rewrite the current goal using HTsub (from right to left).
An exact proof term for the current goal is HTeq2.
∎