isOpenMap_prod_of_discrete_left — Mathlib

English

If α is discrete, IsOpenMap f is equivalent to IsOpenMap of the left fiber maps a ↦ f(a,·) for each a.

Русский

Если α дискретно, IsOpenMap f эквивалентно IsOpenMap каждому отображению a ↦ f(a,·).

LaTeX

$$$$\text{IsOpenMap } f \iff \forall a, \text{IsOpenMap }\bigl( x \mapsto f(a,x) \bigr). $$$$

Lean4

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

Похожие утверждения