English
For hp: 0 < f(0), and o1 ≤ o2, we have veblenWith(f,o1,a) < veblenWith(f,o2,b) iff a < veblenWith(f,o2,b) or related cases depending on o1,o2.
Русский
При hp: 0 < f(0) и o1 ≤ o2 выполняется неразрывное условие: veblenWith(f,o1,a) < veblenWith(f,o2,b) эквивалентно a < veblenWith(f,o2,b) или другим разбором по o1,o2.
LaTeX
$$$\forall f:\,\operatorname{Ordinal} \to \operatorname{Ordinal},\ \operatorname{IsNormal}(f)\Rightarrow\ \forall o1,o2,a,b:\operatorname{Ordinal},\ hp:\, 0 < f(0) \Rightarrow \ \operatorname{veblenWith}(f,o1,a) < \operatorname{veblenWith}(f,o2,b) \iff \text{(case split as in definition)}}$$$
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_lt_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_lt_iff, cmp_veblenWith hf]
aesop (add simp lt_asymm)
