length_add_le — Mathlib

English

For intervals s,t in Interval(α), length(s + t) ≤ length(s) + length(t).

Русский

Для интервалов s,t в Interval(α) выполняется length(s + t) ≤ length(s) + length(t).

LaTeX

$$$ \operatorname{length}(s + t) \le \operatorname{length}(s) + \operatorname{length}(t) $$$

Lean4

theorem length_add_le : ∀ s t : Interval α, (s + t).length ≤ s.length + t.length
  | ⊥, _ => by simp
  | _, ⊥ => by simp
  | (s : NonemptyInterval α), (t : NonemptyInterval α) => (s.length_add t).le

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