Theorems · Theorem · general topology

Topology.IsQuotientMap.continuous_lift_prod_left

∀ {X₀ : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X₀]
  [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace Y] [inst_3 : TopologicalSpace Z] [LocallyCompactSpace Y]
  {f : X₀ → X}, Topology.IsQuotientMap f → ∀ {g : X × Y → Z}, (Continuous fun p => g (f p.1, p.2)) → Continuous g

Defined in

Mathlib.Topology.CompactOpen

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceLocallyCompactSpace