Theorems · Theorem · general topology

continuous_quot_map

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

Defined in

Mathlib.Topology.Constructions

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace