English
Let a,b,c,d be ordinals. Then a ⊗ b ⊗ c ≤ d if and only if for all a' < a, for all b' < b, for all c' < c, a' ⊗ b ⊗ c ⊞ a ⊗ b' ⊗ c ⊞ a ⊗ b ⊗ c' ⊞ a' ⊗ b' ⊗ c' < d ⊞ a' ⊗ b' ⊗ c ⊞ a' ⊗ b ⊗ c' ⊞ a ⊗ b' ⊗ c'
Русский
Пусть a,b,c,d — ординалы. Тогда a ⊗ b ⊗ c ≤ d эквивалентно тому, что для всех a'<a, b'<b, c'<c выполняется неравенство, содержащее хаусербергово-сложение и обычное умножение на соответствующих позициях.
LaTeX
$$$a \otimes b \otimes c \le d \iff \forall a' < a, \forall b' < b, \forall c' < c, a' \otimes b \otimes c \boxplus a \otimes b' \otimes c \boxplus a \otimes b \otimes c' \boxplus a' \otimes b' \otimes c' < d \boxplus a' \otimes b' \otimes c \boxplus a' \otimes b \otimes c' \boxplus a \otimes b' \otimes c' }$$
Lean4
theorem nmul_le_iff₃ :
a ⨳ b ⨳ c ≤ d ↔
∀ a' < a,
∀ b' < b,
∀ c' < c, a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < d ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' :=
by simpa using lt_nmul_iff₃.not
