X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : Y × X → Z
hg : Continuous fun p => g (p.fst, f p.snd)
this : Continuous fun p => g ((Prod.swap p).fst, f (Prod.swap p).snd)
⊢ Continuous g
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : Y × X → Z
hg : Continuous fun p => g (p.fst, f p.snd)
⊢ Continuous g
have : Continuous fun p : X₀ × Y => g ((Prod.swap p).1, f (Prod.swap p).2) :=
  hg.comp continuous_swap
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : Y × X → Z
hg : Continuous fun p => g (p.fst, f p.snd)
this✝ : Continuous fun p => g ((Prod.swap p).fst, f (Prod.swap p).snd)
this : Continuous fun p => (g ∘ Prod.swap) (f p.fst, p.snd)
⊢ Continuous g
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : Y × X → Z
hg : Continuous fun p => g (p.fst, f p.snd)
this : Continuous fun p => g ((Prod.swap p).fst, f (Prod.swap p).snd)
⊢ Continuous g
have : Continuous fun p : X₀ × Y => (g ∘ Prod.swap) (f p.1, p.2) := this
no goals
X₀ : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X₀
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace Y
f : X₀ → X
hf : QuotientMap f
g : Y × X → Z
hg : Continuous fun p => g (p.fst, f p.snd)
this✝ : Continuous fun p => g ((Prod.swap p).fst, f (Prod.swap p).snd)
this : Continuous fun p => (g ∘ Prod.swap) (f p.fst, p.snd)
⊢ Continuous g
exact (hf.continuous_lift_prod_left this).comp continuous_swap