isIsometricSMul'' — Mathlib

English

The opposite-coordinate variant yields that the space (∀ i, M_i)ᵐᵒᵖ acts isometrically on (∀ i, X_i).

Русский

Противоположно-координатный вариант показывает, что пространство (∀ i, M_i)ᵐᵒᵖ действует изометрично на (∀ i, X_i).

LaTeX

$$$\\forall c \\in (\\prod_i M_i)^{\\mathrm{op}}, \\forall x,y, edist\\big(c \\cdot x, c \\cdot y\\big) = edist(x,y).$$$

Lean4

@[to_additive]
instance isIsometricSMul'' {ι} {M : ι → Type*} [Fintype ι] [∀ i, Mul (M i)] [∀ i, PseudoEMetricSpace (M i)]
    [∀ i, IsIsometricSMul (M i)ᵐᵒᵖ (M i)] : IsIsometricSMul (∀ i, M i)ᵐᵒᵖ (∀ i, M i) :=
  ⟨fun c => .piMap (fun i (x : M i) => x * c.unop i) fun _ => isometry_mul_right _⟩

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