Theorems · Theorem · general topology

continuous_quot_lift

∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {r : X → X → Prop} {f : X → Y}
  (hr : ∀ (a b : X), r a b → f a = f b), Continuous f → Continuous (Quot.lift f hr)

Defined in

Mathlib.Topology.Constructions

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace