IsClosedMap — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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