α : Type u
β : Type v
ι : Type ?u.90929
π : ι → Type ?u.90934
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed s
⊢ ∀ (a : Y), a ∈ (Prod.snd '' s)ᶜ → (Prod.snd '' s)ᶜ ∈ 𝓝 a
α : Type u
β : Type v
ι : Type ?u.90929
π : ι → Type ?u.90934
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed s
⊢ IsClosed (Prod.snd '' s)
rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
α : Type u
β : Type v
ι : Type ?u.90929
π : ι → Type ?u.90934
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
⊢ (Prod.snd '' s)ᶜ ∈ 𝓝 y
α : Type u
β : Type v
ι : Type ?u.90929
π : ι → Type ?u.90934
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed s
⊢ ∀ (a : Y), a ∈ (Prod.snd '' s)ᶜ → (Prod.snd '' s)ᶜ ∈ 𝓝 a
intro y hy
case this
α : Type u
β : Type v
ι : Type ?u.90929
π : ι → Type ?u.90934
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
⊢ univ ×ˢ {y} ⊆ sᶜ

α : Type u
β : Type v
ι : Type ?u.90929
π : ι → Type ?u.90934
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
this : univ ×ˢ {y} ⊆ sᶜ
⊢ (Prod.snd '' s)ᶜ ∈ 𝓝 y
α : Type u
β : Type v
ι : Type ?u.90929
π : ι → Type ?u.90934
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
⊢ (Prod.snd '' s)ᶜ ∈ 𝓝 y
have : univ ×ˢ {y} ⊆ sᶜ
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.90929
π : ι → Type ?u.90934
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs✝ : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
this : univ ×ˢ {y} ⊆ sᶜ
U : Set X
V : Set Y
hVo : IsOpen V
hU : univ ⊆ U
hV : {y} ⊆ V
hs : U ×ˢ V ⊆ sᶜ
⊢ (Prod.snd '' s)ᶜ ∈ 𝓝 y
α : Type u
β : Type v
ι : Type ?u.90929
π : ι → Type ?u.90934
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
this : univ ×ˢ {y} ⊆ sᶜ
⊢ (Prod.snd '' s)ᶜ ∈ 𝓝 y
rcases generalized_tube_lemma isCompact_univ isCompact_singleton hs.isOpen_compl this
  with ⟨U, V, -, hVo, hU, hV, hs⟩
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.90929
π : ι → Type ?u.90934
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs✝ : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
this : univ ×ˢ {y} ⊆ sᶜ
U : Set X
V : Set Y
hVo : IsOpen V
hU : univ ⊆ U
hV : {y} ⊆ V
hs : U ×ˢ V ⊆ sᶜ
⊢ V ⊆ (Prod.snd '' s)ᶜ
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.90929
π : ι → Type ?u.90934
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs✝ : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
this : univ ×ˢ {y} ⊆ sᶜ
U : Set X
V : Set Y
hVo : IsOpen V
hU : univ ⊆ U
hV : {y} ⊆ V
hs : U ×ˢ V ⊆ sᶜ
⊢ (Prod.snd '' s)ᶜ ∈ 𝓝 y
refine mem_nhds_iff.2 ⟨V, ?_, hVo, hV rfl⟩
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.90929
π : ι → Type ?u.90934
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs✝ : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
this : univ ×ˢ {y} ⊆ sᶜ
U : Set X
V : Set Y
hVo : IsOpen V
hU : univ ⊆ U
hV : {y} ⊆ V
hs : U ×ˢ V ⊆ sᶜ
z : X × Y
hzs : z ∈ s
hzV : z.snd ∈ V
⊢ False
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.90929
π : ι → Type ?u.90934
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs✝ : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
this : univ ×ˢ {y} ⊆ sᶜ
U : Set X
V : Set Y
hVo : IsOpen V
hU : univ ⊆ U
hV : {y} ⊆ V
hs : U ×ˢ V ⊆ sᶜ
⊢ V ⊆ (Prod.snd '' s)ᶜ
rintro _ hzV ⟨z, hzs, rfl⟩
no goals
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.90929
π : ι → Type ?u.90934
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs✝ : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
this : univ ×ˢ {y} ⊆ sᶜ
U : Set X
V : Set Y
hVo : IsOpen V
hU : univ ⊆ U
hV : {y} ⊆ V
hs : U ×ˢ V ⊆ sᶜ
z : X × Y
hzs : z ∈ s
hzV : z.snd ∈ V
⊢ False
exact hs ⟨hU trivial, hzV⟩ hzs
no goals
case this
α : Type u
β : Type v
ι : Type ?u.90929
π : ι → Type ?u.90934
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
⊢ univ ×ˢ {y} ⊆ sᶜ
exact fun (x, y') ⟨_, rfl⟩ hs => hy ⟨(x, y'), hs, rfl⟩