copy — Mathlib

English

Copying a vanishing-at-infinity map by replacing its underlying function with an equal function yields a new map that is equal to the old one.

Русский

Копирование отображения с vanish-at-infinity путём замены базовой функции на равную даёт новую карту, равную исходной.

LaTeX

$$$ f.copy\, f'\, h \;: C_0(\alpha, \beta) $$$

Lean4

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

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