toIsometry

Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

URI: https://scilib.ai/kg/mathlib#QuadraticMap.IsometryEquiv.toIsometry

English

Isometric equivalences are isometric maps.

Русский

Изометрические эквивалентности являются изометрическими отображениями.

LaTeX

$$$\mathrm{toIsometry}(g) : Q_1 \to qᵢ Q_2$$$

Lean4

/-- Isometric equivalences are isometric maps -/
@[simps]
def toIsometry (g : Q₁.IsometryEquiv Q₂) : Q₁ →qᵢ Q₂
    where
  toFun x := g x
  __ := g

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

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

Разделы

Аффилиация

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