veblenWith_veblenWith_of_lt — Mathlib

English

If o1 < o2, then veblenWith f o1 (veblenWith f o2 a) = veblenWith f o2 a for all a.

Русский

Если o1 < o2, то veblenWith f o1 (veblenWith f o2 a) = veblenWith f o2 a для всех a.

LaTeX

$$theorem veblenWith_veblenWith_of_lt (h : o1 < o2) (a : Ordinal) : veblenWith f o1 (veblenWith f o2 a) = veblenWith f o2 a$$

Lean4

theorem veblenWith_veblenWith_of_lt (h : o₁ < o₂) (a : Ordinal) :
    veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a :=
  by
  apply (mem_range_veblenWith hf h.ne_bot).1 _ _ h
  simp

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