veblen_veblen_eq_veblen_iff — Mathlib

English

If o2 ≤ o1, then veBl en(o1, veBl en(o2, a)) = veBl en(o2, a) iff veBl en(o1, a) = a.

Русский

Если o2 ≤ o1, то veBl en(o1, veBl en(o2, a)) = veBl en(o2, a) тогда и только тогда, когда veBl en(o1, a) = a.

LaTeX

$$$$\\operatorname{veblen}(o_1, \\operatorname{veblen}(o_2,a)) = \\operatorname{veblen}(o_2,a) \\iff \\operatorname{veblen}(o_1,a) = a.$$$$

Lean4

theorem veblen_veblen_eq_veblen_iff (h : o₂ ≤ o₁) : veblen o₁ (veblen o₂ a) = veblen o₂ a ↔ veblen o₁ a = a :=
  veblenWith_veblenWith_eq_veblenWith_iff (isNormal_opow one_lt_omega0) h

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