case h.e'_4.h.a
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
x✝ : Set α
⊢ x✝ ∈ 𝓝 a ∧ IsOpen x✝ ↔ a ∈ x✝ ∧ IsOpen x✝
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
⊢ HasBasis (𝓝 a) (fun s => s ∈ 𝓝 a ∧ IsOpen s) fun x => x
convert nhds_basis_opens a using 2
no goals
case h.e'_4.h.a
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
x✝ : Set α
⊢ x✝ ∈ 𝓝 a ∧ IsOpen x✝ ↔ a ∈ x✝ ∧ IsOpen x✝
exact and_congr_left_iff.2 IsOpen.mem_nhds_iff