α : Type u_1
β : Type ?u.19949
σ✝ : Type ?u.19952
τ : Type ?u.19955
T : TopologicalSpace α
σ : Type u_2
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ f F b ∧ f F b ⊆ s
x : α
⊢ 𝓝 x = 𝓝 x
α : Type u_1
β : Type ?u.19949
σ✝ : Type ?u.19952
τ : Type ?u.19955
T : TopologicalSpace α
σ : Type u_2
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ f F b ∧ f F b ⊆ s
⊢ toTopsp F = T
refine' eq_of_nhds_eq_nhds fun x ↦ _
case a
α : Type u_1
β : Type ?u.19949
σ✝ : Type ?u.19952
τ : Type ?u.19955
T : TopologicalSpace α
σ : Type u_2
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ f F b ∧ f F b ⊆ s
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ s ∈ 𝓝 x
α : Type u_1
β : Type ?u.19949
σ✝ : Type ?u.19952
τ : Type ?u.19955
T : TopologicalSpace α
σ : Type u_2
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ f F b ∧ f F b ⊆ s
x : α
⊢ 𝓝 x = 𝓝 x
ext s
no goals
case a
α : Type u_1
β : Type ?u.19949
σ✝ : Type ?u.19952
τ : Type ?u.19955
T : TopologicalSpace α
σ : Type u_2
F : Ctop α σ
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ f F b ∧ f F b ⊆ s
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ s ∈ 𝓝 x
rw [mem_nhds_toTopsp, H]