Theorem PiLp.antilipschitzWith_equiv_aux

Modification history

2023-05-26 22:04

Mathlib/Analysis/NormedSpace/PiLp.lean

feat: port Analysis.NormedSpace.PiLp (#4345)

Added PiLp.antilipschitzWith_equiv_aux View on Github →