α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
⊢ HasBasis (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ IsOpen s}), 𝓟 s) (fun s => a ∈ s ∧ IsOpen s) fun s => s
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
⊢ HasBasis (𝓝 a) (fun s => a ∈ s ∧ IsOpen s) fun s => s
rw [nhds_def]
no goals
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
⊢ HasBasis (⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ IsOpen s}), 𝓟 s) (fun s => a ∈ s ∧ IsOpen s) fun s => s
exact hasBasis_biInf_principal
  (fun s ⟨has, hs⟩ t ⟨hat, ht⟩ =>
    ⟨s ∩ t, ⟨⟨has, hat⟩, IsOpen.inter hs ht⟩, ⟨inter_subset_left _ _, inter_subset_right _ _⟩⟩)
  ⟨univ, ⟨mem_univ a, isOpen_univ⟩⟩