decomp — Mathlib

English

Every continuous affine map f: V →ᴬ[R] W decomposes as a sum of its linear part and a constant function: (f : V → W) = f.contLinear + constant(f(0)).

Русский

Любое непрерывное аффинное отображение f: V →ᴬ[R] W раскладывается как сумма своей линейной части и константной функции: (f : V → W) = f.contLinear + константное( f(0) ).

LaTeX

$$$$f = f.contLinear + \\text{const}(f(0)).$$$$

Lean4

theorem _root_.ContinuousAffineMap.decomp (f : V →ᴬ[R] W) : (f : V → W) = f.contLinear + Function.const V (f 0) :=
  by
  rcases f with ⟨f, h⟩
  rw [ContinuousAffineMap.coe_mk_contLinear_eq_linear, ContinuousAffineMap.coe_mk, f.decomp, Pi.add_apply,
    LinearMap.map_zero, zero_add, ← Function.const_def]

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