Theorem PiLp.nndist_apply_le

Modification history

2025-04-27 05:05
Mathlib/Analysis/Normed/Lp/PiLp.lean
feat: `‖x i‖ ≤ ‖x‖` for PiLp (#24402)
Added PiLp.nndist_apply_leView on Github →