veblenWith_left_monotone — Mathlib

English

For a fixed a, the map o ↦ veblenWith(f, o, a) is monotone in o.

Русский

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

LaTeX

$$$\forall f:\,\operatorname{Ordinal} \to \operatorname{Ordinal},\ \operatorname{IsNormal}(f)\ \Rightarrow\ \forall a:\operatorname{Ordinal},\ \operatorname{Monotone}(o \mapsto \operatorname{veblenWith}(f,o,a))$$$

Lean4

theorem veblenWith_left_monotone (a : Ordinal) : Monotone (veblenWith f · a) :=
  by
  rw [monotone_iff_forall_lt]
  intro o₁ o₂ h
  rw [← veblenWith_veblenWith_of_lt hf h]
  exact (veblenWith_right_strictMono hf o₁).monotone (right_le_veblenWith hf o₂ a)

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