Theorem WithLp.equiv_sub

Modification history

2023-08-14 01:22
Mathlib/Analysis/NormedSpace/WithLp.lean
refactor: generalize PiLp to WithLp (#6409) …
Added WithLp.equiv_subView on Github →