infsep_exists_of_finite — Mathlib

English

If s is finite and nontrivial, there exist x ∈ s and y ∈ s with x ≠ y and 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_finite [Finite s] (hs : s.Nontrivial) : ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y := by
  classical
  cases nonempty_fintype s
  simp_rw [hs.infsep_of_fintype]
  rcases Finset.exists_mem_eq_inf' (s := s.offDiag.toFinset) (by simpa) (uncurry dist) with ⟨w, hxy, hed⟩
  simp_rw [mem_toFinset] at hxy
  exact ⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩

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