copy — Mathlib

English

Copy of a ContinuousMap f with a new underlying function f' and a witness h: f' = f; the resulting map has toFun = f'.

Русский

Копия непрерывной карты f с новым основанным на f' основанием и доказательством h: f' = f; полученная карта имеет toFun = f'.

LaTeX

$$copy (f) (f') (h) : C(X,Y)$$

Lean4

/-- Copy of a `ContinuousMap` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (f : C(X, Y)) (f' : X → Y) (h : f' = f) : C(X, Y)
    where
  toFun := f'
  continuous_toFun := h.symm ▸ f.continuous_toFun

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