map_app

Mathlib.LinearAlgebra.QuadraticForm.Isometry

URI: https://scilib.ai/kg/mathlib#QuadraticMap.Isometry.map_app

English

If f: Q1 →qᵢ Q2 is an isometry, then for every m in M1, Q2(f(m)) = Q1(m).

Русский

Если f: Q1 →qᵢ Q2 — изометрия, то для каждого m в M1 выполняется Q2(f(m)) = Q1(m).

LaTeX

$$$\forall m \in M_1,\; Q_2(f(m)) = Q_1(m)$$$

Lean4

@[simp]
theorem map_app (f : Q₁ →qᵢ Q₂) (m : M₁) : Q₂ (f m) = Q₁ m :=
  f.map_app' m

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

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

Разделы

Аффилиация

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