decomp' — Mathlib

English

The linear part of an affine map f equals f minus the constant map that returns f(0): f.linear = f − (fun _ => f(0)).

Русский

Линейная часть отображения f равна f минус константное отображение, отдающее f(0): f.linear = f − c, где c(x) = f(0).

LaTeX

$$$ f.linear = f - (\\lambda x. f(0)) $$$

Lean4

/-- Decomposition of an affine map in the special case when the point space and vector space
are the same. -/
theorem decomp' (f : V1 →ᵃ[k] V2) : (f.linear : V1 → V2) = ⇑f - fun _ => f 0 :=
  by
  rw [decomp]
  simp only [LinearMap.map_zero, Pi.add_apply, add_sub_cancel_right, zero_add]

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