map_vsub

Mathlib.Analysis.Normed.Affine.Isometry

URI: https://scilib.ai/kg/mathlib#AffineIsometry.map_vsub

English

If two affine isometries agree on all inputs, they are equal.

Русский

Если две аффинные изометрии совпадают на всех точках, они равны.

LaTeX

$$$∀ f,g : P \toᵃⁱ[𝕜] P₂, ∀ x, f x = g x ⇒ f = g$$$

Lean4

@[simp]
theorem map_vsub (p1 p2 : P) : f.linearIsometry (p1 -ᵥ p2) = f p1 -ᵥ f p2 :=
  f.toAffineMap.linearMap_vsub p1 p2

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru