relatively_discrete_of_finite — Mathlib

English

If s is finite, there exists a positive constant C > 0 such that for all distinct x,y ∈ s, C ≤ edist(x,y).

Русский

Пусть s конечно; тогда есть положительная константа C > 0 такая, что для любых различных x,y ∈ s выполняется C ≤ edist(x,y).

LaTeX

$$$ [Finite\ s] \Rightarrow \exists C>0, \forall x\in s, \forall y\in s, x\neq y \Rightarrow C \le edist(x,y) $$$

Lean4

theorem relatively_discrete_of_finite [Finite s] : ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y :=
  by
  rw [← einfsep_pos]
  exact einfsep_pos_of_finite

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