veblenWith_zero_lt_veblenWith_zero

English

If 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

theorem veblenWith_zero_lt_veblenWith_zero (hp : 0 < f 0) : veblenWith f o₁ 0 < veblenWith f o₂ 0 ↔ o₁ < o₂ :=
  (veblenWith_zero_strictMono hf hp).lt_iff_lt

Похожие утверждения