English
Let p be a real nonnegative extended value and V a vector space over a field K. The canonical linear equivalence between WithLp p V and V has an inverse that commutes with scalar multiplication; i.e., for any scalar c in K and any x′ in V, the inverse image of c·x′ equals c times the inverse image of x′.
Русский
Пусть p — элемент множества неотрицательных расширенных чисел, и V — векторное пространство над полем K. Каноническое линейное эквивалентное отображение между WithLp p V и V имеет обратное отображение, сохраняющее скаляры: для любого скаляра c ∈ K и любого x′ ∈ V выполняется (WithLp.equiv p V)^{-1}(c·x′) = c·(WithLp.equiv p V)^{-1}(x′).
LaTeX
$$$$ \bigl(\varphi_p\bigr)^{-1}(c\,x) = c\,\bigl(\varphi_p\bigr)^{-1}(x) , $$$$
Lean4
@[deprecated toLp_smul (since := "2025-06-08")]
theorem equiv_symm_smul [SMul K V] (c : K) (x' : V) :
(WithLp.equiv p V).symm (c • x') = c • (WithLp.equiv p V).symm x' :=
rfl
