case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
⊢ IsOpen (coev α β ⁻¹' CompactOpen.gen s u)
α : Type u_2
β : Type u_1
γ : Type ?u.41809
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
⊢ ∀ (s : Set C(α, β × α)), s ∈ {m | ∃ s x u x, m = CompactOpen.gen s u} → IsOpen (coev α β ⁻¹' s)
rintro _ ⟨s, sc, u, uo, rfl⟩
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
sc : IsCompact s
u : Set (β × α)
uo : IsOpen u
⊢ IsOpen (coev α β ⁻¹' CompactOpen.gen s u)
rw [isOpen_iff_forall_mem_open]
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
intro y hy
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
have hy' : (↑(coev α β y) '' s ⊆ u) := hy
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
rw [image_coev s] at hy'
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
rcases generalized_tube_lemma isCompact_singleton sc uo hy' with ⟨v, w, vo, _, yv, sw, vwu⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
refine' ⟨v, _, vo, singleton_subset_iff.mp yv⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
intro y' hy'
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
change coev α β y' '' s ⊆ u
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
rw [image_coev s]
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.41809
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
exact (prod_mono (singleton_subset_iff.mpr hy') sw).trans vwu