einfsep — Mathlib

English

If s is a Subsingleton, then its extended infimum separation is infinite: s.einfsep = ∞.

Русский

Если множество s сведено до одного элемента или пусто, то его расширенная инфиминальная разделённость бесконечна: s.einfsep = ∞.

LaTeX

$$$\text{If } s \text{ is Subsingleton, then } s.einfsep = \infty.$$$

Lean4

/-- The "extended infimum separation" of a set with an edist function. -/
noncomputable def einfsep [EDist α] (s : Set α) : ℝ≥0∞ :=
  ⨅ (x ∈ s) (y ∈ s) (_ : x ≠ y), edist x y

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