Theorems · Inductive type · general topology

Topology.IsQuotientMap

{X : Type u_3} → {Y : Type u_4} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop

A function between topological spaces is a quotient map if it is surjective, and for all s : Set Y, s is open iff its preimage is an open set.

Defined in

Mathlib.Topology.Defs.Induced

Cited by

124 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

TopologicalSpaceTopologicalSpace