α : Type u_1
β : Type ?u.8047
σ : Type ?u.8050
τ : Type ?u.8053
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : s ∈ 𝓝 a ↔ ∃ b, a ∈ f F.F b ∧ f F.F b ⊆ s
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ f F.F b ∧ f F.F b ⊆ s
α : Type u_1
β : Type ?u.8047
σ : Type ?u.8050
τ : Type ?u.8053
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ f F.F b ∧ f F.F b ⊆ s
have := @mem_nhds_toTopsp _ _ F.F s a
no goals
α : Type u_1
β : Type ?u.8047
σ : Type ?u.8050
τ : Type ?u.8053
T : TopologicalSpace α
F : Realizer α
s : Set α
a : α
this : s ∈ 𝓝 a ↔ ∃ b, a ∈ f F.F b ∧ f F.F b ⊆ s
⊢ s ∈ 𝓝 a ↔ ∃ b, a ∈ f F.F b ∧ f F.F b ⊆ s
rwa [F.eq] at this