einfsep_exists_of_finite — Mathlib

English

If s is finite and nonempty, there exist x,y ∈ s with x ≠ y such that einfsep(s) = edist(x,y).

Русский

При конечности и не пустоте множества найдутся x,y ∈ s, x ≠ y, для которых einfsep(s) = edist(x,y).

LaTeX

$$$ \exists x \in s, \exists y \in s, x \neq y \wedge s.einfsep = \operatorname{edist}(x,y) $$$

Lean4

theorem einfsep_exists_of_finite [Finite s] (hs : s.Nontrivial) : ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y := by
  classical
  cases nonempty_fintype s
  simp_rw [einfsep_of_fintype]
  rcases Finset.exists_mem_eq_inf s.offDiag.toFinset (by simpa) (uncurry edist) with ⟨w, hxy, hed⟩
  simp_rw [mem_toFinset] at hxy
  exact ⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩

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