α : Type u
β : Type v
ι : Type ?u.205
π : ι → Type ?u.210
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
f : Filter α
hf : ¬sᶜ ∈ f
⊢ ∃ a, a ∈ s ∧ ¬sᶜ ∈ 𝓝 a ⊓ f
α : Type u
β : Type v
ι : Type ?u.205
π : ι → Type ?u.210
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
f : Filter α
hf : ∀ (a : α), a ∈ s → sᶜ ∈ 𝓝 a ⊓ f
⊢ sᶜ ∈ f
contrapose! hf
α : Type u
β : Type v
ι : Type ?u.205
π : ι → Type ?u.210
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
f : Filter α
hf : NeBot (f ⊓ 𝓟 s)
⊢ ∃ a, a ∈ s ∧ NeBot (𝓝 a ⊓ (f ⊓ 𝓟 s))
α : Type u
β : Type v
ι : Type ?u.205
π : ι → Type ?u.210
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
f : Filter α
hf : ¬sᶜ ∈ f
⊢ ∃ a, a ∈ s ∧ ¬sᶜ ∈ 𝓝 a ⊓ f
simp only [not_mem_iff_inf_principal_compl, compl_compl, inf_assoc] at hf ⊢
no goals
α : Type u
β : Type v
ι : Type ?u.205
π : ι → Type ?u.210
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
f : Filter α
hf : NeBot (f ⊓ 𝓟 s)
⊢ ∃ a, a ∈ s ∧ NeBot (𝓝 a ⊓ (f ⊓ 𝓟 s))
exact @hs _ hf inf_le_right