Theorems · Definition · general topology

SeparationQuotient.lift

{X : Type u_1} →
  {α : Type u_4} →
    [inst : TopologicalSpace X] → (f : X → α) → (∀ (x y : X), Inseparable x y → f x = f y) → SeparationQuotient X → α

Lift a map f : X → α such that Inseparable x y → f x = f y to a map SeparationQuotient X → α.

Defined in

Mathlib.Topology.Inseparable

Cited by

12 results in Mathlib

Foundations

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

Assumes

TopologicalSpace