infsep_of_nontrivial — Mathlib

English

If s is finite and nontrivial, then s.infsep equals the minimum distance between two distinct points of s; i.e., there exist x,y ∈ s with x ≠ y such that s.infsep = dist(x,y).

Русский

Если S — конечное множество и не тривиально, то s.infsep равно минимальному расстоянию между двумя различными точками множества; т.е. существуют x,y ∈ s такие, что x ≠ y и s.infsep = dist(x,y).

LaTeX

$$$\displaystyle \text{If } s \text{ is finite and nontrivial, then } s.infsep = \min_{x,y \in s,\ x \neq y} \operatorname{dist}(x,y).$$$

Lean4

theorem infsep_of_nontrivial (hsf : s.Finite) (hs : s.Nontrivial) :
    s.infsep = hsf.offDiag.toFinset.inf' (by simpa) (uncurry dist) := by classical simp_rw [hsf.infsep, dif_pos hs]

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