veblen_le_veblen_iff — Mathlib

English

If o2 ≤ o1, then veblen o2 a < veblen o1 (veblen o2 a) iff a < veblen o1 a.

Русский

Если o2 ≤ o1, то veblen o2 a < veblen o1(veblen o2 a) тогда и только тогда a < veblen 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

/-- `veblen o₁ a ≤ veblen o₂ b` iff one of the following holds:
* `o₁ = o₂` and `a ≤ b`
* `o₁ < o₂` and `a ≤ veblen o₂ b`
* `o₁ > o₂` and `veblen o₁ a ≤ b` -/
theorem veblen_le_veblen_iff :
    veblen o₁ a ≤ veblen o₂ b ↔ o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblen o₂ b ∨ o₂ < o₁ ∧ veblen o₁ a ≤ b :=
  veblenWith_le_veblenWith_iff (isNormal_opow one_lt_omega0)

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