Mathlib v3 is deprecated. Go to Mathlib v4

Theorem pi_Lp.continuous_equiv

Modification history

2023-02-08 20:27
src/analysis/normed_space/pi_Lp.lean
chore(analysis/normed_space/pi_Lp): pi_Lp.equiv is continuous (#18402) …
Added pi_Lp.continuous_equivView on Github →