hausdorffEdist_ne_top — Mathlib

English

For convex bodies K,L in a normed space, the Hausdorff distance between their underlying sets is finite.

Русский

Для выпуклых тел K,L в нормированном пространстве расстояние Хаусдорфа между их базовыми множествами конечное.

LaTeX

$$$\\mathrm{hausdorffEdist}((K:\\,\\mathrm{Set}V),L) < \\infty.$$$

Lean4

theorem hausdorffEdist_ne_top {K L : ConvexBody V} : EMetric.hausdorffEdist (K : Set V) L ≠ ⊤ := by
  apply_rules [Metric.hausdorffEdist_ne_top_of_nonempty_of_bounded, ConvexBody.nonempty, ConvexBody.isBounded]

Похожие утверждения