isIsIsometricVAdd'' — Mathlib

English

Opposite-structure action by MulOpposite / Multiplicative preserves distances with a reversed VAdd on M.

Русский

Противоположная структура действия MulOpposite сохраняет расстояния при обратной структуре VAdd на M.

LaTeX

$$$\\forall c \\in (M)^{\\mathrm{op}}, \\forall x,y:\\ edist(c \\cdot x, c \\cdot y) = edist(x,y).$$$

Lean4

instance isIsIsometricVAdd'' [Add M] [PseudoEMetricSpace M] [IsIsometricVAdd Mᵃᵒᵖ M] :
    IsIsometricSMul (Multiplicative M)ᵐᵒᵖ (Multiplicative M) :=
  ⟨fun c x y => edist_vadd_left (AddOpposite.op c.unop.toAdd) x.toAdd y.toAdd⟩

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