Theorems · Definition · general topology

Topology.IsStrictMap

{X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop

A map is a strict map in the sense of Bourbaki if the natural map to its image is a quotient map.

Defined in

Mathlib.Topology.Maps.Strict.Basic

Cited by

45 results in Mathlib

Foundations

Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace