α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
o : IsOpen s
sf : 𝓟 s ≤ f
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ IsOpen s}), 𝓟 s) ≤ f
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
o : IsOpen s
sf : 𝓟 s ≤ f
⊢ 𝓝 a ≤ f
rw [nhds_def]
no goals
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
o : IsOpen s
sf : 𝓟 s ≤ f
⊢ (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ IsOpen s}), 𝓟 s) ≤ f
exact iInf₂_le_of_le s ⟨h, o⟩ sf