copy_eq — Mathlib

English

If h expresses that f' equals the underlying function of f, then f.copy f' h equals f.

Русский

Если условие h устанавливает равенство f' и функции f, то копия f копирует обратно в f.

LaTeX

$$$\forall f:\mathrm{PseudoEpimorphism}(\alpha,\beta),\forall f':\alpha\to\beta,\forall h:\,f' = f,\ f.copy\, f'\, h = f$$$

Lean4

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

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