English
The statement gives a tri-branch decomposition of veblen o1 a < veblen o2 b depending on the relative order of o1 and o2.
Русский
Выравнивание неравенства veblen o1 a < veblen o2 b разбивается на три случая в зависимости от отношения o1 и o2.
LaTeX
$$$$\\operatorname{veblen}(o_1,a) < \\operatorname{veblen}(o_2,b) \\\\ \\iff \\\\ o_1 = o_2 ∧ a < b \\\\ ∨ \\\\ o_1 < o_2 ∧ a < \\operatorname{veblen}(o_2,b) \\\\ ∨ \\\\ o_2 < o_1 ∧ \\operatorname{veblen}(o_1,a) < b.$$$$
Lean4
/-- `veblen o₁ a < veblen o₂ b` iff one of the following holds:
* `o₁ = o₂` and `a < b`
* `o₁ < o₂` and `a < veblen o₂ b`
* `o₁ > o₂` and `veblen o₁ a < b` -/
theorem veblen_lt_veblen_iff :
veblen o₁ a < veblen o₂ b ↔ o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblen o₂ b ∨ o₂ < o₁ ∧ veblen o₁ a < b :=
veblenWith_lt_veblenWith_iff (isNormal_opow one_lt_omega0)
