infsep — Mathlib

English

For any set s, infsep(s) is defined as the real value corresponding to s.einfsep, i.e., infsep(s) = toReal(s.einfsep).

Русский

Для множества s инфsep определяется как действительное значение, соответствующее s.einfsep: infsep(s) = toReal(s.einfsep).

LaTeX

$$$ \mathrm{infsep}(s) = \operatorname{toReal}(s.einfsep) $$$

Lean4

/-- The "infimum separation" of a set with an edist function. -/
noncomputable def infsep [EDist α] (s : Set α) : ℝ :=
  ENNReal.toReal s.einfsep

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