mulLeft — Mathlib

English

Left multiplication by any element a in G is a homeomorphism G → G.

Русский

Левое умножение на произвольный элемент a в группе G является гомеоморфизмом G → G.

LaTeX

$$$\\forall a\\in G:\\ (x\\mapsto a x) \\text{ is a homeomorphism } G \\to G.$$$

Lean4

/-- Multiplication from the left in a topological group as a homeomorphism. -/
@[to_additive /-- Addition from the left in a topological additive group as a homeomorphism. -/
    ]
protected def mulLeft (a : G) : G ≃ₜ G :=
  { Equiv.mulLeft a with
    continuous_toFun := continuous_const.mul continuous_id
    continuous_invFun := continuous_const.mul continuous_id }

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