decomp — Mathlib

English

Every affine map f: V1 →ᵃ[k] V2 can be written as its linear part plus the constant map sending every input to f(0): f(x) = f.linear(x) + f(0).

Русский

Любая аффинная карта f: V1 →ᵃ[k] V2 раскладывается как её линейная часть плюс константная карта: f(x) = f.linear(x) + f(0).

LaTeX

$$$ f(x) = f.linear(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 : V1 → V2) = ⇑f.linear + fun _ => f 0 :=
  by
  ext x
  calc
    f x = f.linear x +ᵥ f 0 := by rw [← f.map_vadd, vadd_eq_add, add_zero]
    _ = (f.linear + fun _ : V1 => f 0) x := rfl

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