English
If hp: 0 < f(0), then veblenWith(f, o1, 0) = veblenWith(f, o2, 0) iff o1 = o2.
Русский
Если 0 < f(0), тогда veblenWith(f, o1, 0) = veblenWith(f, o2, 0) эквивалентно o1 = o2.
LaTeX
$$$\forall f:\,\operatorname{Ordinal} \to \operatorname{Ordinal},\ \operatorname{IsNormal}(f)\Rightarrow (0 < f(0)) \Rightarrow (\operatorname{veblenWith}(f,o1,0) = \operatorname{veblenWith}(f,o2,0) \iff o1 = o2)$$$
Lean4
/-- `veblenWith f o₁ a = veblenWith f o₂ b` iff one of the following holds:
* `o₁ = o₂` and `a = b`
* `o₁ < o₂` and `a = veblenWith f o₂ b`
* `o₁ > o₂` and `veblenWith f o₁ a = b` -/
theorem veblenWith_eq_veblenWith_iff :
veblenWith f o₁ a = veblenWith f o₂ b ↔
o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a = b :=
by
rw [← cmp_eq_eq_iff, cmp_veblenWith hf]
aesop (add simp lt_asymm)
