isOpenMap_prod_of_discrete_right — Mathlib

English

If β is discrete, IsOpenMap f is equivalent to IsOpenMap of the right fiber maps x ↦ f(·,x) for each x.

Русский

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

LaTeX

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

Lean4

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

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