left_le_veblenWith — Mathlib

English

For hp: 0 < f(0) and any o,a, o ≤ veblenWith(f, o, a).

Русский

При hp: 0 < f(0) и любых o,a выполняется o ≤ veblenWith(f, o, a).

LaTeX

$$$\forall f:\,\operatorname{Ordinal} \to \operatorname{Ordinal},\ \operatorname{IsNormal}(f)\ \Rightarrow\ (0 < f(0))\Rightarrow \forall o,a \in \operatorname{Ordinal},\ o \le \operatorname{veblenWith}(f,o,a)$$$

Lean4

theorem left_le_veblenWith (hp : 0 < f 0) (o a : Ordinal) : o ≤ veblenWith f o a :=
  (veblenWith_zero_strictMono hf hp).le_apply.trans <| (veblenWith_right_strictMono hf _).monotone (Ordinal.zero_le _)

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