veblen_lt_veblen_veblen_iff — Mathlib

English

For h : o2 ≤ o1, the inequality veBl en o2 a < veBl en o1 (veblen o2 a) is equivalent to a < veBl en o1 a.

Русский

При h: o2 ≤ o1 верно veBl en o2 a < veBl en o1 (veblen o2 a) тогда и только тогда a < veBl en o1 a.

LaTeX

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

Lean4

theorem veblen_lt_veblen_veblen_iff (h : o₂ ≤ o₁) : veblen o₂ a < veblen o₁ (veblen o₂ a) ↔ a < veblen o₁ a :=
  veblenWith_lt_veblenWith_veblenWith_iff (isNormal_opow one_lt_omega0) h

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