empty_or_nonempty_of_hausdorffEdist_ne_top

English

If the two sets are not both empty, then both are nonempty when the finite Hausdorff distance to the other set is considered.

Русский

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

LaTeX

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

Lean4

theorem empty_or_nonempty_of_hausdorffEdist_ne_top (fin : hausdorffEdist s t ≠ ⊤) :
    (s = ∅ ∧ t = ∅) ∨ (s.Nonempty ∧ t.Nonempty) :=
  by
  rcases s.eq_empty_or_nonempty with hs | hs
  · rcases t.eq_empty_or_nonempty with ht | ht
    · exact Or.inl ⟨hs, ht⟩
    · rw [hausdorffEdist_comm] at fin
      exact Or.inr ⟨nonempty_of_hausdorffEdist_ne_top ht fin, ht⟩
  · exact Or.inr ⟨hs, nonempty_of_hausdorffEdist_ne_top hs fin⟩

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