length — Mathlib

English

The length function measures intervals by the infimum of differences f(b)−f(a) over all containing intervals.

Русский

Длина интервала определяется как наименьшее возможное значение f(b)−f(a) для интервалов, содержащих срез.

LaTeX

$$$$ \\text{length }(s) = \\inf_{a,b: s\\subset Ioc(a,b)} \\; \\mathrm{ofReal}(f(b) - f(a)). $$$$

Lean4

/-- Length of an interval. This is the largest monotone function which correctly measures all
intervals. -/
def length (s : Set ℝ) : ℝ≥0∞ :=
  ⨅ (a) (b) (_ : s ⊆ Ioc a b), ofReal (f b - f a)

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