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 : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (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 : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
⊢ Continuous g
let Gf : C(X₀, C(Y, Z)) := ContinuousMap.curry ⟨_, hg⟩
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 : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
h : ∀ (x : X), Continuous fun y => g (x, y)
⊢ 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 : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
⊢ Continuous g
have h : ∀ x : X, Continuous fun y => g (x, y) := by
  intro x
  obtain ⟨x₀, rfl⟩ := hf.surjective x
  exact (Gf x₀).continuous
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 : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => mk fun y => g (x, y)
⊢ 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 : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
h : ∀ (x : X), Continuous fun y => g (x, y)
⊢ Continuous g
let G : X → C(Y, Z) := fun x => ⟨_, h x⟩
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 : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => mk fun y => g (x, y)
this : Continuous G
⊢ 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 : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => mk fun y => g (x, y)
⊢ Continuous g
have : Continuous G := by
  rw [hf.continuous_iff]
  exact Gf.continuous
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 : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => mk fun y => g (x, y)
this : Continuous G
⊢ Continuous g
exact ContinuousMap.continuous_uncurry_of_continuous ⟨G, this⟩
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 : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
x : X
⊢ Continuous fun y => g (x, y)
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 : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
⊢ ∀ (x : X), Continuous fun y => g (x, y)
intro x
case intro
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 : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
x₀ : X₀
⊢ Continuous fun y => g (f x₀, y)
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 : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
x : X
⊢ Continuous fun y => g (x, y)
obtain ⟨x₀, rfl⟩ := hf.surjective x
no goals
case intro
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 : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
x₀ : X₀
⊢ Continuous fun y => g (f x₀, y)
exact (Gf x₀).continuous
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 : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => mk fun y => g (x, y)
⊢ Continuous (G ∘ f)
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 : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => mk fun y => g (x, y)
⊢ Continuous G
rw [hf.continuous_iff]
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 : X × Y → Z
hg : Continuous fun p => g (f p.fst, p.snd)
Gf : C(X₀, C(Y, Z)) := curry (mk fun p => g (f p.fst, p.snd))
h : ∀ (x : X), Continuous fun y => g (x, y)
G : X → C(Y, Z) := fun x => mk fun y => g (x, y)
⊢ Continuous (G ∘ f)
exact Gf.continuous