English
For all o1,o2,a,b, the equality veBl en o1 a = veBl en o2 b holds iff one of three cases holds: o1=o2 ∧ a=b, or o1<o2 ∧ a=veblen o2 b, or o2<o1 ∧ veblen o1 a = b.
Русский
Для любых o1,o2,a,b верно равенство veblen o1 a = veblen o2 b тогда и только тогда, когда выполняется одно из трёх условий: o1=o2 и a=b; или o1<o2 и a=veblen o2 b; или o2<o1 и veblen o1 a = b.
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_eq_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_eq_veblenWith_iff (isNormal_opow one_lt_omega0)
