Theorems · Definition · Lie groups

MulOpposite.opUniformEquivRight

(G : Type u_2) → [inst : Group G] → [inst_1 : TopologicalSpace G] → [inst_2 : IsTopologicalGroup G] → G ≃ᵤ Gᵐᵒᵖ

The equivalence between a topological group G and Gᵐᵒᵖ as a uniform equivalence when G is equipped with the right uniformity and Gᵐᵒᵖ with the left uniformity.

Defined in

Mathlib.Topology.Algebra.IsUniformGroup.Basic

Cited by

0 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupTopologicalSpaceIsTopologicalGroup