copy — Mathlib

English

Copying a continuous linear map with a new function equal to the old one yields a map equal to the original.

Русский

Копирование непрерывного линейного отображения в новое отображение с тем же графом даёт отображение, равное исходному.

LaTeX

$$$f.copy\; f'\; h = f$ when $h$ asserts $f'=f$$$

Lean4

/-- Copy of a `ContinuousLinearMap` with a new `toFun` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂) (h : f' = ⇑f) : M₁ →SL[σ₁₂] M₂
    where
  toLinearMap := f.toLinearMap.copy f' h
  cont := show Continuous f' from h.symm ▸ f.continuous

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