copy_eq — Mathlib

English

Let Q be a quadratic map R → M → N and let Q' be a map M → N with h the proof that Q' equals the underlying function of Q. Then Q.copy Q' h equals Q. In words, copying a quadratic map along its own underlying function yields the original map.

Русский

Пусть Q — квадратичная карта R → M → N и Q' — функция M → N такая, что существует доказательство h равенства Q' и соответствующей функции Q. Тогда Q.copy Q' h = Q. Иными словами, копирование по собственной функции даёт исходную карту.

LaTeX

$$$Q.copy Q' h = Q$$$

Lean4

theorem copy_eq (Q : QuadraticMap R M N) (Q' : M → N) (h : Q' = ⇑Q) : Q.copy Q' h = Q :=
  DFunLike.ext' h

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