copy_eq

Mathlib.Topology.Spectral.Hom

URI: https://scilib.ai/kg/mathlib#SpectralMap.copy_eq

English

If the new function equals the old one, then the copy equals the original map.

Русский

Если новая функция равна старой, копия равна исходному отображению.

LaTeX

$$$ f.copy f' h = f. $$$

Lean4

theorem copy_eq (f : SpectralMap α β) (f' : α → β) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

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

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

Разделы

Аффилиация

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