IsOpenMap — Mathlib

English

Let f: X → Y be a map between topological spaces. f is an open map if the image of every open subset of X is open in Y.

Русский

Пусть f: X → Y — отображение между топологическими пространствами. Оно является открытым отображением, если образ каждого открытого множества U ⊆ X является открытым во Y.

LaTeX

$$$\\forall U : Set X, IsOpen U \\to IsOpen (f '' U)$$$

Lean4

/-- A map `f : X → Y` is said to be an *open map*,
if the image of any open `U : Set X` is open in `Y`. -/
def IsOpenMap (f : X → Y) : Prop :=
  ∀ U : Set X, IsOpen U → IsOpen (f '' U)

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