Theorems · Definition · general topology

GeneralizingMap

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

A map f between topological spaces is generalizing if generalizations lifts along f, i.e. for each y ⤳ f x' there is some x ⤳ x' whose image is y.

Defined in

Mathlib.Topology.Inseparable

Cited by

16 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace