Let X, Tx, Y, Ty and Tprod be given.
Assume HTx: topology_on X Tx.
Assume HTy: topology_on Y Ty.
Assume HTprod: topology_on (setprod X Y) Tprod.
Assume Hc1: continuous_map (setprod X Y) Tprod X Tx (projection_map1 X Y).
Assume Hc2: continuous_map (setprod X Y) Tprod Y Ty (projection_map2 X Y).
We will prove coarser_than (product_topology X Tx Y Ty) Tprod.
We will prove product_topology X Tx Y Ty ⊆ Tprod.
Set B to be the term product_subbasis X Tx Y Ty.
We prove the intermediate claim HBasis: basis_on (setprod X Y) B.
An exact proof term for the current goal is (product_subbasis_is_basis X Tx Y Ty HTx HTy).
We prove the intermediate claim Hc1_pre: ∀U : set, U ∈ Tx → preimage_of (setprod X Y) (projection_map1 X Y) U ∈ Tprod.
An exact proof term for the current goal is (andER ((topology_on (setprod X Y) Tprod ∧ topology_on X Tx) ∧ function_on (projection_map1 X Y) (setprod X Y) X) (∀U : set, U ∈ Tx → preimage_of (setprod X Y) (projection_map1 X Y) U ∈ Tprod) Hc1).
We prove the intermediate claim Hc2_pre: ∀V : set, V ∈ Ty → preimage_of (setprod X Y) (projection_map2 X Y) V ∈ Tprod.
An exact proof term for the current goal is (andER ((topology_on (setprod X Y) Tprod ∧ topology_on Y Ty) ∧ function_on (projection_map2 X Y) (setprod X Y) Y) (∀V : set, V ∈ Ty → preimage_of (setprod X Y) (projection_map2 X Y) V ∈ Tprod) Hc2).
We prove the intermediate claim HallB: ∀b ∈ B, b ∈ Tprod.
Let b be given.
Assume HbB: b ∈ B.
Apply (famunionE Tx (λU0 : set ⇒ {rectangle_set U0 V0|V0 ∈ Ty}) b HbB) to the current goal.
Let U be given.
Assume HUconj: U ∈ Tx ∧ b ∈ {rectangle_set U V0|V0 ∈ Ty}.
We prove the intermediate claim HUinTx: U ∈ Tx.
An exact proof term for the current goal is (andEL (U ∈ Tx) (b ∈ {rectangle_set U V0|V0 ∈ Ty}) HUconj).
We prove the intermediate claim HbRepl: b ∈ {rectangle_set U V0|V0 ∈ Ty}.
An exact proof term for the current goal is (andER (U ∈ Tx) (b ∈ {rectangle_set U V0|V0 ∈ Ty}) HUconj).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HUinTx).
We prove the intermediate claim HexV: ∃V ∈ Ty, b = rectangle_set U V.
An exact proof term for the current goal is (ReplE Ty (λV0 : set ⇒ rectangle_set U V0) b HbRepl).
Apply HexV to the current goal.
Let V be given.
Assume HVconj: V ∈ Ty ∧ b = rectangle_set U V.
We prove the intermediate claim HVinTy: V ∈ Ty.
An exact proof term for the current goal is (andEL (V ∈ Ty) (b = rectangle_set U V) HVconj).
We prove the intermediate claim Hbeq: b = rectangle_set U V.
An exact proof term for the current goal is (andER (V ∈ Ty) (b = rectangle_set U V) HVconj).
We prove the intermediate claim HVsubY: V ⊆ Y.
An exact proof term for the current goal is (topology_elem_subset Y Ty V HTy HVinTy).
We prove the intermediate claim Hpre1eq: preimage_of (setprod X Y) (projection_map1 X Y) U = rectangle_set U Y.
An exact proof term for the current goal is (preimage_projection1_rectangle X Y U HUsubX).
We prove the intermediate claim Hpre2eq: preimage_of (setprod X Y) (projection_map2 X Y) V = rectangle_set X V.
An exact proof term for the current goal is (preimage_projection2_rectangle X Y V HVsubY).
We prove the intermediate claim Hstrip1: rectangle_set U Y ∈ Tprod.
rewrite the current goal using Hpre1eq (from right to left).
An exact proof term for the current goal is (Hc1_pre U HUinTx).
We prove the intermediate claim Hstrip2: rectangle_set X V ∈ Tprod.
rewrite the current goal using Hpre2eq (from right to left).
An exact proof term for the current goal is (Hc2_pre V HVinTy).
We prove the intermediate claim HrectEq: rectangle_set U V = (rectangle_set U Y) ∩ (rectangle_set X V).
An exact proof term for the current goal is (rectangle_set_as_intersection X Y U V HUsubX HVsubY).
We prove the intermediate claim Hcap: (rectangle_set U Y) ∩ (rectangle_set X V) ∈ Tprod.
An exact proof term for the current goal is (topology_binintersect_closed (setprod X Y) Tprod (rectangle_set U Y) (rectangle_set X V) HTprod Hstrip1 Hstrip2).
rewrite the current goal using Hbeq (from left to right).
rewrite the current goal using HrectEq (from left to right).
An exact proof term for the current goal is Hcap.
We prove the intermediate claim Hfiner: finer_than Tprod (generated_topology (setprod X Y) B).
An exact proof term for the current goal is (generated_topology_finer_weak (setprod X Y) B Tprod HTprod HallB).
An exact proof term for the current goal is Hfiner.
∎