Let X and Tx be given.
Assume HTx: topology_on X Tx.
Assume Hclosed: one_point_sets_closed X Tx.
Let F and J be given.
Assume Hsep: separating_family_of_functions X Tx F J.
We will prove ∃Fmap : set, embedding_of X Tx (power_real J) (product_topology_full J (const_space_family J R R_standard_topology)) Fmap.
Set Fmap to be the term diagonal_map X F J.
We use Fmap to witness the existential quantifier.
Set Xi to be the term const_space_family J R R_standard_topology.
Set Ty to be the term product_topology_full J Xi.
We prove the intermediate claim HcontFmap: continuous_map X Tx (power_real J) Ty Fmap.
We prove the intermediate claim HpR: power_real J = product_space J Xi.
Use reflexivity.
We prove the intermediate claim HTyDef: Ty = product_topology_full J Xi.
Use reflexivity.
rewrite the current goal using HpR (from left to right).
rewrite the current goal using HTyDef (from left to right).
We will prove continuous_map X Tx (product_space J Xi) (product_topology_full J Xi) Fmap.
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
We prove the intermediate claim HdiagDef: diagonal_map X F J = graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
We prove the intermediate claim HsepCore: (topology_on X Tx ∧ total_function_on F J (function_space X R)) ∧ (∀j0 : set, j0 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j0)).
An exact proof term for the current goal is (andEL ((topology_on X Tx ∧ total_function_on F J (function_space X R)) ∧ (∀j0 : set, j0 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j0))) (∀x0 : set, x0 ∈ X → ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → ∃j0 : set, j0 ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j0) x0) ∧ ∀x1 : set, x1 ∈ X ∖ U0 → apply_fun (apply_fun F j0) x1 = 0) Hsep).
We prove the intermediate claim HtopTot: topology_on X Tx ∧ total_function_on F J (function_space X R).
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ total_function_on F J (function_space X R)) (∀j0 : set, j0 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j0)) HsepCore).
We prove the intermediate claim Htot: total_function_on F J (function_space X R).
An exact proof term for the current goal is (andER (topology_on X Tx) (total_function_on F J (function_space X R)) HtopTot).
We prove the intermediate claim HfunPow: function_on Fmap X (power_real J).
rewrite the current goal using HFmapDef (from left to right).
An exact proof term for the current goal is (diagonal_map_function_on_power_real X F J Htot).
We prove the intermediate claim Hfun: function_on Fmap X (product_space J Xi).
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun Fmap x ∈ product_space J Xi.
rewrite the current goal using HpR (from right to left).
An exact proof term for the current goal is (HfunPow x HxX).
Apply (xm (J = Empty)) to the current goal.
Assume HJ0: J = Empty.
rewrite the current goal using HJ0 (from left to right).
We prove the intermediate claim HTy0: topology_on (product_space Empty Xi) (product_topology_full Empty Xi).
An exact proof term for the current goal is (product_topology_full_empty_is_topology Xi).
We prove the intermediate claim HX0: product_space Empty Xi = {Empty}.
An exact proof term for the current goal is (product_space_empty_index Xi).
We prove the intermediate claim HEmptyY: Empty ∈ product_space Empty Xi.
rewrite the current goal using HX0 (from left to right).
An exact proof term for the current goal is (SingI Empty).
We prove the intermediate claim HXieq: Xi = const_space_family Empty R R_standard_topology.
We prove the intermediate claim HXidef: Xi = const_space_family J R R_standard_topology.
Use reflexivity.
rewrite the current goal using HXidef (from left to right).
rewrite the current goal using HJ0 (from left to right).
Use reflexivity.
We prove the intermediate claim HFmapConst: Fmap = const_fun X Empty.
We prove the intermediate claim HFmapE: Fmap = diagonal_map X F Empty.
rewrite the current goal using HFmapDef (from left to right).
rewrite the current goal using HJ0 (from left to right).
Use reflexivity.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ Fmap.
We will prove p ∈ const_fun X Empty.
We prove the intermediate claim HpDiag: p ∈ diagonal_map X F Empty.
rewrite the current goal using HFmapE (from right to left).
An exact proof term for the current goal is Hp.
We prove the intermediate claim Hdiag0: diagonal_map X F Empty = graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
We prove the intermediate claim HpGraph: p ∈ graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
rewrite the current goal using Hdiag0 (from right to left).
An exact proof term for the current goal is HpDiag.
Apply (ReplE_impred X (λx0 : set ⇒ (x0,graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0))) p HpGraph (p ∈ const_fun X Empty)) to the current goal.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Assume Hpeq: p = (x0,graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
We prove the intermediate claim Hem: graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0) = Empty.
We prove the intermediate claim HgraphDef: graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0) = {(j0,apply_fun (apply_fun F j0) x0)|j0 ∈ Empty}.
Use reflexivity.
rewrite the current goal using HgraphDef (from left to right).
An exact proof term for the current goal is (Repl_Empty (λj0 : set ⇒ (j0,apply_fun (apply_fun F j0) x0))).
rewrite the current goal using Hpeq (from left to right).
rewrite the current goal using Hem (from left to right).
An exact proof term for the current goal is (ReplI X (λa0 : set ⇒ (a0,Empty)) x0 Hx0X).
Let p be given.
Assume Hp: p ∈ const_fun X Empty.
We will prove p ∈ Fmap.
We prove the intermediate claim HFmapE: Fmap = diagonal_map X F Empty.
rewrite the current goal using HFmapDef (from left to right).
rewrite the current goal using HJ0 (from left to right).
Use reflexivity.
We prove the intermediate claim Hdiag0: diagonal_map X F Empty = graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
We prove the intermediate claim HpGraph: p ∈ graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Apply (ReplE_impred X (λa0 : set ⇒ (a0,Empty)) p Hp (p ∈ graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)))) to the current goal.
Let x2 be given.
Assume Hx2X: x2 ∈ X.
Assume Hpeq: p = (x2,Empty).
We prove the intermediate claim Hem: graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x2) = Empty.
We prove the intermediate claim HgraphDef: graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x2) = {(j0,apply_fun (apply_fun F j0) x2)|j0 ∈ Empty}.
Use reflexivity.
rewrite the current goal using HgraphDef (from left to right).
An exact proof term for the current goal is (Repl_Empty (λj0 : set ⇒ (j0,apply_fun (apply_fun F j0) x2))).
We prove the intermediate claim HpEq2: p = (x2,graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x2)).
rewrite the current goal using Hpeq (from left to right).
rewrite the current goal using Hem (from left to right).
Use reflexivity.
rewrite the current goal using HpEq2 (from left to right).
An exact proof term for the current goal is (ReplI X (λx1 : set ⇒ (x1,graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x1))) x2 Hx2X).
We prove the intermediate claim HpDiag: p ∈ diagonal_map X F Empty.
rewrite the current goal using Hdiag0 (from left to right).
An exact proof term for the current goal is HpGraph.
rewrite the current goal using HFmapE (from left to right).
An exact proof term for the current goal is HpDiag.
We prove the intermediate claim HdiagConst: diagonal_map X F Empty = const_fun X Empty.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ diagonal_map X F Empty.
We will prove p ∈ const_fun X Empty.
We prove the intermediate claim Hdiag0: diagonal_map X F Empty = graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
We prove the intermediate claim HpGraph: p ∈ graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
rewrite the current goal using Hdiag0 (from right to left).
An exact proof term for the current goal is Hp.
Apply (ReplE_impred X (λx0 : set ⇒ (x0,graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0))) p HpGraph (p ∈ const_fun X Empty)) to the current goal.
Let x0 be given.
Assume Hx0X: x0 ∈ X.
Assume Hpeq: p = (x0,graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
We prove the intermediate claim Hem: graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0) = Empty.
We prove the intermediate claim HgraphDef: graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0) = {(j0,apply_fun (apply_fun F j0) x0)|j0 ∈ Empty}.
Use reflexivity.
rewrite the current goal using HgraphDef (from left to right).
An exact proof term for the current goal is (Repl_Empty (λj0 : set ⇒ (j0,apply_fun (apply_fun F j0) x0))).
rewrite the current goal using Hpeq (from left to right).
rewrite the current goal using Hem (from left to right).
An exact proof term for the current goal is (ReplI X (λa0 : set ⇒ (a0,Empty)) x0 Hx0X).
Let p be given.
Assume Hp: p ∈ const_fun X Empty.
We will prove p ∈ diagonal_map X F Empty.
We prove the intermediate claim Hdiag0: diagonal_map X F Empty = graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
We prove the intermediate claim HpGraph: p ∈ graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Apply (ReplE_impred X (λa0 : set ⇒ (a0,Empty)) p Hp (p ∈ graph X (λx0 : set ⇒ graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)))) to the current goal.
Let x2 be given.
Assume Hx2X: x2 ∈ X.
Assume Hpeq: p = (x2,Empty).
We prove the intermediate claim Hem: graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x2) = Empty.
We prove the intermediate claim HgraphDef: graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x2) = {(j0,apply_fun (apply_fun F j0) x2)|j0 ∈ Empty}.
Use reflexivity.
rewrite the current goal using HgraphDef (from left to right).
An exact proof term for the current goal is (Repl_Empty (λj0 : set ⇒ (j0,apply_fun (apply_fun F j0) x2))).
We prove the intermediate claim HpEq2: p = (x2,graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x2)).
rewrite the current goal using Hpeq (from left to right).
rewrite the current goal using Hem (from left to right).
Use reflexivity.
rewrite the current goal using HpEq2 (from left to right).
An exact proof term for the current goal is (ReplI X (λx1 : set ⇒ (x1,graph Empty (λj0 : set ⇒ apply_fun (apply_fun F j0) x1))) x2 Hx2X).
rewrite the current goal using Hdiag0 (from left to right).
An exact proof term for the current goal is HpGraph.
We prove the intermediate claim Hconst: continuous_map X Tx (product_space Empty Xi) (product_topology_full Empty Xi) (const_fun X Empty).
An exact proof term for the current goal is (const_fun_continuous X Tx (product_space Empty Xi) (product_topology_full Empty Xi) Empty HTx HTy0 HEmptyY).
rewrite the current goal using HdiagConst (from left to right).
rewrite the current goal using HXieq (from right to left).
An exact proof term for the current goal is Hconst.
Assume HJne: J ≠ Empty.
We prove the intermediate claim HcompTop: ∀i : set, i ∈ J → topology_on (space_family_set Xi i) (space_family_topology Xi i).
Let i be given.
Assume HiJ: i ∈ J.
We prove the intermediate claim Hset: space_family_set Xi i = R.
An exact proof term for the current goal is (space_family_set_const_space_family J R R_standard_topology i HiJ).
We prove the intermediate claim Htop: space_family_topology Xi i = R_standard_topology.
An exact proof term for the current goal is (space_family_topology_const_space_family J R R_standard_topology i HiJ).
rewrite the current goal using Hset (from left to right).
rewrite the current goal using Htop (from left to right).
An exact proof term for the current goal is R_standard_topology_is_topology.
We prove the intermediate claim HSsub: subbasis_on (product_space J Xi) (product_subbasis_full J Xi).
An exact proof term for the current goal is (product_subbasis_full_subbasis_on J Xi HJne HcompTop).
We prove the intermediate claim HcontCoord: ∀j0 : set, j0 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j0).
An exact proof term for the current goal is (andER (topology_on X Tx ∧ total_function_on F J (function_space X R)) (∀j0 : set, j0 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j0)) HsepCore).
Apply (continuous_map_from_subbasis X Tx (product_space J Xi) (product_subbasis_full J Xi) Fmap HTx Hfun HSsub) to the current goal.
Let s be given.
Assume HsS: s ∈ product_subbasis_full J Xi.
We will prove preimage_of X Fmap s ∈ Tx.
Set Fam to be the term (λi0 : set ⇒ {product_cylinder J Xi i0 U0|U0 ∈ space_family_topology Xi i0}).
We prove the intermediate claim HsFam: s ∈ (⋃i0 ∈ JFam i0).
An exact proof term for the current goal is HsS.
Apply (famunionE_impred J Fam s HsFam (preimage_of X Fmap s ∈ Tx)) to the current goal.
Let i be given.
Assume HiJ: i ∈ J.
Assume HsFi: s ∈ Fam i.
We prove the intermediate claim HexU: ∃U ∈ space_family_topology Xi i, s = product_cylinder J Xi i U.
An exact proof term for the current goal is (ReplE (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder J Xi i U0) s HsFi).
Apply HexU to the current goal.
Let U be given.
Assume HUand: U ∈ space_family_topology Xi i ∧ s = product_cylinder J Xi i U.
We prove the intermediate claim HUtop: U ∈ space_family_topology Xi i.
An exact proof term for the current goal is (andEL (U ∈ space_family_topology Xi i) (s = product_cylinder J Xi i U) HUand).
We prove the intermediate claim Hseq: s = product_cylinder J Xi i U.
An exact proof term for the current goal is (andER (U ∈ space_family_topology Xi i) (s = product_cylinder J Xi i U) HUand).
rewrite the current goal using Hseq (from left to right).
We prove the intermediate claim Hconti: continuous_map X Tx R R_standard_topology (apply_fun F i).
An exact proof term for the current goal is (HcontCoord i HiJ).
We prove the intermediate claim HUstd: U ∈ R_standard_topology.
We prove the intermediate claim Htopi: space_family_topology Xi i = R_standard_topology.
An exact proof term for the current goal is (space_family_topology_const_space_family J R R_standard_topology i HiJ).
rewrite the current goal using Htopi (from right to left).
An exact proof term for the current goal is HUtop.
We prove the intermediate claim HpreEq: preimage_of X Fmap (product_cylinder J Xi i U) = preimage_of X (apply_fun F i) U.
Apply set_ext to the current goal.
Let x be given.
Assume HxPre: x ∈ preimage_of X Fmap (product_cylinder J Xi i U).
We will prove x ∈ preimage_of X (apply_fun F i) U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun Fmap x0 ∈ product_cylinder J Xi i U) x HxPre).
We prove the intermediate claim HfxCyl: apply_fun Fmap x ∈ product_cylinder J Xi i U.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun Fmap x0 ∈ product_cylinder J Xi i U) x HxPre).
We prove the intermediate claim HcylProp: i ∈ J ∧ U ∈ space_family_topology Xi i ∧ apply_fun (apply_fun Fmap x) i ∈ U.
An exact proof term for the current goal is (SepE2 (product_space J Xi) (λf0 : set ⇒ i ∈ J ∧ U ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U) (apply_fun Fmap x) HfxCyl).
We prove the intermediate claim HcoordU: apply_fun (apply_fun Fmap x) i ∈ U.
We prove the intermediate claim H12: i ∈ J ∧ U ∈ space_family_topology Xi i.
An exact proof term for the current goal is (andEL (i ∈ J ∧ U ∈ space_family_topology Xi i) (apply_fun (apply_fun Fmap x) i ∈ U) HcylProp).
An exact proof term for the current goal is (andER (i ∈ J ∧ U ∈ space_family_topology Xi i) (apply_fun (apply_fun Fmap x) i ∈ U) HcylProp).
We prove the intermediate claim HFmapx: apply_fun Fmap x = graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x).
rewrite the current goal using HFmapDef (from left to right).
rewrite the current goal using HdiagDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)) x HxX).
We prove the intermediate claim HcoordEq: apply_fun (apply_fun Fmap x) i = apply_fun (apply_fun F i) x.
rewrite the current goal using HFmapx (from left to right).
rewrite the current goal using (apply_fun_graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x) i HiJ) (from left to right).
Use reflexivity.
We prove the intermediate claim HfiU: apply_fun (apply_fun F i) x ∈ U.
rewrite the current goal using HcoordEq (from right to left).
An exact proof term for the current goal is HcoordU.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun (apply_fun F i) x0 ∈ U) x HxX HfiU).
Let x be given.
Assume HxPre: x ∈ preimage_of X (apply_fun F i) U.
We will prove x ∈ preimage_of X Fmap (product_cylinder J Xi i U).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun (apply_fun F i) x0 ∈ U) x HxPre).
We prove the intermediate claim HfiU: apply_fun (apply_fun F i) x ∈ U.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun (apply_fun F i) x0 ∈ U) x HxPre).
We prove the intermediate claim HFmapx: apply_fun Fmap x = graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x).
rewrite the current goal using HFmapDef (from left to right).
rewrite the current goal using HdiagDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)) x HxX).
We prove the intermediate claim HcoordEq: apply_fun (apply_fun Fmap x) i = apply_fun (apply_fun F i) x.
rewrite the current goal using HFmapx (from left to right).
rewrite the current goal using (apply_fun_graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x) i HiJ) (from left to right).
Use reflexivity.
We prove the intermediate claim HcoordU: apply_fun (apply_fun Fmap x) i ∈ U.
rewrite the current goal using HcoordEq (from left to right).
An exact proof term for the current goal is HfiU.
We prove the intermediate claim Hpred: i ∈ J ∧ U ∈ space_family_topology Xi i ∧ apply_fun (apply_fun Fmap x) i ∈ U.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HiJ.
An exact proof term for the current goal is HUtop.
An exact proof term for the current goal is HcoordU.
We prove the intermediate claim HfxCyl: apply_fun Fmap x ∈ product_cylinder J Xi i U.
An exact proof term for the current goal is (SepI (product_space J Xi) (λf0 : set ⇒ i ∈ J ∧ U ∈ space_family_topology Xi i ∧ apply_fun f0 i ∈ U) (apply_fun Fmap x) (Hfun x HxX) Hpred).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun Fmap x0 ∈ product_cylinder J Xi i U) x HxX HfxCyl).
rewrite the current goal using HpreEq (from left to right).
An exact proof term for the current goal is (continuous_map_preimage X Tx R R_standard_topology (apply_fun F i) Hconti U HUstd).
We prove the intermediate claim HlocFmap: ∀x U : set, x ∈ X → U ∈ Tx → x ∈ U → ∃V : set, V ∈ Ty ∧ apply_fun Fmap x ∈ V ∧ preimage_of X Fmap V ⊆ U.
Let x be given.
Let U be given.
Assume HxX: x ∈ X.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We prove the intermediate claim HsepCore: ((topology_on X Tx ∧ total_function_on F J (function_space X R)) ∧ (∀j0 : set, j0 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j0))).
An exact proof term for the current goal is (andEL (((topology_on X Tx ∧ total_function_on F J (function_space X R)) ∧ (∀j0 : set, j0 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j0)))) (∀x0 : set, x0 ∈ X → ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → ∃j0 : set, j0 ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j0) x0) ∧ ∀x1 : set, x1 ∈ X ∖ U0 → apply_fun (apply_fun F j0) x1 = 0) Hsep).
We prove the intermediate claim Hneigh: ∀x0 : set, x0 ∈ X → ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → ∃j0 : set, j0 ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j0) x0) ∧ ∀x1 : set, x1 ∈ X ∖ U0 → apply_fun (apply_fun F j0) x1 = 0.
An exact proof term for the current goal is (andER (((topology_on X Tx ∧ total_function_on F J (function_space X R)) ∧ (∀j0 : set, j0 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j0)))) (∀x0 : set, x0 ∈ X → ∀U0 : set, U0 ∈ Tx → x0 ∈ U0 → ∃j0 : set, j0 ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j0) x0) ∧ ∀x1 : set, x1 ∈ X ∖ U0 → apply_fun (apply_fun F j0) x1 = 0) Hsep).
We prove the intermediate claim Hexj: ∃j0 : set, j0 ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j0) x) ∧ ∀x1 : set, x1 ∈ X ∖ U → apply_fun (apply_fun F j0) x1 = 0.
An exact proof term for the current goal is (Hneigh x HxX U HU HxU).
Apply Hexj to the current goal.
Let j be given.
Assume Hjpack.
We prove the intermediate claim Hj12: j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x).
An exact proof term for the current goal is (andEL (j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x)) (∀x1 : set, x1 ∈ X ∖ U → apply_fun (apply_fun F j) x1 = 0) Hjpack).
We prove the intermediate claim HjJ: j ∈ J.
An exact proof term for the current goal is (andEL (j ∈ J) (Rlt 0 (apply_fun (apply_fun F j) x)) Hj12).
We prove the intermediate claim Hjpos: Rlt 0 (apply_fun (apply_fun F j) x).
An exact proof term for the current goal is (andER (j ∈ J) (Rlt 0 (apply_fun (apply_fun F j) x)) Hj12).
We prove the intermediate claim Hjzero: ∀x1 : set, x1 ∈ X ∖ U → apply_fun (apply_fun F j) x1 = 0.
An exact proof term for the current goal is (andER (j ∈ J ∧ Rlt 0 (apply_fun (apply_fun F j) x)) (∀x1 : set, x1 ∈ X ∖ U → apply_fun (apply_fun F j) x1 = 0) Hjpack).
Set V to be the term product_cylinder J Xi j (open_ray_upper R 0).
We use V to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HTyDef: Ty = product_topology_full J Xi.
Use reflexivity.
rewrite the current goal using HTyDef (from left to right).
We prove the intermediate claim HprodDef: product_topology_full J Xi = generated_topology_from_subbasis (product_space J Xi) (product_subbasis_full J Xi).
Use reflexivity.
rewrite the current goal using HprodDef (from left to right).
We prove the intermediate claim HJne: J ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty J j HjJ).
We prove the intermediate claim HcompTop: ∀i : set, i ∈ J → topology_on (space_family_set Xi i) (space_family_topology Xi i).
Let i be given.
Assume HiJ: i ∈ J.
We prove the intermediate claim Hset: space_family_set Xi i = R.
An exact proof term for the current goal is (space_family_set_const_space_family J R R_standard_topology i HiJ).
We prove the intermediate claim Htop: space_family_topology Xi i = R_standard_topology.
An exact proof term for the current goal is (space_family_topology_const_space_family J R R_standard_topology i HiJ).
rewrite the current goal using Hset (from left to right).
rewrite the current goal using Htop (from left to right).
An exact proof term for the current goal is R_standard_topology_is_topology.
We prove the intermediate claim HSsub: subbasis_on (product_space J Xi) (product_subbasis_full J Xi).
An exact proof term for the current goal is (product_subbasis_full_subbasis_on J Xi HJne HcompTop).
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim HopenRay: open_ray_upper R 0 ∈ R_standard_topology.
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: open_ray_upper R 0 ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis R 0 H0R).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_upper R 0) HsRay).
We prove the intermediate claim Htopj: space_family_topology Xi j = R_standard_topology.
An exact proof term for the current goal is (space_family_topology_const_space_family J R R_standard_topology j HjJ).
We prove the intermediate claim HUtop: open_ray_upper R 0 ∈ space_family_topology Xi j.
rewrite the current goal using Htopj (from left to right).
An exact proof term for the current goal is HopenRay.
We prove the intermediate claim HVsub: V ∈ product_subbasis_full J Xi.
Set Fam to be the term (λi0 : set ⇒ {product_cylinder J Xi i0 U0|U0 ∈ space_family_topology Xi i0}).
We prove the intermediate claim HVfam: V ∈ Fam j.
An exact proof term for the current goal is (ReplI (space_family_topology Xi j) (λU0 : set ⇒ product_cylinder J Xi j U0) (open_ray_upper R 0) HUtop).
An exact proof term for the current goal is (famunionI J Fam j V HjJ HVfam).
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis (product_space J Xi) (product_subbasis_full J Xi) V HSsub HVsub).
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
We prove the intermediate claim HdiagDef: diagonal_map X F J = graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
We prove the intermediate claim Hfx: apply_fun Fmap x = graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x).
rewrite the current goal using HFmapDef (from left to right).
rewrite the current goal using HdiagDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)) x HxX).
We prove the intermediate claim Hval: apply_fun (apply_fun Fmap x) j ∈ open_ray_upper R 0.
rewrite the current goal using Hfx (from left to right).
rewrite the current goal using (apply_fun_graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x) j HjJ) (from left to right).
We prove the intermediate claim HxjR: apply_fun (apply_fun F j) x ∈ R.
We prove the intermediate claim HtopTot: topology_on X Tx ∧ total_function_on F J (function_space X R).
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ total_function_on F J (function_space X R)) (∀j0 : set, j0 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j0)) HsepCore).
We prove the intermediate claim Htot: total_function_on F J (function_space X R).
An exact proof term for the current goal is (andER (topology_on X Tx) (total_function_on F J (function_space X R)) HtopTot).
We prove the intermediate claim HfjFS: apply_fun F j ∈ function_space X R.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y F J (function_space X R) j Htot HjJ).
We prove the intermediate claim HfjFun: function_on (apply_fun F j) X R.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod X R)) (λf0 : set ⇒ function_on f0 X R) (apply_fun F j) HfjFS).
An exact proof term for the current goal is (HfjFun x HxX).
We prove the intermediate claim Hord: order_rel R 0 (apply_fun (apply_fun F j) x).
An exact proof term for the current goal is (Rlt_implies_order_rel_R 0 (apply_fun (apply_fun F j) x) Hjpos).
An exact proof term for the current goal is (SepI R (λt : set ⇒ order_rel R 0 t) (apply_fun (apply_fun F j) x) HxjR Hord).
We prove the intermediate claim HVdef: V = {f0 ∈ product_space J Xi|j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j ∧ apply_fun f0 j ∈ open_ray_upper R 0}.
Use reflexivity.
rewrite the current goal using HVdef (from left to right).
We prove the intermediate claim Htot: total_function_on F J (function_space X R).
We prove the intermediate claim HtopTot: topology_on X Tx ∧ total_function_on F J (function_space X R).
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ total_function_on F J (function_space X R)) (∀j0 : set, j0 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j0)) HsepCore).
An exact proof term for the current goal is (andER (topology_on X Tx) (total_function_on F J (function_space X R)) HtopTot).
We prove the intermediate claim HfunF: function_on Fmap X (power_real J).
rewrite the current goal using HFmapDef (from left to right).
An exact proof term for the current goal is (diagonal_map_function_on_power_real X F J Htot).
We prove the intermediate claim HpR: power_real J = product_space J Xi.
Use reflexivity.
We prove the intermediate claim HfxProd: apply_fun Fmap x ∈ product_space J Xi.
rewrite the current goal using HpR (from right to left).
An exact proof term for the current goal is (HfunF x HxX).
Apply (SepI (product_space J Xi) (λf0 : set ⇒ j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j ∧ apply_fun f0 j ∈ open_ray_upper R 0) (apply_fun Fmap x) HfxProd) 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 HjJ.
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim HopenRay: open_ray_upper R 0 ∈ R_standard_topology.
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: open_ray_upper R 0 ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis R 0 H0R).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_upper R 0) HsRay).
We prove the intermediate claim Htopj: space_family_topology Xi j = R_standard_topology.
An exact proof term for the current goal is (space_family_topology_const_space_family J R R_standard_topology j HjJ).
rewrite the current goal using Htopj (from left to right).
An exact proof term for the current goal is HopenRay.
We prove the intermediate claim Hcoord: apply_fun (apply_fun Fmap x) j ∈ open_ray_upper R 0.
An exact proof term for the current goal is Hval.
An exact proof term for the current goal is Hcoord.
Let z be given.
Assume HzPre: z ∈ preimage_of X Fmap V.
We will prove z ∈ U.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun Fmap x0 ∈ V) z HzPre).
We prove the intermediate claim HzV: apply_fun Fmap z ∈ V.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun Fmap x0 ∈ V) z HzPre).
We prove the intermediate claim HVdef: V = {f0 ∈ product_space J Xi|j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j ∧ apply_fun f0 j ∈ open_ray_upper R 0}.
Use reflexivity.
We prove the intermediate claim HzV2: apply_fun Fmap z ∈ {f0 ∈ product_space J Xi|j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j ∧ apply_fun f0 j ∈ open_ray_upper R 0}.
rewrite the current goal using HVdef (from right to left).
An exact proof term for the current goal is HzV.
We prove the intermediate claim Hcore: j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j ∧ apply_fun (apply_fun Fmap z) j ∈ open_ray_upper R 0.
An exact proof term for the current goal is (SepE2 (product_space J Xi) (λf0 : set ⇒ j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j ∧ apply_fun f0 j ∈ open_ray_upper R 0) (apply_fun Fmap z) HzV2).
We prove the intermediate claim Hzcoord: apply_fun (apply_fun Fmap z) j ∈ open_ray_upper R 0.
We prove the intermediate claim H12: j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j.
An exact proof term for the current goal is (andEL (j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j) (apply_fun (apply_fun Fmap z) j ∈ open_ray_upper R 0) Hcore).
An exact proof term for the current goal is (andER (j ∈ J ∧ open_ray_upper R 0 ∈ space_family_topology Xi j) (apply_fun (apply_fun Fmap z) j ∈ open_ray_upper R 0) Hcore).
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
We prove the intermediate claim HdiagDef: diagonal_map X F J = graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
We prove the intermediate claim HFmapz: apply_fun Fmap z = graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) z).
rewrite the current goal using HFmapDef (from left to right).
rewrite the current goal using HdiagDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)) z HzX).
We prove the intermediate claim Hzcoord2: apply_fun (apply_fun F j) z ∈ open_ray_upper R 0.
We prove the intermediate claim HcoordEq: apply_fun (apply_fun Fmap z) j = apply_fun (apply_fun F j) z.
rewrite the current goal using HFmapz (from left to right).
rewrite the current goal using (apply_fun_graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) z) j HjJ) (from left to right).
Use reflexivity.
rewrite the current goal using HcoordEq (from right to left).
An exact proof term for the current goal is Hzcoord.
We prove the intermediate claim HzR: apply_fun (apply_fun F j) z ∈ R.
We prove the intermediate claim HtopTot: topology_on X Tx ∧ total_function_on F J (function_space X R).
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ total_function_on F J (function_space X R)) (∀j0 : set, j0 ∈ J → continuous_map X Tx R R_standard_topology (apply_fun F j0)) HsepCore).
We prove the intermediate claim Htot: total_function_on F J (function_space X R).
An exact proof term for the current goal is (andER (topology_on X Tx) (total_function_on F J (function_space X R)) HtopTot).
We prove the intermediate claim HfjFS: apply_fun F j ∈ function_space X R.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y F J (function_space X R) j Htot HjJ).
We prove the intermediate claim HfjFun: function_on (apply_fun F j) X R.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod X R)) (λf0 : set ⇒ function_on f0 X R) (apply_fun F j) HfjFS).
An exact proof term for the current goal is (HfjFun z HzX).
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
We prove the intermediate claim Hzord: order_rel R 0 (apply_fun (apply_fun F j) z).
An exact proof term for the current goal is (SepE2 R (λt : set ⇒ order_rel R 0 t) (apply_fun (apply_fun F j) z) Hzcoord2).
We prove the intermediate claim Hzpos: Rlt 0 (apply_fun (apply_fun F j) z).
An exact proof term for the current goal is (order_rel_R_implies_Rlt 0 (apply_fun (apply_fun F j) z) Hzord).
Apply (xm (z ∈ U)) to the current goal.
Assume HzU: z ∈ U.
An exact proof term for the current goal is HzU.
Assume HznotU: z ∉ U.
We prove the intermediate claim HzOut: z ∈ X ∖ U.
Apply setminusI to the current goal.
An exact proof term for the current goal is HzX.
An exact proof term for the current goal is HznotU.
We prove the intermediate claim Hz0: apply_fun (apply_fun F j) z = 0.
An exact proof term for the current goal is (Hjzero z HzOut).
We prove the intermediate claim Hbad: False.
We prove the intermediate claim Hzpos0: Rlt 0 0.
rewrite the current goal using Hz0 (from right to left) at position 2.
An exact proof term for the current goal is Hzpos.
An exact proof term for the current goal is ((not_Rlt_refl 0 H0R) Hzpos0).
An exact proof term for the current goal is (FalseE Hbad (z ∈ U)).
We prove the intermediate claim HinjFmap: ∀x y : set, x ∈ X → y ∈ X → apply_fun Fmap x = apply_fun Fmap y → x = y.
Let x and y be given.
Assume HxX: x ∈ X.
Assume HyX: y ∈ X.
Assume Heq: apply_fun Fmap x = apply_fun Fmap y.
Apply (xm (x = y)) to the current goal.
Assume Hxy: x = y.
An exact proof term for the current goal is Hxy.
Assume Hxyne: x ≠ y.
We prove the intermediate claim Hexj: ∃j : set, j ∈ J ∧ apply_fun (apply_fun F j) x ≠ apply_fun (apply_fun F j) y.
An exact proof term for the current goal is (separating_family_of_functions_separates_points X Tx F J x y HTx Hclosed Hsep HxX HyX Hxyne).
Apply Hexj to the current goal.
Let j be given.
Assume Hjpair.
We prove the intermediate claim HjJ: j ∈ J.
An exact proof term for the current goal is (andEL (j ∈ J) (apply_fun (apply_fun F j) x ≠ apply_fun (apply_fun F j) y) Hjpair).
We prove the intermediate claim Hneq: apply_fun (apply_fun F j) x ≠ apply_fun (apply_fun F j) y.
An exact proof term for the current goal is (andER (j ∈ J) (apply_fun (apply_fun F j) x ≠ apply_fun (apply_fun F j) y) Hjpair).
We prove the intermediate claim HFmapDef: Fmap = diagonal_map X F J.
Use reflexivity.
We prove the intermediate claim HdiagDef: diagonal_map X F J = graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)).
Use reflexivity.
We prove the intermediate claim HFmapx: apply_fun Fmap x = graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x).
rewrite the current goal using HFmapDef (from left to right).
rewrite the current goal using HdiagDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)) x HxX).
We prove the intermediate claim HFmapy: apply_fun Fmap y = graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) y).
rewrite the current goal using HFmapDef (from left to right).
rewrite the current goal using HdiagDef (from left to right).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x0)) y HyX).
We prove the intermediate claim HgraphEq: graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x) = graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) y).
rewrite the current goal using HFmapx (from right to left) at position 1.
rewrite the current goal using HFmapy (from right to left) at position 1.
An exact proof term for the current goal is Heq.
We prove the intermediate claim Heqj: apply_fun (apply_fun F j) x = apply_fun (apply_fun F j) y.
We prove the intermediate claim HapplyEq: apply_fun (graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x)) j = apply_fun (graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) y)) j.
rewrite the current goal using HgraphEq (from left to right).
Use reflexivity.
We prove the intermediate claim Hleft: apply_fun (graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x)) j = apply_fun (apply_fun F j) x.
rewrite the current goal using (apply_fun_graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) x) j HjJ) (from left to right).
Use reflexivity.
We prove the intermediate claim Hright: apply_fun (graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) y)) j = apply_fun (apply_fun F j) y.
rewrite the current goal using (apply_fun_graph J (λj0 : set ⇒ apply_fun (apply_fun F j0) y) j HjJ) (from left to right).
Use reflexivity.
rewrite the current goal using Hleft (from right to left) at position 1.
rewrite the current goal using Hright (from right to left) at position 1.
An exact proof term for the current goal is HapplyEq.
We prove the intermediate claim Hbad: False.
An exact proof term for the current goal is (Hneq Heqj).
An exact proof term for the current goal is (FalseE Hbad (x = y)).
An exact proof term for the current goal is (embedding_of_from_local_refinement X Tx (power_real J) Ty Fmap HcontFmap HlocFmap HinjFmap).
∎