infsep_exists_of_nontrivial — Mathlib

English

If s is finite and nontrivial, then there exist x,y ∈ s, x ≠ y, with s.infsep = dist x y.

Русский

Если s конечное и не тривиальное, то существуют x,y ∈ s такие, что x ≠ y и s.infsep = dist(x,y).

LaTeX

$$$\exists x \in s, \exists y \in s, x \neq y \land s.infsep = dist(x,y)$$$

Lean4

theorem infsep_exists_of_nontrivial (hsf : s.Finite) (hs : s.Nontrivial) :
    ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y :=
  letI := hsf.fintype
  hs.infsep_exists_of_finite

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