lt_add_iff — Mathlib

English

Let a, b, c be NatOrdinal. Then a is less than b + c if and only if either there exists b' < b with a ≤ b' + c, or there exists c' < c with a ≤ b + c'.

Русский

Пусть a, b, c — NatOrdinal. Тогда a < b + c тогда и только тогда, когда либо существует b' < b такое, что a ≤ b' + c, либо существует c' < c такое, что a ≤ b + c'.

LaTeX

$$$$ a < b + c \iff (\exists b' < b, a \le b' + c) \lor \exists c' < c, a \le b + c' $$$$

Lean4

theorem lt_add_iff {a b c : NatOrdinal} : a < b + c ↔ (∃ b' < b, a ≤ b' + c) ∨ ∃ c' < c, a ≤ b + c' :=
  Ordinal.lt_nadd_iff

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