length_nonneg

Mathlib.Algebra.Order.Interval.Basic

URI: https://scilib.ai/kg/mathlib#Interval.length_nonneg

English

For every interval s, length(s) ≥ 0.

Русский

Для любого интервала s длина неотрицательна.

LaTeX

$$$ 0 \le \operatorname{length}(s) $$$

Lean4

@[simp]
theorem length_nonneg : ∀ s : Interval α, 0 ≤ s.length
  | ⊥ => le_rfl
  | (s : NonemptyInterval α) => s.length_nonneg

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru