[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
x✝ : Set C(α, β)
⊢ x✝ ∈ {m | ∃ s x u x, m = CompactOpen.gen s u} ↔ x✝ ∈ image2 CompactOpen.gen {s | IsCompact s} {t | IsOpen t}
[PROOFSTEP]
simp [eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ CompactOpen.gen s u ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
[PROOFSTEP]
dsimp [mem_setOf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ ∃ s_1 x u_1 x, CompactOpen.gen s u = CompactOpen.gen s_1 u_1
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
s : Set α
u : Set γ
⊢ comp g ⁻¹' CompactOpen.gen s u = CompactOpen.gen s (↑g ⁻¹' u)
[PROOFSTEP]
ext ⟨f, _⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
s : Set α
u : Set γ
f : α → β
continuous_toFun✝ : Continuous f
⊢ mk f ∈ comp g ⁻¹' CompactOpen.gen s u ↔ mk f ∈ CompactOpen.gen s (↑g ⁻¹' u)
[PROOFSTEP]
change g ∘ f '' s ⊆ u ↔ f '' s ⊆ g ⁻¹' u
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
s : Set α
u : Set γ
f : α → β
continuous_toFun✝ : Continuous f
⊢ ↑g ∘ f '' s ⊆ u ↔ f '' s ⊆ ↑g ⁻¹' u
[PROOFSTEP]
rw [image_comp, image_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
m : Set C(α, γ)
x✝ : m ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
s : Set α
hs : IsCompact s
u : Set γ
hu : IsOpen u
hm : m = CompactOpen.gen s u
⊢ IsOpen (comp g ⁻¹' m)
[PROOFSTEP]
rw [hm, preimage_gen g]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
m : Set C(α, γ)
x✝ : m ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
s : Set α
hs : IsCompact s
u : Set γ
hu : IsOpen u
hm : m = CompactOpen.gen s u
⊢ IsOpen (CompactOpen.gen s (↑g ⁻¹' u))
[PROOFSTEP]
exact ContinuousMap.isOpen_gen hs (hu.preimage g.2)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
hg : Inducing ↑g
⊢ compactOpen = TopologicalSpace.induced (comp g) compactOpen
[PROOFSTEP]
simp only [compactOpen_eq, induced_generateFrom_eq, image_image2, preimage_gen, hg.setOf_isOpen, image2_image_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
s : Set α
x✝¹ : IsCompact s
u : Set γ
x✝ : IsOpen u
⊢ (fun g => comp g f) ⁻¹' CompactOpen.gen s u = CompactOpen.gen (↑f '' s) u
[PROOFSTEP]
ext ⟨g, _⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g✝ : C(β, γ)
f : C(α, β)
s : Set α
x✝¹ : IsCompact s
u : Set γ
x✝ : IsOpen u
g : β → γ
continuous_toFun✝ : Continuous g
⊢ mk g ∈ (fun g => comp g f) ⁻¹' CompactOpen.gen s u ↔ mk g ∈ CompactOpen.gen (↑f '' s) u
[PROOFSTEP]
change g ∘ f '' s ⊆ u ↔ g '' (f '' s) ⊆ u
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g✝ : C(β, γ)
f : C(α, β)
s : Set α
x✝¹ : IsCompact s
u : Set γ
x✝ : IsOpen u
g : β → γ
continuous_toFun✝ : Continuous g
⊢ g ∘ ↑f '' s ⊆ u ↔ g '' (↑f '' s) ⊆ u
[PROOFSTEP]
rw [Set.image_comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
m : Set C(α, γ)
x✝ : m ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
s : Set α
hs : IsCompact s
u : Set γ
hu : IsOpen u
hm : m = CompactOpen.gen s u
⊢ IsOpen ((fun g => comp g f) ⁻¹' m)
[PROOFSTEP]
rw [hm, image_gen f hs hu]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
m : Set C(α, γ)
x✝ : m ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
s : Set α
hs : IsCompact s
u : Set γ
hu : IsOpen u
hm : m = CompactOpen.gen s u
⊢ IsOpen (CompactOpen.gen (↑f '' s) u)
[PROOFSTEP]
exact ContinuousMap.isOpen_gen (hs.image f.2) hu
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
⊢ ∀ (s : Set C(α, γ)), s ∈ {m | ∃ s x u x, m = CompactOpen.gen s u} → IsOpen ((fun x => comp x.snd x.fst) ⁻¹' s)
[PROOFSTEP]
rintro M ⟨K, hK, U, hU, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
⊢ IsOpen ((fun x => comp x.snd x.fst) ⁻¹' CompactOpen.gen K U)
[PROOFSTEP]
conv =>
  congr
  rw [CompactOpen.gen, preimage_setOf_eq]
    --congr
  ext; dsimp [setOf]
  rw [image_comp, image_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
| IsOpen ((fun x => comp x.snd x.fst) ⁻¹' CompactOpen.gen K U)
[PROOFSTEP]
  congr
  rw [CompactOpen.gen, preimage_setOf_eq]
    --congr
  ext; dsimp [setOf]
  rw [image_comp, image_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
| IsOpen ((fun x => comp x.snd x.fst) ⁻¹' CompactOpen.gen K U)
[PROOFSTEP]
  congr
  rw [CompactOpen.gen, preimage_setOf_eq]
    --congr
  ext; dsimp [setOf]
  rw [image_comp, image_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
| IsOpen ((fun x => comp x.snd x.fst) ⁻¹' CompactOpen.gen K U)
[PROOFSTEP]
congr
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
| (fun x => comp x.snd x.fst) ⁻¹' CompactOpen.gen K U
[PROOFSTEP]
rw [CompactOpen.gen, preimage_setOf_eq]
  --congr
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
| {a | ↑(comp a.snd a.fst) '' K ⊆ U}
[PROOFSTEP]
ext
[GOAL]
case a.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
x✝ : C(α, β) × C(β, γ)
| setOf (fun a => ↑(comp a.snd a.fst) '' K ⊆ U) x✝
[PROOFSTEP]
dsimp [setOf]
[GOAL]
case a.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
x✝ : C(α, β) × C(β, γ)
| ↑x✝.snd ∘ ↑x✝.fst '' K ⊆ U
[PROOFSTEP]
rw [image_comp, image_subset_iff]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
⊢ IsOpen fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
[PROOFSTEP]
rw [isOpen_iff_forall_mem_open]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
⊢ ∀ (x : C(α, β) × C(β, γ)),
    (x ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) → ∃ t, (t ⊆ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) ∧ IsOpen t ∧ x ∈ t
[PROOFSTEP]
rintro ⟨φ₀, ψ₀⟩ H
[GOAL]
case intro.intro.intro.intro.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
⊢ ∃ t, (t ⊆ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) ∧ IsOpen t ∧ (φ₀, ψ₀) ∈ t
[PROOFSTEP]
obtain ⟨L, hL, hKL, hLU⟩ := exists_compact_between (hK.image φ₀.2) (hU.preimage ψ₀.2) H
[GOAL]
case intro.intro.intro.intro.mk.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
L : Set β
hL : IsCompact L
hKL : φ₀.toFun '' K ⊆ interior L
hLU : L ⊆ ψ₀.toFun ⁻¹' U
⊢ ∃ t, (t ⊆ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) ∧ IsOpen t ∧ (φ₀, ψ₀) ∈ t
[PROOFSTEP]
use{φ : C(α, β) | φ '' K ⊆ interior L} ×ˢ
    {ψ : C(β, γ) | ψ '' L ⊆ U}
      -- porting note: typing hint `: φ '' K ⊆ interior L` wasn't previously required
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
L : Set β
hL : IsCompact L
hKL : φ₀.toFun '' K ⊆ interior L
hLU : L ⊆ ψ₀.toFun ⁻¹' U
⊢ ({φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U} ⊆ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U) ∧
    IsOpen ({φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}) ∧
      (φ₀, ψ₀) ∈ {φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}
[PROOFSTEP]
use fun ⟨φ, ψ⟩ ⟨(hφ : φ '' K ⊆ interior L), hψ⟩ => subset_trans hφ (interior_subset.trans <| image_subset_iff.mp hψ)
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
L : Set β
hL : IsCompact L
hKL : φ₀.toFun '' K ⊆ interior L
hLU : L ⊆ ψ₀.toFun ⁻¹' U
⊢ IsOpen ({φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}) ∧ (φ₀, ψ₀) ∈ {φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}
[PROOFSTEP]
use(ContinuousMap.isOpen_gen hK isOpen_interior).prod (ContinuousMap.isOpen_gen hL hU)
[GOAL]
case right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
inst✝ : LocallyCompactSpace β
K : Set α
hK : IsCompact K
U : Set γ
hU : IsOpen U
φ₀ : C(α, β)
ψ₀ : C(β, γ)
H : (φ₀, ψ₀) ∈ fun x => ↑x.fst '' K ⊆ ↑x.snd ⁻¹' U
L : Set β
hL : IsCompact L
hKL : φ₀.toFun '' K ⊆ interior L
hLU : L ⊆ ψ₀.toFun ⁻¹' U
⊢ (φ₀, ψ₀) ∈ {φ | ↑φ '' K ⊆ interior L} ×ˢ {ψ | ↑ψ '' L ⊆ U}
[PROOFSTEP]
exact mem_prod.mpr ⟨hKL, image_subset_iff.mpr hLU⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : LocallyCompactSpace α
x✝ : C(α, β) × α
n : Set β
f : C(α, β)
x : α
hn : n ∈ 𝓝 (↑(f, x).fst (f, x).snd)
v : Set β
vn : v ⊆ n
vo : IsOpen v
fxv : ↑(f, x).fst (f, x).snd ∈ v
this✝² : v ∈ 𝓝 (↑f x)
s : Set α
hs : s ∈ 𝓝 x
sv : s ⊆ ↑f ⁻¹' v
sc : IsCompact s
u : Set α
us : u ⊆ s
uo : IsOpen u
xu : x ∈ u
w : Set (C(α, β) × α) := CompactOpen.gen s v ×ˢ u
this✝¹ : w ⊆ (fun p => ↑p.fst p.snd) ⁻¹' n
this✝ : IsOpen w
this : (f, x) ∈ w
⊢ w ⊆ (fun p => ↑p.fst p.snd) ⁻¹' n
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : LocallyCompactSpace α
x✝ : C(α, β) × α
n : Set β
f : C(α, β)
x : α
hn : n ∈ 𝓝 (↑(f, x).fst (f, x).snd)
v : Set β
vn : v ⊆ n
vo : IsOpen v
fxv : ↑(f, x).fst (f, x).snd ∈ v
this✝² : v ∈ 𝓝 (↑f x)
s : Set α
hs : s ∈ 𝓝 x
sv : s ⊆ ↑f ⁻¹' v
sc : IsCompact s
u : Set α
us : u ⊆ s
uo : IsOpen u
xu : x ∈ u
w : Set (C(α, β) × α) := CompactOpen.gen s v ×ˢ u
this✝¹ : w ⊆ (fun p => ↑p.fst p.snd) ⁻¹' n
this✝ : IsOpen w
this : (f, x) ∈ w
⊢ IsOpen w
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : LocallyCompactSpace α
x✝ : C(α, β) × α
n : Set β
f : C(α, β)
x : α
hn : n ∈ 𝓝 (↑(f, x).fst (f, x).snd)
v : Set β
vn : v ⊆ n
vo : IsOpen v
fxv : ↑(f, x).fst (f, x).snd ∈ v
this✝² : v ∈ 𝓝 (↑f x)
s : Set α
hs : s ∈ 𝓝 x
sv : s ⊆ ↑f ⁻¹' v
sc : IsCompact s
u : Set α
us : u ⊆ s
uo : IsOpen u
xu : x ∈ u
w : Set (C(α, β) × α) := CompactOpen.gen s v ×ˢ u
this✝¹ : w ⊆ (fun p => ↑p.fst p.snd) ⁻¹' n
this✝ : IsOpen w
this : (f, x) ∈ w
⊢ (f, x) ∈ w
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
a : α
⊢ Continuous fun f => ↑f a
[PROOFSTEP]
refine continuous_def.2 fun U hU ↦ ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
a : α
U : Set ((fun x => β) a)
hU : IsOpen U
⊢ IsOpen ((fun f => ↑f a) ⁻¹' U)
[PROOFSTEP]
convert ContinuousMap.isOpen_gen (isCompact_singleton (a := a)) hU using 1
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
a : α
U : Set ((fun x => β) a)
hU : IsOpen U
⊢ (fun f => ↑f a) ⁻¹' U = CompactOpen.gen {a} U
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
a : α
U : Set ((fun x => β) a)
hU : IsOpen U
x✝ : C(α, β)
⊢ x✝ ∈ (fun f => ↑f a) ⁻¹' U ↔ x✝ ∈ CompactOpen.gen {a} U
[PROOFSTEP]
simp [CompactOpen.gen]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
⊢ compactOpen ≤ TopologicalSpace.induced (restrict s) compactOpen
[PROOFSTEP]
simp only [induced_generateFrom_eq, ContinuousMap.compactOpen]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
⊢ TopologicalSpace.generateFrom {m | ∃ s x u x, m = CompactOpen.gen s u} ≤
    TopologicalSpace.generateFrom (preimage (restrict s) '' {m | ∃ s_1 x u x, m = CompactOpen.gen s_1 u})
[PROOFSTEP]
apply TopologicalSpace.generateFrom_anti
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
⊢ preimage (restrict s) '' {m | ∃ s_1 x u x, m = CompactOpen.gen s_1 u} ⊆ {m | ∃ s x u x, m = CompactOpen.gen s u}
[PROOFSTEP]
rintro b ⟨a, ⟨c, hc, u, hu, rfl⟩, rfl⟩
[GOAL]
case h.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
c : Set ↑s
hc : IsCompact c
u : Set β
hu : IsOpen u
⊢ restrict s ⁻¹' CompactOpen.gen c u ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
[PROOFSTEP]
refine' ⟨(↑) '' c, hc.image continuous_subtype_val, u, hu, _⟩
[GOAL]
case h.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
c : Set ↑s
hc : IsCompact c
u : Set β
hu : IsOpen u
⊢ restrict s ⁻¹' CompactOpen.gen c u = CompactOpen.gen (Subtype.val '' c) u
[PROOFSTEP]
ext f
[GOAL]
case h.intro.intro.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
c : Set ↑s
hc : IsCompact c
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ f ∈ restrict s ⁻¹' CompactOpen.gen c u ↔ f ∈ CompactOpen.gen (Subtype.val '' c) u
[PROOFSTEP]
simp only [CompactOpen.gen, mem_setOf_eq, mem_preimage, ContinuousMap.coe_restrict]
[GOAL]
case h.intro.intro.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
c : Set ↑s
hc : IsCompact c
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ (fun a => (↑f ∘ Subtype.val) a) '' c ⊆ u ↔ (fun a => ↑f a) '' (Subtype.val '' c) ⊆ u
[PROOFSTEP]
rw [image_comp f ((↑) : s → α)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ compactOpen = ⨅ (s : Set α) (_ : IsCompact s), TopologicalSpace.induced (restrict s) compactOpen
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ compactOpen ≤ ⨅ (s : Set α) (_ : IsCompact s), TopologicalSpace.induced (restrict s) compactOpen
[PROOFSTEP]
refine' le_iInf₂ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ ∀ (i : Set α), IsCompact i → compactOpen ≤ TopologicalSpace.induced (restrict i) compactOpen
[PROOFSTEP]
exact fun s _ => compactOpen_le_induced s
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ ⨅ (s : Set α) (_ : IsCompact s), TopologicalSpace.induced (restrict s) compactOpen ≤ compactOpen
[PROOFSTEP]
simp only [← generateFrom_iUnion, induced_generateFrom_eq, ContinuousMap.compactOpen]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ TopologicalSpace.generateFrom
      (⋃ (i : Set α) (_ : IsCompact i), preimage (restrict i) '' {m | ∃ s x u x, m = CompactOpen.gen s u}) ≤
    TopologicalSpace.generateFrom {m | ∃ s x u x, m = CompactOpen.gen s u}
[PROOFSTEP]
apply TopologicalSpace.generateFrom_anti
[GOAL]
case refine'_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ {m | ∃ s x u x, m = CompactOpen.gen s u} ⊆
    ⋃ (i : Set α) (_ : IsCompact i), preimage (restrict i) '' {m | ∃ s x u x, m = CompactOpen.gen s u}
[PROOFSTEP]
rintro _ ⟨s, hs, u, hu, rfl⟩
[GOAL]
case refine'_2.h.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ CompactOpen.gen s u ∈
    ⋃ (i : Set α) (_ : IsCompact i), preimage (restrict i) '' {m | ∃ s x u x, m = CompactOpen.gen s u}
[PROOFSTEP]
rw [mem_iUnion₂]
[GOAL]
case refine'_2.h.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ ∃ i j, CompactOpen.gen s u ∈ preimage (restrict i) '' {m | ∃ s x u x, m = CompactOpen.gen s u}
[PROOFSTEP]
refine' ⟨s, hs, _, ⟨univ, isCompact_iff_isCompact_univ.mp hs, u, hu, rfl⟩, _⟩
[GOAL]
case refine'_2.h.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ restrict s ⁻¹' CompactOpen.gen univ u = CompactOpen.gen s u
[PROOFSTEP]
ext f
[GOAL]
case refine'_2.h.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ f ∈ restrict s ⁻¹' CompactOpen.gen univ u ↔ f ∈ CompactOpen.gen s u
[PROOFSTEP]
simp only [CompactOpen.gen, mem_setOf_eq, mem_preimage, ContinuousMap.coe_restrict]
[GOAL]
case refine'_2.h.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ (fun a => (↑f ∘ Subtype.val) a) '' univ ⊆ u ↔ (fun a => ↑f a) '' s ⊆ u
[PROOFSTEP]
rw [image_comp f ((↑) : s → α)]
[GOAL]
case refine'_2.h.intro.intro.intro.intro.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
f : C(α, β)
⊢ ↑f '' (Subtype.val '' univ) ⊆ u ↔ (fun a => ↑f a) '' s ⊆ u
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
⊢ Continuous fun F => restrict s F
[PROOFSTEP]
rw [continuous_iff_le_induced]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
⊢ compactOpen ≤ TopologicalSpace.induced (fun F => restrict s F) compactOpen
[PROOFSTEP]
exact compactOpen_le_induced s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(α, β)
⊢ 𝓝 f = ⨅ (s : Set α) (_ : IsCompact s), Filter.comap (restrict s) (𝓝 (restrict s f))
[PROOFSTEP]
rw [compactOpen_eq_sInf_induced]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(α, β)
⊢ 𝓝 f = ⨅ (s : Set α) (_ : IsCompact s), Filter.comap (restrict s) (𝓝 (restrict s f))
[PROOFSTEP]
simp [nhds_iInf, nhds_induced]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_4
l : Filter ι
F : ι → C(α, β)
f : C(α, β)
⊢ Filter.Tendsto F l (𝓝 f) ↔
    ∀ (s : Set α), IsCompact s → Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (restrict s f))
[PROOFSTEP]
rw [compactOpen_eq_sInf_induced]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
ι : Type u_4
l : Filter ι
F : ι → C(α, β)
f : C(α, β)
⊢ Filter.Tendsto F l (𝓝 f) ↔
    ∀ (s : Set α), IsCompact s → Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (restrict s f))
[PROOFSTEP]
simp [nhds_iInf, nhds_induced, Filter.tendsto_comap_iff, Function.comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
⊢ (∃ f, Filter.Tendsto F l (𝓝 f)) ↔ ∀ (s : Set α), IsCompact s → ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
⊢ (∃ f, Filter.Tendsto F l (𝓝 f)) → ∀ (s : Set α), IsCompact s → ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)
[PROOFSTEP]
rintro ⟨f, hf⟩ s _
[GOAL]
case mp.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : C(α, β)
hf : Filter.Tendsto F l (𝓝 f)
s : Set α
hs✝ : IsCompact s
⊢ ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)
[PROOFSTEP]
exact ⟨f.restrict s, tendsto_compactOpen_restrict hf s⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
⊢ (∀ (s : Set α), IsCompact s → ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)) → ∃ f, Filter.Tendsto F l (𝓝 f)
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
h : ∀ (s : Set α), IsCompact s → ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)
⊢ ∃ f, Filter.Tendsto F l (𝓝 f)
[PROOFSTEP]
choose f hf using h
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
⊢ ∃ f, Filter.Tendsto F l (𝓝 f)
[PROOFSTEP]
have h :
  ∀ (s₁) (hs₁ : IsCompact s₁) (s₂) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    f s₁ hs₁ ⟨x, hxs₁⟩ = f s₂ hs₂ ⟨x, hxs₂⟩ :=
  by
  rintro s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂
  haveI := isCompact_iff_compactSpace.mp hs₁
  haveI := isCompact_iff_compactSpace.mp hs₂
  have h₁ := (continuous_eval_const (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)
  have h₂ := (continuous_eval_const (⟨x, hxs₂⟩ : s₂)).continuousAt.tendsto.comp (hf s₂ hs₂)
  exact tendsto_nhds_unique h₁ h₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
⊢ ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
[PROOFSTEP]
rintro s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
[PROOFSTEP]
haveI := isCompact_iff_compactSpace.mp hs₁
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this : CompactSpace ↑s₁
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
[PROOFSTEP]
haveI := isCompact_iff_compactSpace.mp hs₂
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this✝ : CompactSpace ↑s₁
this : CompactSpace ↑s₂
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
[PROOFSTEP]
have h₁ := (continuous_eval_const (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this✝ : CompactSpace ↑s₁
this : CompactSpace ↑s₂
h₁ :
  Filter.Tendsto ((fun f => ↑f { val := x, property := hxs₁ }) ∘ fun i => restrict s₁ (F i)) l
    (𝓝 (↑(f s₁ hs₁) { val := x, property := hxs₁ }))
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
[PROOFSTEP]
have h₂ := (continuous_eval_const (⟨x, hxs₂⟩ : s₂)).continuousAt.tendsto.comp (hf s₂ hs₂)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this✝ : CompactSpace ↑s₁
this : CompactSpace ↑s₂
h₁ :
  Filter.Tendsto ((fun f => ↑f { val := x, property := hxs₁ }) ∘ fun i => restrict s₁ (F i)) l
    (𝓝 (↑(f s₁ hs₁) { val := x, property := hxs₁ }))
h₂ :
  Filter.Tendsto ((fun f => ↑f { val := x, property := hxs₂ }) ∘ fun i => restrict s₂ (F i)) l
    (𝓝 (↑(f s₂ hs₂) { val := x, property := hxs₂ }))
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
[PROOFSTEP]
exact tendsto_nhds_unique h₁ h₂
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
⊢ ∃ f, Filter.Tendsto F l (𝓝 f)
[PROOFSTEP]
have hs : ∀ x : α, ∃ (s : _), IsCompact s ∧ s ∈ 𝓝 x := by
  intro x
  obtain ⟨s, hs, hs'⟩ := exists_compact_mem_nhds x
  exact ⟨s, hs, hs'⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
⊢ ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
x : α
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x
[PROOFSTEP]
obtain ⟨s, hs, hs'⟩ := exists_compact_mem_nhds x
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
x : α
s : Set α
hs : IsCompact s
hs' : s ∈ 𝓝 x
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x
[PROOFSTEP]
exact ⟨s, hs, hs'⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
⊢ ∃ f, Filter.Tendsto F l (𝓝 f)
[PROOFSTEP]
refine ⟨liftCover' _ _ h hs, ?_⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
⊢ Filter.Tendsto F l
    (𝓝
      (liftCover'
        (fun s => ∀ ⦃f : Filter α⦄ [inst : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f)
        (fun s hs => f s hs) h hs))
[PROOFSTEP]
rw [tendsto_compactOpen_iff_forall]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
⊢ ∀ (s : Set α),
    IsCompact s →
      Filter.Tendsto (fun i => restrict s (F i)) l
        (𝓝
          (restrict s
            (liftCover'
              (fun s => ∀ ⦃f : Filter α⦄ [inst : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f)
              (fun s hs => f s hs) h hs)))
[PROOFSTEP]
intro s hs
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs✝ : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
s : Set α
hs : IsCompact s
⊢ Filter.Tendsto (fun i => restrict s (F i)) l
    (𝓝
      (restrict s
        (liftCover'
          (fun s => ∀ ⦃f : Filter α⦄ [inst : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f)
          (fun s hs => f s hs) h hs✝)))
[PROOFSTEP]
rw [liftCover_restrict']
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs✝ : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
s : Set α
hs : IsCompact s
⊢ Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s ?m.52935))
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : LocallyCompactSpace α
inst✝¹ : T2Space β
ι : Type u_4
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs✝ : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
s : Set α
hs : IsCompact s
⊢ s ∈ fun s => ∀ ⦃f : Filter α⦄ [inst : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f
[PROOFSTEP]
exact hf s hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
y : β
s : Set α
⊢ ↑(coev α β y) '' s = {y} ×ˢ s
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ ∀ (s : Set C(α, β × α)), s ∈ {m | ∃ s x u x, m = CompactOpen.gen s u} → IsOpen (coev α β ⁻¹' s)
[PROOFSTEP]
rintro _ ⟨s, sc, u, uo, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
⊢ IsOpen (coev α β ⁻¹' CompactOpen.gen s u)
[PROOFSTEP]
rw [isOpen_iff_forall_mem_open]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
⊢ ∀ (x : β), x ∈ coev α β ⁻¹' CompactOpen.gen s u → ∃ t, t ⊆ coev α β ⁻¹' CompactOpen.gen s u ∧ IsOpen t ∧ x ∈ t
[PROOFSTEP]
intro y hy
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
y : β
hy : y ∈ coev α β ⁻¹' CompactOpen.gen s u
⊢ ∃ t, t ⊆ coev α β ⁻¹' CompactOpen.gen s u ∧ IsOpen t ∧ y ∈ t
[PROOFSTEP]
have hy' : (↑(coev α β y) '' s ⊆ u) := hy
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
y : β
hy : y ∈ coev α β ⁻¹' CompactOpen.gen s u
hy' : ↑(coev α β y) '' s ⊆ u
⊢ ∃ t, t ⊆ coev α β ⁻¹' CompactOpen.gen s u ∧ IsOpen t ∧ y ∈ t
[PROOFSTEP]
rw [image_coev s] at hy' 
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
y : β
hy : y ∈ coev α β ⁻¹' CompactOpen.gen s u
hy' : {y} ×ˢ s ⊆ u
⊢ ∃ t, t ⊆ coev α β ⁻¹' CompactOpen.gen s u ∧ IsOpen t ∧ y ∈ t
[PROOFSTEP]
rcases generalized_tube_lemma isCompact_singleton sc uo hy' with ⟨v, w, vo, _, yv, sw, vwu⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
y : β
hy : y ∈ coev α β ⁻¹' CompactOpen.gen s u
hy' : {y} ×ˢ s ⊆ u
v : Set β
w : Set α
vo : IsOpen v
left✝ : IsOpen w
yv : {y} ⊆ v
sw : s ⊆ w
vwu : v ×ˢ w ⊆ u
⊢ ∃ t, t ⊆ coev α β ⁻¹' CompactOpen.gen s u ∧ IsOpen t ∧ y ∈ t
[PROOFSTEP]
refine' ⟨v, _, vo, singleton_subset_iff.mp yv⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
y : β
hy : y ∈ coev α β ⁻¹' CompactOpen.gen s u
hy' : {y} ×ˢ s ⊆ u
v : Set β
w : Set α
vo : IsOpen v
left✝ : IsOpen w
yv : {y} ⊆ v
sw : s ⊆ w
vwu : v ×ˢ w ⊆ u
⊢ v ⊆ coev α β ⁻¹' CompactOpen.gen s u
[PROOFSTEP]
intro y' hy'
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
y : β
hy : y ∈ coev α β ⁻¹' CompactOpen.gen s u
hy'✝ : {y} ×ˢ s ⊆ u
v : Set β
w : Set α
vo : IsOpen v
left✝ : IsOpen w
yv : {y} ⊆ v
sw : s ⊆ w
vwu : v ×ˢ w ⊆ u
y' : β
hy' : y' ∈ v
⊢ y' ∈ coev α β ⁻¹' CompactOpen.gen s u
[PROOFSTEP]
change coev α β y' '' s ⊆ u
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
y : β
hy : y ∈ coev α β ⁻¹' CompactOpen.gen s u
hy'✝ : {y} ×ˢ s ⊆ u
v : Set β
w : Set α
vo : IsOpen v
left✝ : IsOpen w
yv : {y} ⊆ v
sw : s ⊆ w
vwu : v ×ˢ w ⊆ u
y' : β
hy' : y' ∈ v
⊢ ↑(coev α β y') '' s ⊆ u
[PROOFSTEP]
rw [image_coev s]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
y : β
hy : y ∈ coev α β ⁻¹' CompactOpen.gen s u
hy'✝ : {y} ×ˢ s ⊆ u
v : Set β
w : Set α
vo : IsOpen v
left✝ : IsOpen w
yv : {y} ⊆ v
sw : s ⊆ w
vwu : v ×ˢ w ⊆ u
y' : β
hy' : y' ∈ v
⊢ {y'} ×ˢ s ⊆ u
[PROOFSTEP]
exact (prod_mono (singleton_subset_iff.mpr hy') sw).trans vwu
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(α × β, γ)
⊢ curry' f = comp f ∘ coev β α
[PROOFSTEP]
ext
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : C(α × β, γ)
x✝ : α
a✝ : β
⊢ ↑(curry' f x✝) a✝ = ↑((comp f ∘ coev β α) x✝) a✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : LocallyCompactSpace (α × β)
⊢ Continuous curry
[PROOFSTEP]
apply continuous_of_continuous_uncurry
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : LocallyCompactSpace (α × β)
⊢ Continuous (Function.uncurry fun x y => ↑(curry x) y)
[PROOFSTEP]
apply continuous_of_continuous_uncurry
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : LocallyCompactSpace (α × β)
⊢ Continuous (Function.uncurry fun x y => ↑(Function.uncurry (fun x y => ↑(curry x) y) x) y)
[PROOFSTEP]
rw [← (Homeomorph.prodAssoc _ _ _).symm.comp_continuous_iff']
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : LocallyCompactSpace (α × β)
⊢ Continuous
    ((Function.uncurry fun x y => ↑(Function.uncurry (fun x y => ↑(curry x) y) x) y) ∘
      ↑(Homeomorph.symm (Homeomorph.prodAssoc C(α × β, γ) α β)))
[PROOFSTEP]
exact continuous_eval'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
⊢ Continuous uncurry
[PROOFSTEP]
apply continuous_of_continuous_uncurry
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
⊢ Continuous (Function.uncurry fun x y => ↑(uncurry x) y)
[PROOFSTEP]
rw [← (Homeomorph.prodAssoc _ _ _).comp_continuous_iff']
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
⊢ Continuous ((Function.uncurry fun x y => ↑(uncurry x) y) ∘ ↑(Homeomorph.prodAssoc C(α, C(β, γ)) α β))
[PROOFSTEP]
apply continuous_eval'.comp (continuous_eval'.prod_map continuous_id)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
⊢ Function.LeftInverse uncurry ContinuousMap.curry
[PROOFSTEP]
intro
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
x✝ : C(α × β, γ)
⊢ uncurry (ContinuousMap.curry x✝) = x✝
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
x✝ : C(α × β, γ)
a✝ : α × β
⊢ ↑(uncurry (ContinuousMap.curry x✝)) a✝ = ↑x✝ a✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
⊢ Function.RightInverse uncurry ContinuousMap.curry
[PROOFSTEP]
intro
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
x✝ : C(α, C(β, γ))
⊢ ContinuousMap.curry (uncurry x✝) = x✝
[PROOFSTEP]
ext
[GOAL]
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LocallyCompactSpace α
inst✝ : LocallyCompactSpace β
x✝ : C(α, C(β, γ))
a✝¹ : α
a✝ : β
⊢ ↑(↑(ContinuousMap.curry (uncurry x✝)) a✝¹) a✝ = ↑(↑x✝ a✝¹) a✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : Unique α
f : C(α, β)
⊢ const α ((fun f => ↑f default) f) = f
[PROOFSTEP]
ext a
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : Unique α
f : C(α, β)
a : α
⊢ ↑(const α ((fun f => ↑f default) f)) a = ↑f a
[PROOFSTEP]
rw [Unique.eq_default a]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : Unique α
f : C(α, β)
a : α
⊢ ↑(const α ((fun f => ↑f default) f)) default = ↑f default
[PROOFSTEP]
rfl
[GOAL]
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
[PROOFSTEP]
let Gf : C(X₀, C(Y, Z)) := ContinuousMap.curry ⟨_, hg⟩
[GOAL]
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
[PROOFSTEP]
have h : ∀ x : X, Continuous fun y => g (x, y) := by
  intro x
  obtain ⟨x₀, rfl⟩ := hf.surjective x
  exact (Gf x₀).continuous
[GOAL]
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)
[PROOFSTEP]
intro x
[GOAL]
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)
[PROOFSTEP]
obtain ⟨x₀, rfl⟩ := hf.surjective x
[GOAL]
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)
[PROOFSTEP]
exact (Gf x₀).continuous
[GOAL]
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
[PROOFSTEP]
let G : X → C(Y, Z) := fun x => ⟨_, h x⟩
[GOAL]
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
[PROOFSTEP]
have : Continuous G := by
  rw [hf.continuous_iff]
  exact Gf.continuous
[GOAL]
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
[PROOFSTEP]
rw [hf.continuous_iff]
[GOAL]
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)
[PROOFSTEP]
exact Gf.continuous
[GOAL]
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
[PROOFSTEP]
exact ContinuousMap.continuous_uncurry_of_continuous ⟨G, this⟩
[GOAL]
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
[PROOFSTEP]
have : Continuous fun p : X₀ × Y => g ((Prod.swap p).1, f (Prod.swap p).2) := hg.comp continuous_swap
[GOAL]
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
[PROOFSTEP]
have : Continuous fun p : X₀ × Y => (g ∘ Prod.swap) (f p.1, p.2) := this
[GOAL]
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
[PROOFSTEP]
exact (hf.continuous_lift_prod_left this).comp continuous_swap
