Closedness of conjugacy in compact groups

For a compact Hausdorff topological group, conjugacy is a closed relation on the product. The binary form allows both elements to vary, as needed when imposing conjugacy conditions on a family of group elements.

theorem TauCeti.isClosed_isConj_prod {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] : IsClosed {q : G × G | IsConj q.1 q.2}

In a compact Hausdorff topological group, the set of conjugate pairs is closed.