isOpenMap_iff — Mathlib

English

A map f is an open map if and only if the image of every basis element is open.

Русский

Отображение f открыто тогда и только тогда, когда образ каждого базисного элемента является открытым.

LaTeX

$$$\text{IsOpenMap}(f) \iff \forall s \in B,\; f''s\ \text{ is open}.$$$

Lean4

theorem isOpenMap_iff {β} [TopologicalSpace β] {B : Set (Set α)} (hB : IsTopologicalBasis B) {f : α → β} :
    IsOpenMap f ↔ ∀ s ∈ B, IsOpen (f '' s) :=
  by
  refine ⟨fun H o ho => H _ (hB.isOpen ho), fun hf o ho => ?_⟩
  rw [hB.open_eq_sUnion' ho, sUnion_eq_iUnion, image_iUnion]
  exact isOpen_iUnion fun s => hf s s.2.1

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