English
Let a,b,c,d be ordinals. Then d < a ⊗ (b ⊗ c) holds iff there exist a' < a, b' < b, c' < c with d ⊞ (a' ⊗ (b' ⊗ c)) ⊞ (a' ⊗ (b ⊗ c')) ⊞ (a ⊗ (b' ⊗ c')) ≤ a' ⊗ (b ⊗ c) ⊞ a ⊗ (b' ⊗ c) ⊞ a ⊗ (b ⊗ c') ⊞ a' ⊗ (b' ⊗ c')
Русский
Пусть a,b,c,d — ординалы. Тогда d < a ⊗ (b ⊗ c) эквивалентно существованию a'<a, b'<b, c'<c, таких что неравенство с Hessenberg-сложением и обычными тандемами выполняется.
LaTeX
$$$d < a \otimes (b \otimes c) \iff \exists a' < a, \exists b' < b, \exists c' < c, d \boxplus (a' \otimes (b' \otimes c)) \boxplus (a' \otimes (b \otimes c')) \boxplus (a \otimes (b' \otimes c')) \le a' \otimes (b \otimes c) \boxplus a \otimes (b' \otimes c) \boxplus a \otimes (b \otimes c') \boxplus a' \otimes (b' \otimes c')$$$
Lean4
@[deprecated lt_nmul_iff₃ (since := "2024-11-19")]
theorem lt_nmul_iff₃' :
d < a ⨳ (b ⨳ c) ↔
∃ a' < a,
∃ b' < b,
∃ c' < c,
d ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c') ≤
a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') :=
by simpa using nmul_le_iff₃'.not
