veblenWith_pos — Mathlib

English

If 0 < f(0) for a normal f, then 0 < veblenWith(f, o, a) for all o, a.

Русский

Если для нормальной f выполнено 0 < f(0), то для всех o, a выполняется 0 < 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},\ 0 < \operatorname{veblenWith}(f,o,a)$$$

Lean4

theorem veblenWith_pos (hp : 0 < f 0) : 0 < veblenWith f o a :=
  by
  have H (b) : 0 < veblenWith f 0 b := by
    rw [veblenWith_zero]
    exact hp.trans_le (hf.monotone (Ordinal.zero_le _))
  obtain rfl | h := eq_zero_or_pos o
  · exact H a
  · rw [← veblenWith_veblenWith_of_lt hf h]
    exact H _

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