α : 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✝ : α
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : HasBasis (𝓝 1) p s
x : G
⊢ HasBasis (Filter.comap (fun y => y * x⁻¹) (𝓝 1)) p fun i => {y | y / x ∈ s i}
α : 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✝ : α
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : HasBasis (𝓝 1) p s
x : G
⊢ HasBasis (𝓝 x) p fun i => {y | y / x ∈ s i}
rw [← nhds_translation_mul_inv]
α : 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✝ : α
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : HasBasis (𝓝 1) p s
x : G
⊢ HasBasis (Filter.comap (fun y => y * x⁻¹) (𝓝 1)) p fun i => {y | y * x⁻¹ ∈ s i}
α : 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✝ : α
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : HasBasis (𝓝 1) p s
x : G
⊢ HasBasis (Filter.comap (fun y => y * x⁻¹) (𝓝 1)) p fun i => {y | y / x ∈ s i}
simp_rw [div_eq_mul_inv]
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✝ : α
ι : Sort u_1
p : ι → Prop
s : ι → Set G
hb : HasBasis (𝓝 1) p s
x : G
⊢ HasBasis (Filter.comap (fun y => y * x⁻¹) (𝓝 1)) p fun i => {y | y * x⁻¹ ∈ s i}
exact hb.comap _