isIsometricSMul' — Mathlib

English

If each coordinate M_i acts on X_i by an isometry, then the coordinatewise action on the product space ∀ i, X_i is an isometry of the product.

Русский

Если на каждом координатном пространстве X_i действие M_i является изометрией, то покоординатное действие на произведении ∀ i X_i является изометрией произведения.

LaTeX

$$$\\forall i, \\text{Isometry}(f_i) \\implies \\text{Isometry}(\\Pi.map f)$$$

Lean4

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

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