toContinuousAffineMap_map_zero — Mathlib

English

Every continuous linear map can be regarded as a continuous affine map, with the linear part equal to itself and a trivial affine structure.

Русский

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

LaTeX

$$$$f: V \\to L[R] W \\implies f\\;\\text{as a ContinuousAffineMap}$$$$

Lean4

@[simp]
theorem toContinuousAffineMap_map_zero (f : V →L[R] W) : f.toContinuousAffineMap 0 = 0 := by simp

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