einfsep_exists_of_nontrivial — Mathlib

English

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

Русский

Если s конечно и неtrivial, существуют x,y ∈ s такие, что x ≠ y и einfsep(s) = edist(x,y).

LaTeX

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

Lean4

theorem einfsep_exists_of_nontrivial (hsf : s.Finite) (hs : s.Nontrivial) :
    ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y :=
  letI := hsf.fintype
  hs.einfsep_exists_of_finite

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