Norm Le Vec Euclidean

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.pi_norm_le_vecEuclideanNorm {d : ℕ} (x : Vec d) : ‖x‖ ≤ vecEuclideanNorm x

The sup norm of a vector of Vec d is at most its Euclidean norm.