length — Mathlib

English

For an interval s in Interval(α), length is defined by length(⊥) = 0 and length(s) = s.length when s is a nonempty interval.

Русский

Для интервала s в Interval(α) определяем length(⊥) = 0 и length(s) = s.length, если s — непустой интервал.

LaTeX

$$$ \operatorname{length}(\perp) = 0 \quad\text{and}\quad \operatorname{length}(s) = s.length \text{ for } s \in \text{NonemptyInterval}(\alpha) $$$

Lean4

/-- The length of an interval is its first component minus its second component. This measures the
accuracy of the approximation by an interval. -/
def length : Interval α → α
  | ⊥ => 0
  | (s : NonemptyInterval α) => s.length

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