veblenWith_zero_le_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) \le \operatorname{veblenWith}(f,o2,0) \iff o1 \le o2)$$$

Lean4

theorem veblenWith_zero_le_veblenWith_zero (hp : 0 < f 0) : veblenWith f o₁ 0 ≤ veblenWith f o₂ 0 ↔ o₁ ≤ o₂ :=
  (veblenWith_zero_strictMono hf hp).le_iff_le

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