no goals
α : Type u_1
β : Type u_2
γ : Type ?u.10621
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
assumption
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.10621
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
assumption
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.10621
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
assumption