isClosed_of_pairwise_le_dist — Mathlib

English

If a subset s has pairwise distances bounded below by a positive ε, then s is closed in the ambient metric space.

Русский

Если для множества s расстояния между любыми двумя различными точками по меньшей мере ε>0, то s замкнуто в пространстве.

LaTeX

$$$ hε>0,\; s.Pairewise(\ x y \mapsto ε \le dist(x,y)) \Rightarrow IsClosed(s) $$$

Lean4

theorem isClosed_of_pairwise_le_dist {s : Set γ} {ε : ℝ} (hε : 0 < ε) (hs : s.Pairwise fun x y => ε ≤ dist x y) :
    IsClosed s :=
  isClosed_of_spaced_out (dist_mem_uniformity hε) <| by simpa using hs

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