le_infsep — Mathlib

English

If s.Nontrivial and a bound holds for all pairwise distances, then that bound is a lower bound for s.infsep.

Русский

Если s не тривиально и для всех пар элементов верно, что d ≤ dist x y, то d ≤ s.infsep.

LaTeX

$$$ s.Nontrivial \rightarrow (\forall x \in s, \forall y \in s, x \neq y \rightarrow d \le dist x y) \rightarrow d \le s.infsep $$$

Lean4

theorem le_infsep {d} (hs : s.Nontrivial) (h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y) : d ≤ s.infsep :=
  hs.le_infsep_iff.2 h

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