copy_eq — Mathlib

English

The copy operation is definitional: applying the copy construction with the equality h recovers the original function.

Русский

Операция копирования разрешима лезть к определению: если h соответствует равенству, копирование возвращает исходную функцию.

LaTeX

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

Lean4

theorem copy_eq (f : A →ₗc[R] B) (f' : A → B) (h : f' = ⇑f) : f.copy f' h = f :=
  DFunLike.ext' h

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