coe_copy — Mathlib

English

If f' equals the underlying function of f, then the coerced copy has the same underlying function: coe (f.copy f' h) = f'.

Русский

Если f' равна базовой функции f, то коэрцированный аналог копии имеет ту же базовую функцию: coe (f.copy f' h) = f'.

LaTeX

$$$\\mathrm{coe\\_copy}(f,f',h):\\; \\; (f.copy f' h)^{\\#} = f'$$$

Lean4

@[simp]
theorem coe_copy (f : C(X, Y)) (f' : X → Y) (h : f' = f) : ⇑(f.copy f' h) = f' :=
  rfl

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