English
Let p be an extended nonnegative real number and V a type equipped with appropriate algebraic structure. The construction WithLp p V is canonically equivalent to V via the maps ofLp and toLp, which are mutual inverses. Consequently, WithLp p V is naturally isomorphic to V.
Русский
Пусть p — расширенное неотрицательное число, а V — множество с необходимой алгебраической структурой. Конструкция WithLp p V естественным образом изоморфна V через отображения ofLp и toLp, которые взаимно обратны. Следовательно, WithLp p V естественным образом изоморфно V.
LaTeX
$$$WithLp(p,V) \cong V$$$
Lean4
/-- `WithLp.ofLp` and `WithLp.toLp` as an equivalence. -/
@[simps]
protected def equiv : WithLp p V ≃ V where
toFun := ofLp
invFun := toLp p
left_inv _ := rfl
right_inv _ := rfl
