English
There is a linear isometry equivalence between affine maps and the product of the codomain with the space of linear maps, given by f ↦ (f(0), f.contLinear).
Русский
Существует линейное изометрическое эквивалентное отображение между аффинными отображениями и произведением кодомпозитора на пространство линейных отображений, задаваемое f ↦ (f(0), f.contLinear).
LaTeX
$$$$\text{toConstProdContinuousLinearMap} : (V \toᴬ[\mathbb{k}] W) \simeqₗᵢ (W × (V \toL[\mathbb{k}] W)).$$$$
Lean4
/-- The space of affine maps between two normed spaces is linearly isometric to the product of the
codomain with the space of linear maps, by taking the value of the affine map at `(0 : V)` and the
linear part. -/
noncomputable def toConstProdContinuousLinearMap : (V →ᴬ[𝕜] W) ≃ₗᵢ[𝕜] W × (V →L[𝕜] W)
where
toFun f := ⟨f 0, f.contLinear⟩
invFun p := p.2.toContinuousAffineMap + const 𝕜 V p.1
left_inv
f := by
ext
rw [f.decomp]
simp only [coe_add, ContinuousLinearMap.coe_toContinuousAffineMap, Pi.add_apply, coe_const]
right_inv := by rintro ⟨v, f⟩; ext <;> simp
map_add' _ _ := rfl
map_smul' _ _ := rfl
norm_map' _ := rfl
