Off Centre Inclusion

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

theorem CKN.Foundation.Parabolic.vec3EuclideanNorm_sub_le_add_sub (x y z : Vec3) : vec3EuclideanNorm (x - z) ≤ vec3EuclideanNorm (x - y) + vec3EuclideanNorm (y - z)

The Euclidean norm on Vec3 satisfies the triangle inequality for three points: |x - z| ≤ |x - y| + |y - z|.