einfsep_pos — Mathlib

English

The extended infimum separation is strictly positive iff there is a positive lower bound on distances between distinct points in s.

Русский

Расширенная инфиминальная разделённость строго положительна тогда и только тогда, когда существуют положительная нижняя граница расстояний между различными точками множества s.

LaTeX

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

Lean4

theorem einfsep_pos : 0 < s.einfsep ↔ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y :=
  by
  rw [pos_iff_ne_zero, Ne, einfsep_zero]
  simp only [not_forall, not_exists, not_lt, exists_prop, not_and]

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