instIsIsometricSMulMulOpposite — Mathlib

English

If M acts isometrically on X, then M acts isometrically on the opposite space Xᵐᵒᵖ with distance preserved via the opposite structure.

Русский

Если M действует изометрически на X, то оно действует изометрически на Xᵐᵒᵖ, сохраняя расстояния через противоположную структуру.

LaTeX

$$$\text{IsIsometricSMul}(M, X^{\mathrm{op}})$ with $d^{\mathrm{op}}(m\cdot x^{\mathrm{op}}, m\cdot y^{\mathrm{op}}) = d^{\mathrm{op}}(x^{\mathrm{op}}, y^{\mathrm{op}})$$$

Lean4

@[to_additive]
instance : IsIsometricSMul M Xᵐᵒᵖ :=
  ⟨fun c x y => by simpa only using edist_smul_left c x.unop y.unop⟩

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