α : Type u
β : Type v
ι : Type ?u.1080
π : ι → Type ?u.1085
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
f : Filter α
hf : ∀ (a : α), a ∈ s → ∃ t, t ∈ 𝓝[s] a ∧ tᶜ ∈ f
a : α
ha : a ∈ s
⊢ sᶜ ∈ 𝓝 a ⊓ f
α : Type u
β : Type v
ι : Type ?u.1080
π : ι → Type ?u.1085
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
f : Filter α
hf : ∀ (a : α), a ∈ s → ∃ t, t ∈ 𝓝[s] a ∧ tᶜ ∈ f
⊢ sᶜ ∈ f
refine' hs.compl_mem_sets fun a ha => _
case intro.intro
α : Type u
β : Type v
ι : Type ?u.1080
π : ι → Type ?u.1085
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
hs : IsCompact s
f : Filter α
hf : ∀ (a : α), a ∈ s → ∃ t, t ∈ 𝓝[s] a ∧ tᶜ ∈ f
a : α
ha : a ∈ s
t : Set α
ht : t ∈ 𝓝[s] a
hst : tᶜ ∈ f
⊢ sᶜ ∈ 𝓝 a ⊓ f
α : Type u
β : Type v
ι : Type ?u.1080
π : ι → Type ?u.1085
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
f : Filter α
hf : ∀ (a : α), a ∈ s → ∃ t, t ∈ 𝓝[s] a ∧ tᶜ ∈ f
a : α
ha : a ∈ s
⊢ sᶜ ∈ 𝓝 a ⊓ f
rcases hf a ha with ⟨t, ht, hst⟩
case intro.intro
α : Type u
β : Type v
ι : Type ?u.1080
π : ι → Type ?u.1085
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
hs : IsCompact s
f : Filter α
hf : ∀ (a : α), a ∈ s → ∃ t, t ∈ 𝓝[s] a ∧ tᶜ ∈ f
a : α
ha : a ∈ s
t : Set α
hst : tᶜ ∈ f
ht : {x | x ∈ s → x ∈ t} ∈ 𝓝 a
⊢ sᶜ ∈ 𝓝 a ⊓ f
case intro.intro
α : Type u
β : Type v
ι : Type ?u.1080
π : ι → Type ?u.1085
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
hs : IsCompact s
f : Filter α
hf : ∀ (a : α), a ∈ s → ∃ t, t ∈ 𝓝[s] a ∧ tᶜ ∈ f
a : α
ha : a ∈ s
t : Set α
ht : t ∈ 𝓝[s] a
hst : tᶜ ∈ f
⊢ sᶜ ∈ 𝓝 a ⊓ f
replace ht := mem_inf_principal.1 ht
case intro.intro
α : Type u
β : Type v
ι : Type ?u.1080
π : ι → Type ?u.1085
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
hs : IsCompact s
f : Filter α
hf : ∀ (a : α), a ∈ s → ∃ t, t ∈ 𝓝[s] a ∧ tᶜ ∈ f
a : α
ha : a ∈ s
t : Set α
hst : tᶜ ∈ f
ht : {x | x ∈ s → x ∈ t} ∈ 𝓝 a
⊢ {x | x ∈ s → x ∈ t} ∩ tᶜ ⊆ sᶜ
case intro.intro
α : Type u
β : Type v
ι : Type ?u.1080
π : ι → Type ?u.1085
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
hs : IsCompact s
f : Filter α
hf : ∀ (a : α), a ∈ s → ∃ t, t ∈ 𝓝[s] a ∧ tᶜ ∈ f
a : α
ha : a ∈ s
t : Set α
hst : tᶜ ∈ f
ht : {x | x ∈ s → x ∈ t} ∈ 𝓝 a
⊢ sᶜ ∈ 𝓝 a ⊓ f
apply mem_inf_of_inter ht hst
case intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.1080
π : ι → Type ?u.1085
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
hs✝ : IsCompact s
f : Filter α
hf : ∀ (a : α), a ∈ s → ∃ t, t ∈ 𝓝[s] a ∧ tᶜ ∈ f
a : α
ha : a ∈ s
t : Set α
hst : tᶜ ∈ f
ht : {x | x ∈ s → x ∈ t} ∈ 𝓝 a
x : α
h₁ : x ∈ {x | x ∈ s → x ∈ t}
h₂ : x ∈ tᶜ
hs : x ∈ s
⊢ False
case intro.intro
α : Type u
β : Type v
ι : Type ?u.1080
π : ι → Type ?u.1085
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
hs : IsCompact s
f : Filter α
hf : ∀ (a : α), a ∈ s → ∃ t, t ∈ 𝓝[s] a ∧ tᶜ ∈ f
a : α
ha : a ∈ s
t : Set α
hst : tᶜ ∈ f
ht : {x | x ∈ s → x ∈ t} ∈ 𝓝 a
⊢ {x | x ∈ s → x ∈ t} ∩ tᶜ ⊆ sᶜ
rintro x ⟨h₁, h₂⟩ hs
no goals
case intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.1080
π : ι → Type ?u.1085
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
hs✝ : IsCompact s
f : Filter α
hf : ∀ (a : α), a ∈ s → ∃ t, t ∈ 𝓝[s] a ∧ tᶜ ∈ f
a : α
ha : a ∈ s
t : Set α
hst : tᶜ ∈ f
ht : {x | x ∈ s → x ∈ t} ∈ 𝓝 a
x : α
h₁ : x ∈ {x | x ∈ s → x ∈ t}
h₂ : x ∈ tᶜ
hs : x ∈ s
⊢ False
exact h₂ (h₁ hs)