continuous_conj — Mathlib

English

For a fixed element g ∈ G, the map h ↦ g h g⁻¹ is continuous.

Русский

Для фиксированного элемента g ∈ G отображение h ↦ g h g⁻¹ непрерывно.

LaTeX

$$$\forall g\in G,\; h \mapsto g h g^{-1} \text{ is continuous on } G.$$$

Lean4

/-- Conjugation by a fixed element is continuous when `mul` is continuous. -/
@[to_additive (attr := continuity) /-- Conjugation by a fixed element is continuous when `add` is continuous. -/
    ]
theorem continuous_conj (g : G) : Continuous fun h : G => g * h * g⁻¹ :=
  (continuous_mul_right g⁻¹).comp (continuous_mul_left g)

Похожие утверждения