copy — Mathlib

English

Copy of a ContDiffMapSupportedIn with a new toFun equal to the old one; the rest of the structure is transported accordingly.

Русский

Копия ContDiffMapSupportedIn с новой функцией-основанием, равной старой; остальная структура переносится соответствующим образом.

LaTeX

$$$ \exists f', h:\, f' = f \Rightarrow f.copy f' h \text{ has underlying function } f' $$$

Lean4

/-- Copy of a `ContDiffMapSupportedIn` with a new `toFun` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (f : 𝓓^{n}_{K}(E, F)) (f' : E → F) (h : f' = f) : 𝓓^{n}_{K}(E, F)
    where
  toFun := f'
  contDiff' := h.symm ▸ f.contDiff
  zero_on_compl' := h.symm ▸ f.zero_on_compl

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