le_einfsep_of_forall_dist_le — Mathlib

English

If every pair of distinct points in s has distance at least d, then ofReal(d) ≤ einfsep(s).

Русский

Если для всех различных x,y∈s выполняется d ≤ dist(x,y), то 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 le_einfsep_of_forall_dist_le {d} (h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y) : ENNReal.ofReal d ≤ s.einfsep :=
  le_einfsep fun x hx y hy hxy => (edist_dist x y).symm ▸ ENNReal.ofReal_le_ofReal (h x hx y hy hxy)

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