copy_eq

Mathlib.Topology.ContinuousMap.CompactlySupported

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

English

For f ∈ C_c(α, β) and any f' with h showing f' = f, the equality f.copy f' h = f holds.

Русский

Для f ∈ C_c(α, β) и любого f' с доказательством h, что f'=f, выполняется равенство f.copy f' h = f.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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