veblenWith_zero_strictMono — Mathlib

English

If 0 < f(0), then the function o ↦ veblenWith(f, o, 0) is strictly monotone in o.

Русский

Если 0 < f(0), то функция o ↦ veblenWith(f, o, 0) строго монотонна по o.

LaTeX

$$$\forall f:\,\operatorname{Ordinal} \to \operatorname{Ordinal},\ \operatorname{IsNormal}(f)\ \Rightarrow\ (0 < f(0)) \Rightarrow \operatorname{StrictMono}(o \mapsto \operatorname{veblenWith}(f,o,0))$$$

Lean4

theorem veblenWith_zero_strictMono (hp : 0 < f 0) : StrictMono (veblenWith f · 0) :=
  by
  intro o₁ o₂ h
  dsimp only
  rw [← veblenWith_veblenWith_of_lt hf h, veblenWith_lt_veblenWith_iff_right hf]
  exact veblenWith_pos hf hp

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