AreSeparated — Mathlib

English

If s is ε-separated from t, then s is contained in the complement of t.

Русский

Если s ε-разделено от t,то s ⊆ tᶜ.

LaTeX

$$$\\operatorname{subset\_compl\_right}(h) : s \\subseteq t^{\\complement}$$$

Lean4

/-- Two sets in an (extended) metric space are called *metric separated* if the (extended) distance
between `x ∈ s` and `y ∈ t` is bounded from below by a positive constant. -/
def AreSeparated (s t : Set X) :=
  ∃ r, r ≠ 0 ∧ ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y

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