unpair_add_le — Mathlib

English

Sum of the components of unpair(n) does not exceed n, i.e., (unpair n).1 + (unpair n).2 ≤ n.

Русский

Сумма компонент распаковки не превосходит n: fst(unpair(n)) + snd(unpair(n)) ≤ n.

LaTeX

$$$ \forall n \in \mathbb{N},\; \operatorname{fst}(\operatorname{unpair}(n)) + \operatorname{snd}(\operatorname{unpair}(n)) \le n. $$$

Lean4

theorem unpair_add_le (n : ℕ) : (unpair n).1 + (unpair n).2 ≤ n :=
  (add_le_pair _ _).trans_eq (pair_unpair _)

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