lt_nadd_iff — Mathlib

English

Characterization of order with natural addition: a < b ⊞ c iff either there exists b' < b with a ≤ b' ⊞ c or there exists c' < c with a ≤ b ⊞ c'.

Русский

Характеризация порядка через натуральное сложение: 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_nadd_iff : a < b ♯ c ↔ (∃ b' < b, a ≤ b' ♯ c) ∨ ∃ c' < c, a ≤ b ♯ c' :=
  by
  rw [nadd]
  simp [Ordinal.lt_iSup_iff]

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