le_infsep_iff — Mathlib

English

If s is Nontrivial, then d ≤ s.infsep iff ∀ x∈s, ∀ y∈s, x≠y → d ≤ dist x y.

Русский

Если s не тривиально, тогда d ≤ s.infsep эквивалентно ∀ x∈s, ∀ y∈s, x≠y → d ≤ dist x y.

LaTeX

$$$ d \le s.infsep \iff \forall x \in s,\ \forall y \in s,\ x \neq y \rightarrow d \le dist x y $$$

Lean4

theorem le_infsep_iff {d} (hs : s.Nontrivial) : d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y := by
  simp_rw [infsep, ← ENNReal.ofReal_le_iff_le_toReal hs.einfsep_ne_top, le_einfsep_iff, edist_dist,
    ENNReal.ofReal_le_ofReal_iff dist_nonneg]

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