α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x✝ : α
x : G
s : Set G
⊢ (∀ (i : Set G), i ∈ 𝓝 1 → ∃ y, y ∈ s ∧ y ∈ {y | y / x ∈ id i}) ↔ ∀ (U : Set G), U ∈ 𝓝 1 → ∃ y, y ∈ s ∧ y / x ∈ U
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x✝ : α
x : G
s : Set G
⊢ x ∈ closure s ↔ ∀ (U : Set G), U ∈ 𝓝 1 → ∃ y, y ∈ s ∧ y / x ∈ U
rw [mem_closure_iff_nhds_basis ((𝓝 1 : Filter G).basis_sets.nhds_of_one x)]
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x✝ : α
x : G
s : Set G
⊢ (∀ (i : Set G), i ∈ 𝓝 1 → ∃ y, y ∈ s ∧ y ∈ {y | y / x ∈ id i}) ↔ ∀ (U : Set G), U ∈ 𝓝 1 → ∃ y, y ∈ s ∧ y / x ∈ U
simp_rw [Set.mem_setOf, id]