Triangle Inequality

Let ( X , ≀ ) 𝑋 (X,\leq) be a Preorder, ( V , ⋆ ) 𝑉 ⋆ (V,\star) be a Magma, and D : X β†’ X β†’ V β†’ Ξ© : 𝐷 β†’ 𝑋 𝑋 β†’ 𝑉 β†’ Ξ© D:X\to X\to V\to\Omega some relation.

We say that D 𝐷 D satisfies the triangle inequality with respect to ⋆ ⋆ \star if for all x , y , z : X : π‘₯ 𝑦 𝑧 𝑋 x,y,z:X and d x ⁒ y , d y ⁒ z : V : subscript 𝑑 π‘₯ 𝑦 subscript 𝑑 𝑦 𝑧 𝑉 d_{xy},d_{yz}:V

Typically, this is phrased in terms of a function d : X β†’ X β†’ V : 𝑑 β†’ 𝑋 𝑋 β†’ 𝑉 d:X\to X\to V where d ⁒ ( x , z ) ≀ d ⁒ ( x , y ) + d ⁒ ( y , z ) 𝑑 π‘₯ 𝑧 𝑑 π‘₯ 𝑦 𝑑 𝑦 𝑧 d(x,z)\leq d(x,y)+d(y,z) , but this definition does not work as well in Constructive Mathematics. This distinction basically boils down to if we wish to work with a Locally Graded Category or an Enriched Category.

This formulation also shows up in the definition of a Richman Premetric Space.

References