theorem TopologicalSpace.prod_mono {α : Type u_1} {β : Type u_2} {σ₁ σ₂ : TopologicalSpace α} {τ₁ τ₂ : TopologicalSpace β} (hσ : σ₁ ≤ σ₂) (hτ : τ₁ ≤ τ₂) : instTopologicalSpaceProd ≤ instTopologicalSpaceProd