einfsep_pos_of_finite — Mathlib

English

Same as the previous statement, with real distance bound: if d ≤ dist(x,y) for all distinct x,y∈s, then ofReal(d) ≤ s.einfsep.

Русский

Аналогично, если d ≤ dist(x,y) для всех различных x,y∈s, то ofReal(d) ≤ einfsep(s).

LaTeX

$$$ \left( \forall x \in s, \forall y \in s, x \neq y \Rightarrow d \le dist(x,y) \right) \Rightarrow \operatorname{ofReal}(d) \le s.einfsep $$$

Lean4

theorem einfsep_pos_of_finite [Finite s] : 0 < s.einfsep :=
  by
  cases nonempty_fintype s
  by_cases hs : s.Nontrivial
  · rcases hs.einfsep_exists_of_finite with ⟨x, _hx, y, _hy, hxy, hxy'⟩
    exact hxy'.symm ▸ edist_pos.2 hxy
  · rw [not_nontrivial_iff] at hs
    exact hs.einfsep.symm ▸ WithTop.top_pos

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