pi_Lp): pi_Lp.equiv is continuous (#18402)

Commit

2 years ago

chore(analysis/normed_space/pi_Lp): pi_Lp.equiv is continuous (#18402) The main benefit here is that this should now work with the continuity tactic.

Author

eric-wieser

Parents