English
The set of candidate distance functions on X ⊕ Y is defined by natural axioms: symmetry, triangle inequality, alignment with original distances on X and on Y, etc.
Русский
Множество кандидатов на функции расстояний на X ⊕ Y определяется аксиомами: симметрия, треугольное неравенство, соответствие исходным расстояниям на X и на Y и т.д.
LaTeX
$$$\text{candidates} : \{f: ProdSpaceFun X Y\} \;|\; \text{(properties as in definition)}\,$$$
Lean4
/-- The set of functions on `X ⊕ Y` that are candidates distances to realize the
minimum of the Hausdorff distances between `X` and `Y` in a coupling. -/
def candidates : Set (ProdSpaceFun X Y) :=
{f |
(((((∀ x y : X, f (Sum.inl x, Sum.inl y) = dist x y) ∧ ∀ x y : Y, f (Sum.inr x, Sum.inr y) = dist x y) ∧
∀ x y, f (x, y) = f (y, x)) ∧
∀ x y z, f (x, z) ≤ f (x, y) + f (y, z)) ∧
∀ x, f (x, x) = 0) ∧
∀ x y, f (x, y) ≤ maxVar X Y}
