Let X, Tx, Y and Ty be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
We will prove ∃Tprod : set, topology_on (setprod X Y) Tprod ∧ continuous_map (setprod X Y) Tprod X Tx (projection_map1 X Y) ∧ continuous_map (setprod X Y) Tprod Y Ty (projection_map2 X Y).
We use (product_topology X Tx Y Ty) to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (product_topology_is_topology X Tx Y Ty HTx HTy).
An exact proof term for the current goal is (andEL (continuous_map (setprod X Y) (product_topology X Tx Y Ty) X Tx (projection_map1 X Y)) (continuous_map (setprod X Y) (product_topology X Tx Y Ty) Y Ty (projection_map2 X Y)) (projections_are_continuous X Tx Y Ty HTx HTy)).
An exact proof term for the current goal is (andER (continuous_map (setprod X Y) (product_topology X Tx Y Ty) X Tx (projection_map1 X Y)) (continuous_map (setprod X Y) (product_topology X Tx Y Ty) Y Ty (projection_map2 X Y)) (projections_are_continuous X Tx Y Ty HTx HTy)).
∎