copy — Mathlib

English

Copying a cocompact map with a new toFun function that is equal to the old one yields the same cocompact map.

Русский

Копирование коккомпактной карты с новой функцией-отображением, равной старой, даёт ту же карту.

LaTeX

$$$f.copy f' h = f$$$

Lean4

/-- Copy of a `CocompactMap` with a new `toFun` equal to the old one. Useful
to fix definitional equalities. -/
protected def copy (f : CocompactMap α β) (f' : α → β) (h : f' = f) : CocompactMap α β
    where
  toFun := f'
  continuous_toFun := by
    rw [h]
    exact f.continuous_toFun
  cocompact_tendsto' := by
    simp_rw [h]
    exact f.cocompact_tendsto'

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