relatively_discrete — Mathlib

English

If s is finite, there exists a positive constant C such that for all x,y in s with x ≠ y, the distance between x and y is at least C.

Русский

Пусть s конечно; существует C > 0, такой что для любых x,y ∈ s, x ≠ y, edist(x,y) ≥ C.

LaTeX

$$$ \exists C>0,\ \forall x\in s,\ \forall y\in s,\ x \neq y \rightarrow C \le edist x y $$$

Lean4

theorem relatively_discrete (hs : s.Finite) : ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y :=
  letI := hs.fintype
  relatively_discrete_of_finite

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