continuous_conj' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Conjugation acting on fixed element of the group is continuous when both `mul` and
`inv` are continuous. -/
@[to_additive (attr := continuity) /-- Conjugation acting on fixed element of the additive group is continuous when both
        `add` and `neg` are continuous. -/
    ]
theorem continuous_conj' [ContinuousInv G] (h : G) : Continuous fun g : G => g * h * g⁻¹ :=
  (continuous_mul_right h).mul continuous_inv

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