copy_eq

Mathlib.Analysis.Distribution.ContDiffMapSupportedIn

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

English

The copy operation yields an object whose underlying function is f'.

Русский

Операция копирования создаёт объект, чья базовая функция равна f'.

LaTeX

$$$ toFun (f.copy f' h) = f' $$$

Lean4

theorem copy_eq (f : 𝓓^{n}_{K}(E, F)) (f' : E → F) (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

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

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

Разделы

Аффилиация

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