infEdist_smul — Mathlib

English

If a group acts by isometries on α, then infEdist is preserved under this action: infEdist (c • x) (c • s) = infEdist x s.

Русский

Если элемент c действует изометрически, то infEdist сохраняется: infEdist (c • x) (c • s) = infEdist x s.

LaTeX

$$$\infEdist (c \cdot x) (c \cdot s) = \infEdist x s$$$

Lean4

@[to_additive (attr := simp)]
theorem infEdist_smul {M} [SMul M α] [IsIsometricSMul M α] (c : M) (x : α) (s : Set α) :
    infEdist (c • x) (c • s) = infEdist x s :=
  infEdist_image (isometry_smul _ _)

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