instIsIsometricSMulForall — Mathlib

English

If each X_i carries an isometric M-action, then the product space ∀ i, X_i carries a natural isometric action of M given coordinatewise by (c · x)_i = c · x_i.

Русский

Если на каждом пространстве X_i задано изометрическое действие M, то произведение ∀ i X_i может быть снабжено естественным изометрическим действием M, действующим по координатам: (c · x)_i = c · x_i.

LaTeX

$$$\\forall c \\in M, \\forall x,y \\in \\prod_{i} X_i:\\ edist\\big(c \\cdot x, c \\cdot y\\big) = edist(x,y).$$$

Lean4

@[to_additive]
instance {ι} {X : ι → Type*} [Fintype ι] [∀ i, SMul M (X i)] [∀ i, PseudoEMetricSpace (X i)]
    [∀ i, IsIsometricSMul M (X i)] : IsIsometricSMul M (∀ i, X i) :=
  ⟨fun c => .piMap (fun _ => (c • ·)) fun i => isometry_smul (X i) c⟩

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