feat: open maps from I × X, I discrete (#7809)

Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Mathlib/Topology/ContinuousOn.lean

@@ -609,6 +609,16 @@ theorem continuous_prod_of_discrete_right [DiscreteTopology β] {f : α × β 
     Continuous f ↔ ∀ b, Continuous (f ⟨·, b⟩) := by
   simp_rw [continuous_iff_continuousOn_univ]; exact continuousOn_prod_of_discrete_right
 
+theorem isOpenMap_prod_of_discrete_left [DiscreteTopology α] {f : α × β → γ} :
+    IsOpenMap f ↔ ∀ a, IsOpenMap (f ⟨a, ·⟩) := by
+  simp_rw [isOpenMap_iff_nhds_le, Prod.forall, nhds_prod_eq, nhds_discrete, pure_prod, map_map]
+  rfl
+
+theorem isOpenMap_prod_of_discrete_right [DiscreteTopology β] {f : α × β → γ} :
+    IsOpenMap f ↔ ∀ b, IsOpenMap (f ⟨·, b⟩) := by
+  simp_rw [isOpenMap_iff_nhds_le, Prod.forall, forall_swap (α := α) (β := β), nhds_prod_eq,
+    nhds_discrete, prod_pure, map_map]; rfl
+
 theorem continuousWithinAt_pi {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
     {f : α → ∀ i, π i} {s : Set α} {x : α} :
     ContinuousWithinAt f s x ↔ ∀ i, ContinuousWithinAt (fun y => f y i) s x :=