nonempty_of_hausdorffEdist_ne_top

English

If the Hausdorff distance between s and t is finite, then either both are empty or both are nonempty.

Русский

Если расстояние Хаусдорфа между s и t конечное, то либо оба множества пустые, либо оба непустые.

LaTeX

$$$ \operatorname{hausdorffEdist}(s,t) \neq \infty \Rightarrow (s = \varnothing \land t = \varnothing) \lor (s \neq \varnothing \land t \neq \varnothing) $$$

Lean4

/-- If a set is at finite Hausdorff edistance of a nonempty set, it is nonempty. -/
theorem nonempty_of_hausdorffEdist_ne_top (hs : s.Nonempty) (fin : hausdorffEdist s t ≠ ⊤) : t.Nonempty :=
  t.eq_empty_or_nonempty.resolve_left fun ht ↦ fin (ht.symm ▸ hausdorffEdist_empty hs)

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