add_le_iff — Mathlib

English

For a, b, c in NatOrdinal, b + c ≤ a if and only if for all b' < b, b' + c < a and for all c' < c, b + c' < a.

Русский

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

LaTeX

$$$$ b + c \le a \iff \Big( \forall b' < b,\ b' + c < a \Big) \land \Big( \forall c' < c,\ b + c' < a \Big) $$$$

Lean4

theorem add_le_iff {a b c : NatOrdinal} : b + c ≤ a ↔ (∀ b' < b, b' + c < a) ∧ ∀ c' < c, b + c' < a :=
  Ordinal.nadd_le_iff

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