length — Mathlib

English

The length of a nonempty interval is the difference between its right endpoint and its left endpoint.

Русский

Длина непустого интервала равна разности правого и левого концов интервала.

LaTeX

$$$ \operatorname{length}(s) = s.\mathrm{snd} - s.\mathrm{fst} $$$

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 : α :=
  s.snd - s.fst

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