Theorems · Definition · general topology

IsClosedMap

{X : Type u} → {Y : Type v} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop

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.

Defined in

Mathlib.Topology.Defs.Basic

Cited by

138 results in Mathlib

Foundations

Depth 5 from the axioms, rests on 14 definitions · uses no axioms

Assumes

TopologicalSpaceTopologicalSpace