smul — Mathlib

English

For any γ ∈ G, the map x ↦ γ · x on α is a homeomorphism from α to itself.

Русский

Для любого γ ∈ G отображение x ↦ γ · x на пространстве α является гомеоморфизмом α в себя.

LaTeX

$$$(x \mapsto c \cdot x): \alpha \to \alpha \text{ is a homeomorphism}$$$

Lean4

/-- The homeomorphism given by scalar multiplication by a given element of a group `Γ` acting on
  `T` is a homeomorphism from `T` to itself. -/
@[to_additive (attr := simps!)]
def smul (γ : G) : α ≃ₜ α where
  toEquiv := MulAction.toPerm γ
  continuous_toFun := continuous_const_smul γ
  continuous_invFun := continuous_const_smul γ⁻¹

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