α : Type u_1
β : Type ?u.171854
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ comap ((fun x => x.fst⁻¹ * x.snd) ∘ Prod.swap) (𝓝 1) = comap (fun x => x.snd⁻¹ * x.fst) (𝓝 1)
α : Type u_1
β : Type ?u.171854
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ 𝓤 α = comap (fun x => x.snd⁻¹ * x.fst) (𝓝 1)
rw [← comap_swap_uniformity, uniformity_eq_comap_inv_mul_nhds_one, comap_comap]
no goals
α : Type u_1
β : Type ?u.171854
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ comap ((fun x => x.fst⁻¹ * x.snd) ∘ Prod.swap) (𝓝 1) = comap (fun x => x.snd⁻¹ * x.fst) (𝓝 1)
rfl