English
From a candidate function f ∈ candidates, construct a bounded continuous function on X ⊕ Y via a compactness trick (mkOfCompact).
Русский
Из функции-кандидата f ∈ candidates конструируем ограниченную непрерывную функцию на X ⊕ Y через компактный приём (mkOfCompact).
LaTeX
$$def candidatesBOfCandidates (f : ProdSpaceFun X Y) (fA : f ∈ candidates X Y) : Cb X Y := BoundedContinuousFunction.mkOfCompact ⟨f, (candidates_lipschitz fA).continuous⟩$$
Lean4
/-- We will then choose the candidate minimizing the Hausdorff distance. Except that we are not
in a metric space setting, so we need to define our custom version of Hausdorff distance,
called `HD`, and prove its basic properties. -/
def HD (f : Cb X Y) :=
max (⨆ x, ⨅ y, f (inl x, inr y))
(⨆ y, ⨅ x, f (inl x, inr y))
/- We will show that `HD` is continuous on `BoundedContinuousFunction`s, to deduce that its
minimum on the compact set `candidatesB` is attained. Since it is defined in terms of
infimum and supremum on `ℝ`, which is only conditionally complete, we will need all the time
to check that the defining sets are bounded below or above. This is done in the next few
technical lemmas. -/
