copy_eq_self

Mathlib.Topology.MetricSpace.Dilation

URI: https://scilib.ai/kg/mathlib#Dilation.copy_eq_self

English

If you copy a dilation f along the same underlying function f', with h = f' = f, you get back f.

Русский

Если копировать дилатацию f по той же самой функции f' и h = f' = f, то получаем обратно f.

LaTeX

$$$f' = f \Rightarrow f.copy f' h = f$$$

Lean4

theorem copy_eq_self (f : α →ᵈ β) {f' : α → β} (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

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

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

Разделы

Аффилиация

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