ext

Mathlib.LinearAlgebra.QuadraticForm.Isometry

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

English

The ext lemma for Isometry maps says two Isometries are equal if they agree on all inputs.

Русский

Лемма экстенсионности для изометрий: две изометрии равны, если они совпадают на всех входах.

LaTeX

$$Isometry.ext : ∀ {f g : Q1 →qᵢ Q2}, (∀ x, f x = g x) → f = g$$

Lean4

@[ext]
theorem ext ⦃f g : Q₁ →qᵢ Q₂⦄ (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext _ _ h

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

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

Разделы

Аффилиация

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