Documentation

Mathlib.SetTheory.Ordinal.Veblen

Veblen hierarchy #

We define the two-arguments Veblen function, which satisfies veblen 0 a = ω ^ a and that for o ≠ 0, veblen o enumerates the common fixed points of veblen o' for o' < o.

We use this to define two important functions on ordinals: the epsilon function ε_ o = veblen 1 o, and the gamma function Γ_ o enumerating the fixed points of veblen · 0.

Main definitions #

veblenWith: The Veblen hierarchy with a specified initial function.
veblen: The Veblen hierarchy starting with ω ^ ·.

Notation #

The following notation is scoped to the Ordinal namespace.

ε_ o is notation for veblen 1 o. ε₀ is notation for ε_ 0.
Γ_ o is notation for gamma o. Γ₀ is notation for Γ_ 0.

TODO #

Prove that ε₀ and Γ₀ are countable.
Prove that the exponential principal ordinals are the epsilon ordinals (and 0, 1, 2, ω).
Prove that the ordinals principal under veblen are the gamma ordinals (and 0).

References #

[Larry W. Miller, Normal functions and constructive ordinal notations][Miller_1976]

Veblen function with a given starting function #

@[irreducible]

def Ordinal.veblenWith (f : Ordinal.{u} → Ordinal.{u}) (o : Ordinal.{u}) :

Ordinal.{u} → Ordinal.{u}

veblenWith f o is the o-th function in the Veblen hierarchy starting with f. This is defined so that

veblenWith f 0 = f.
veblenWith f o for o ≠ 0 enumerates the common fixed points of veblenWith f o' over all o' < o.

Equations

Instances For

@[simp]

theorem Ordinal.veblenWith_zero (f : Ordinal.{u_1} → Ordinal.{u_1}) :

veblenWith f 0 = f

theorem Ordinal.veblenWith_of_ne_zero {o : Ordinal.{u}} (f : Ordinal.{u} → Ordinal.{u}) (h : o ≠ 0) :

veblenWith f o = derivFamily fun (x : ↑(Set.Iio o)) => veblenWith f ↑x

theorem Ordinal.isNormal_veblenWith' {o : Ordinal.{u}} (f : Ordinal.{u} → Ordinal.{u}) (h : o ≠ 0) :

Order.IsNormal (veblenWith f o)

veblenWith f o is always normal for o ≠ 0. See isNormal_veblenWith for a version which assumes IsNormal f.

theorem Ordinal.isNormal_veblenWith {f : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) (o : Ordinal.{u}) :

Order.IsNormal (veblenWith f o)

veblenWith f o is always normal whenever f is. See isNormal_veblenWith' for a version which does not assume IsNormal f.

@[deprecated Ordinal.isNormal_veblenWith (since := "2025-12-25")]

theorem Ordinal.IsNormal.veblenWith {f : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) (o : Ordinal.{u}) :

Order.IsNormal (veblenWith f o)

Alias of Ordinal.isNormal_veblenWith.

veblenWith f o is always normal whenever f is. See isNormal_veblenWith' for a version which does not assume IsNormal f.

theorem Ordinal.mem_range_veblenWith {f : Ordinal.{u} → Ordinal.{u}} {o a : Ordinal.{u}} (hf : Order.IsNormal f) (h : o ≠ 0) :

a ∈ Set.range (veblenWith f o) ↔ ∀ b < o, veblenWith f b a = a

theorem Ordinal.veblenWith_veblenWith_of_lt {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ : Ordinal.{u}} (hf : Order.IsNormal f) (h : o₁ < o₂) (a : Ordinal.{u}) :

veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a

theorem Ordinal.veblenWith_eq_self_of_le {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a : Ordinal.{u}} (hf : Order.IsNormal f) (h : o₁ ≤ o₂) (h' : veblenWith f o₂ a = a) :

veblenWith f o₁ a = a

theorem Ordinal.veblenWith_mem_range {f : Ordinal.{u} → Ordinal.{u}} {o a : Ordinal.{u}} (hf : Order.IsNormal f) :

veblenWith f o a ∈ Set.range f

theorem Ordinal.veblenWith_succ {f : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) (o : Ordinal.{u}) :

veblenWith f (Order.succ o) = deriv (veblenWith f o)

theorem Ordinal.veblenWith_right_strictMono {f : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) (o : Ordinal.{u}) :

StrictMono (veblenWith f o)

@[simp]

theorem Ordinal.veblenWith_lt_veblenWith_iff_right {f : Ordinal.{u} → Ordinal.{u}} {o a b : Ordinal.{u}} (hf : Order.IsNormal f) :

veblenWith f o a < veblenWith f o b ↔ a < b

@[simp]

theorem Ordinal.veblenWith_le_veblenWith_iff_right {f : Ordinal.{u} → Ordinal.{u}} {o a b : Ordinal.{u}} (hf : Order.IsNormal f) :

veblenWith f o a ≤ veblenWith f o b ↔ a ≤ b

theorem Ordinal.veblenWith_injective {f : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) (o : Ordinal.{u}) :

Function.Injective (veblenWith f o)

@[simp]

theorem Ordinal.veblenWith_inj {f : Ordinal.{u} → Ordinal.{u}} {o a b : Ordinal.{u}} (hf : Order.IsNormal f) :

veblenWith f o a = veblenWith f o b ↔ a = b

theorem Ordinal.right_le_veblenWith {f : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) (o a : Ordinal.{u}) :

a ≤ veblenWith f o a

theorem Ordinal.veblenWith_left_monotone {f : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) (a : Ordinal.{u}) :

Monotone fun (x : Ordinal.{u}) => veblenWith f x a

theorem Ordinal.veblenWith_pos {f : Ordinal.{u} → Ordinal.{u}} {o a : Ordinal.{u}} (hf : Order.IsNormal f) (hp : 0 < f 0) :

0 < veblenWith f o a

theorem Ordinal.veblenWith_zero_strictMono {f : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) (hp : 0 < f 0) :

StrictMono fun (x : Ordinal.{u}) => veblenWith f x 0

theorem Ordinal.veblenWith_zero_lt_veblenWith_zero {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ : Ordinal.{u}} (hf : Order.IsNormal f) (hp : 0 < f 0) :

veblenWith f o₁ 0 < veblenWith f o₂ 0 ↔ o₁ < o₂

theorem Ordinal.veblenWith_zero_le_veblenWith_zero {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ : Ordinal.{u}} (hf : Order.IsNormal f) (hp : 0 < f 0) :

veblenWith f o₁ 0 ≤ veblenWith f o₂ 0 ↔ o₁ ≤ o₂

theorem Ordinal.veblenWith_zero_inj {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ : Ordinal.{u}} (hf : Order.IsNormal f) (hp : 0 < f 0) :

veblenWith f o₁ 0 = veblenWith f o₂ 0 ↔ o₁ = o₂

theorem Ordinal.left_le_veblenWith {f : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) (hp : 0 < f 0) (o a : Ordinal.{u}) :

o ≤ veblenWith f o a

theorem Ordinal.isNormal_veblenWith_zero {f : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) (hp : 0 < f 0) :

Order.IsNormal fun (x : Ordinal.{u}) => veblenWith f x 0

@[deprecated Ordinal.isNormal_veblenWith_zero (since := "2025-12-25")]

theorem Ordinal.IsNormal.veblenWith_zero {f : Ordinal.{u} → Ordinal.{u}} (hf : Order.IsNormal f) (hp : 0 < f 0) :

Order.IsNormal fun (x : Ordinal.{u}) => veblenWith f x 0

Alias of Ordinal.isNormal_veblenWith_zero.

theorem Ordinal.veblenWith_veblenWith_eq_veblenWith_iff {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a : Ordinal.{u}} (hf : Order.IsNormal f) (h : o₂ ≤ o₁) :

veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a ↔ veblenWith f o₁ a = a

theorem Ordinal.veblenWith_lt_veblenWith_veblenWith_iff {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a : Ordinal.{u}} (hf : Order.IsNormal f) (h : o₂ ≤ o₁) :

veblenWith f o₂ a < veblenWith f o₁ (veblenWith f o₂ a) ↔ a < veblenWith f o₁ a

theorem Ordinal.veblenWith_apply_eq_apply_iff {f : Ordinal.{u} → Ordinal.{u}} {o a : Ordinal.{u}} (hf : Order.IsNormal f) :

veblenWith f o (f a) = f a ↔ veblenWith f o a = a

theorem Ordinal.apply_lt_veblenWith_apply_iff {f : Ordinal.{u} → Ordinal.{u}} {o a : Ordinal.{u}} (hf : Order.IsNormal f) :

f a < veblenWith f o (f a) ↔ a < veblenWith f o a

theorem Ordinal.cmp_veblenWith {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a b : Ordinal.{u}} (hf : Order.IsNormal f) :

cmp (veblenWith f o₁ a) (veblenWith f o₂ b) = match cmp o₁ o₂ with | Ordering.eq => cmp a b | Ordering.lt => cmp a (veblenWith f o₂ b) | Ordering.gt => cmp (veblenWith f o₁ a) b

theorem Ordinal.veblenWith_lt_veblenWith_iff {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a b : Ordinal.{u}} (hf : Order.IsNormal f) :

veblenWith f o₁ a < veblenWith f o₂ b ↔ o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a < b

veblenWith f o₁ a < veblenWith f o₂ b iff one of the following holds:

o₁ = o₂ and a < b
o₁ < o₂ and a < veblenWith f o₂ b
o₁ > o₂ and veblenWith f o₁ a < b

theorem Ordinal.veblenWith_le_veblenWith_iff {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a b : Ordinal.{u}} (hf : Order.IsNormal f) :

veblenWith f o₁ a ≤ veblenWith f o₂ b ↔ o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a ≤ b

veblenWith f o₁ a ≤ veblenWith f o₂ b iff one of the following holds:

o₁ = o₂ and a ≤ b
o₁ < o₂ and a ≤ veblenWith f o₂ b
o₁ > o₂ and veblenWith f o₁ a ≤ b

theorem Ordinal.veblenWith_eq_veblenWith_iff {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a b : Ordinal.{u}} (hf : Order.IsNormal f) :

veblenWith f o₁ a = veblenWith f o₂ b ↔ o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a = b

veblenWith f o₁ a = veblenWith f o₂ b iff one of the following holds:

o₁ = o₂ and a = b
o₁ < o₂ and a = veblenWith f o₂ b
o₁ > o₂ and veblenWith f o₁ a = b

Veblen function #

def Ordinal.veblen :

Ordinal.{u} → Ordinal.{u} → Ordinal.{u}

veblen o is the o-th function in the Veblen hierarchy starting with ω ^ ·. That is:

veblen 0 a = ω ^ a.
veblen o for o ≠ 0 enumerates the fixed points of veblen o' for o' < o.

Equations

Instances For

@[simp]

theorem Ordinal.veblen_zero :

veblen 0 = fun (a : Ordinal.{u_1}) => omega0 ^ a

theorem Ordinal.veblen_zero_apply (a : Ordinal.{u_1}) :

veblen 0 a = omega0 ^ a

theorem Ordinal.veblen_of_ne_zero {o : Ordinal.{u}} (h : o ≠ 0) :

veblen o = derivFamily fun (x : ↑(Set.Iio o)) => veblen ↑x

theorem Ordinal.isNormal_veblen (o : Ordinal.{u_1}) :

Order.IsNormal (veblen o)

theorem Ordinal.mem_range_veblen {o a : Ordinal.{u}} (h : o ≠ 0) :

a ∈ Set.range (veblen o) ↔ ∀ b < o, veblen b a = a

theorem Ordinal.veblen_veblen_of_lt {o₁ o₂ : Ordinal.{u}} (h : o₁ < o₂) (a : Ordinal.{u}) :

veblen o₁ (veblen o₂ a) = veblen o₂ a

theorem Ordinal.veblen_eq_self_of_le {o₁ o₂ a : Ordinal.{u}} (h : o₁ ≤ o₂) (h' : veblen o₂ a = a) :

veblen o₁ a = a

theorem Ordinal.veblen_mem_range_opow (o a : Ordinal.{u_1}) :

veblen o a ∈ Set.range fun (x : Ordinal.{u_1}) => omega0 ^ x

theorem Ordinal.veblen_succ (o : Ordinal.{u_1}) :

veblen (Order.succ o) = deriv (veblen o)

theorem Ordinal.veblen_right_strictMono (o : Ordinal.{u_1}) :

StrictMono (veblen o)

@[simp]

theorem Ordinal.veblen_lt_veblen_iff_right {o a b : Ordinal.{u}} :

veblen o a < veblen o b ↔ a < b

@[simp]

theorem Ordinal.veblen_le_veblen_iff_right {o a b : Ordinal.{u}} :

veblen o a ≤ veblen o b ↔ a ≤ b

theorem Ordinal.veblen_injective (o : Ordinal.{u_1}) :

Function.Injective (veblen o)

@[simp]

theorem Ordinal.veblen_inj {o a b : Ordinal.{u}} :

veblen o a = veblen o b ↔ a = b

theorem Ordinal.right_le_veblen (o a : Ordinal.{u_1}) :

a ≤ veblen o a

theorem Ordinal.veblen_left_monotone (o : Ordinal.{u_1}) :

Monotone fun (x : Ordinal.{u_1}) => veblen x o

@[simp]

theorem Ordinal.veblen_pos {o a : Ordinal.{u}} :

0 < veblen o a

theorem Ordinal.veblen_zero_strictMono :

StrictMono fun (x : Ordinal.{u_1}) => veblen x 0

@[simp]

theorem Ordinal.veblen_zero_lt_veblen_zero {o₁ o₂ : Ordinal.{u}} :

veblen o₁ 0 < veblen o₂ 0 ↔ o₁ < o₂

@[simp]

theorem Ordinal.veblen_zero_le_veblen_zero {o₁ o₂ : Ordinal.{u}} :

veblen o₁ 0 ≤ veblen o₂ 0 ↔ o₁ ≤ o₂

@[simp]

theorem Ordinal.veblen_zero_inj {o₁ o₂ : Ordinal.{u}} :

veblen o₁ 0 = veblen o₂ 0 ↔ o₁ = o₂

theorem Ordinal.left_le_veblen (o a : Ordinal.{u_1}) :

o ≤ veblen o a

theorem Ordinal.isNormal_veblen_zero :

Order.IsNormal fun (x : Ordinal.{u_1}) => veblen x 0

theorem Ordinal.veblen_veblen_eq_veblen_iff {o₁ o₂ a : Ordinal.{u}} (h : o₂ ≤ o₁) :

veblen o₁ (veblen o₂ a) = veblen o₂ a ↔ veblen o₁ a = a

theorem Ordinal.veblen_lt_veblen_veblen_iff {o₁ o₂ a : Ordinal.{u}} (h : o₂ ≤ o₁) :

veblen o₂ a < veblen o₁ (veblen o₂ a) ↔ a < veblen o₁ a

theorem Ordinal.veblen_opow_eq_opow_iff {o a : Ordinal.{u}} :

veblen o (omega0 ^ a) = omega0 ^ a ↔ veblen o a = a

theorem Ordinal.opow_lt_veblen_opow_iff {o a : Ordinal.{u}} :

omega0 ^ a < veblen o (omega0 ^ a) ↔ a < veblen o a

theorem Ordinal.lt_veblen (a : Ordinal.{u_1}) :

a < veblen a a

theorem Ordinal.cmp_veblen {o₁ o₂ a b : Ordinal.{u}} :

cmp (veblen o₁ a) (veblen o₂ b) = match cmp o₁ o₂ with | Ordering.eq => cmp a b | Ordering.lt => cmp a (veblen o₂ b) | Ordering.gt => cmp (veblen o₁ a) b

theorem Ordinal.veblen_lt_veblen_iff {o₁ o₂ a b : Ordinal.{u}} :

veblen o₁ a < veblen o₂ b ↔ o₁ = o₂ ∧ a < b ∨ o₁ < o₂ ∧ a < veblen o₂ b ∨ o₂ < o₁ ∧ veblen o₁ a < b

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 Ordinal.veblen_le_veblen_iff {o₁ o₂ a b : Ordinal.{u}} :

veblen o₁ a ≤ veblen o₂ b ↔ o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblen o₂ b ∨ o₂ < o₁ ∧ veblen o₁ a ≤ b

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 Ordinal.veblen_eq_veblen_iff {o₁ o₂ a b : Ordinal.{u}} :

veblen o₁ a = veblen o₂ b ↔ o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblen o₂ b ∨ o₂ < o₁ ∧ veblen o₁ a = b

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

Inverse Veblen function #

def Ordinal.invVeblen₁ (x : Ordinal.{u_1}) :

For any given x, there exists a unique pair (o, a) such that ω ^ x = veblen o a and a < ω ^ x. invVeblen₁ x and invVeblen₂ x return the first and second entries of this pair, respectively. See veblen_eq_opow_iff for a proof.

Composing this function with Ordinal.CNF yields a predicative ordinal notation up to Γ₀.

Equations

Instances For

theorem Ordinal.veblen_eq_of_lt_invVeblen₁ {o x : Ordinal.{u}} (h : o < x.invVeblen₁) :

veblen o x = x

theorem Ordinal.invVeblen₁_le (x : Ordinal.{u_1}) :

x.invVeblen₁ ≤ x

theorem Ordinal.lt_veblen_invVeblen₁ (x : Ordinal.{u_1}) :

x < veblen x.invVeblen₁ x

theorem Ordinal.lt_veblen_iff_invVeblen₁_le {o a : Ordinal.{u}} :

a < veblen o a ↔ a.invVeblen₁ ≤ o

theorem Ordinal.mem_range_veblen_iff_le_invVeblen₁ {o x : Ordinal.{u}} :

omega0 ^ x ∈ Set.range (veblen o) ↔ o ≤ x.invVeblen₁

theorem Ordinal.invVeblen₁_veblen {o a : Ordinal.{u}} (h : a < veblen o a) :

(veblen o a).invVeblen₁ = o

theorem Ordinal.invVeblen₁_of_lt_opow {a : Ordinal.{u}} (h : a < omega0 ^ a) :

a.invVeblen₁ = 0

@[simp]

theorem Ordinal.invVeblen₁_zero :

invVeblen₁ 0 = 0

def Ordinal.invVeblen₂ (x : Ordinal.{u_1}) :

For any given x, there exists a unique pair (o, a) such that ω ^ x = veblen o a and a < ω ^ x. invVeblen₁ x and invVeblen₂ x return the first and second entries of this pair, respectively. See veblen_eq_opow_iff for a proof.

Composing this function with Ordinal.CNF yields a predicative ordinal notation up to Γ₀.

Equations

Instances For

@[simp]

theorem Ordinal.veblen_invVeblen₁_invVeblen₂ (x : Ordinal.{u_1}) :

veblen x.invVeblen₁ x.invVeblen₂ = omega0 ^ x

theorem Ordinal.invVeblen₂_eq_iff {a x : Ordinal.{u}} :

x.invVeblen₂ = a ↔ omega0 ^ x = veblen x.invVeblen₁ a

theorem Ordinal.invVeblen₂_lt_iff {a x : Ordinal.{u}} :

x.invVeblen₂ < a ↔ omega0 ^ x < veblen x.invVeblen₁ a

theorem Ordinal.invVeblen₂_le_iff {a x : Ordinal.{u}} :

x.invVeblen₂ ≤ a ↔ omega0 ^ x ≤ veblen x.invVeblen₁ a

theorem Ordinal.lt_invVeblen₂_iff {a x : Ordinal.{u}} :

a < x.invVeblen₂ ↔ veblen x.invVeblen₁ a < omega0 ^ x

theorem Ordinal.le_invVeblen₂_iff {a x : Ordinal.{u}} :

a ≤ x.invVeblen₂ ↔ veblen x.invVeblen₁ a ≤ omega0 ^ x

theorem Ordinal.invVeblen₂_lt (x : Ordinal.{u_1}) :

x.invVeblen₂ < omega0 ^ x

theorem Ordinal.invVeblen₂_le (x : Ordinal.{u_1}) :

x.invVeblen₂ ≤ x

theorem Ordinal.invVeblen₂_of_lt_opow {a : Ordinal.{u}} (h : a < omega0 ^ a) :

a.invVeblen₂ = a

@[simp]

theorem Ordinal.invVeblen₂_zero :

invVeblen₂ 0 = 0

theorem Ordinal.invVeblen₂_veblen {o a : Ordinal.{u}} (ho : o ≠ 0) (h : a < veblen o a) :

(veblen o a).invVeblen₂ = a

theorem Ordinal.veblen_eq_opow_iff {o a x : Ordinal.{u}} (h : a < veblen o a) :

veblen o a = omega0 ^ x ↔ x.invVeblen₁ = o ∧ x.invVeblen₂ = a

Epsilon function #

@[reducible, inline]

abbrev Ordinal.epsilon :

Ordinal.{u_1} → Ordinal.{u_1}

The epsilon function enumerates the fixed points of ω ^ ⬝. This is an abbreviation for veblen 1.

Conventions for notations in identifiers:

The recommended spelling of ε_ in identifiers is epsilon.

Equations

Instances For

def Ordinal.termε_ :

Lean.ParserDescr

The epsilon function enumerates the fixed points of ω ^ ⬝. This is an abbreviation for veblen 1.

Conventions for notations in identifiers:

The recommended spelling of ε_ in identifiers is epsilon.

Equations

Instances For

def Ordinal.termε₀ :

Lean.ParserDescr

ε₀ is the first fixed point of ω ^ ⬝, i.e. the supremum of ω, ω ^ ω, ω ^ ω ^ ω, …

Conventions for notations in identifiers:

The recommended spelling of ε₀ in identifiers is epsilon_zero.

Equations

Instances For

theorem Ordinal.epsilon_eq_deriv (o : Ordinal.{u_1}) :

o.epsilon = deriv (fun (a : Ordinal.{u_1}) => omega0 ^ a) o

theorem Ordinal.epsilon_zero_eq_nfp :

epsilon 0 = nfp (fun (a : Ordinal.{u_1}) => omega0 ^ a) 0

@[deprecated Ordinal.epsilon_zero_eq_nfp (since := "2026-02-02")]

theorem Ordinal.epsilon0_eq_nfp :

epsilon 0 = nfp (fun (a : Ordinal.{u_1}) => omega0 ^ a) 0

Alias of Ordinal.epsilon_zero_eq_nfp.

theorem Ordinal.epsilon_succ_eq_nfp (o : Ordinal.{u_1}) :

(Order.succ o).epsilon = nfp (fun (a : Ordinal.{u_1}) => omega0 ^ a) (Order.succ o.epsilon)

theorem Ordinal.epsilon_zero_le_of_omega0_opow_le {o : Ordinal.{u}} (h : omega0 ^ o ≤ o) :

epsilon 0 ≤ o

@[deprecated Ordinal.epsilon_zero_le_of_omega0_opow_le (since := "2026-02-02")]

theorem Ordinal.epsilon0_le_of_omega0_opow_le {o : Ordinal.{u}} (h : omega0 ^ o ≤ o) :

epsilon 0 ≤ o

Alias of Ordinal.epsilon_zero_le_of_omega0_opow_le.

@[simp]

theorem Ordinal.omega0_opow_epsilon (o : Ordinal.{u_1}) :

omega0 ^ o.epsilon = o.epsilon

theorem Ordinal.lt_epsilon_zero {o : Ordinal.{u}} :

o < epsilon 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) => omega0 ^ a)^[n] 0

ε₀ is the limit of 0, ω ^ 0, ω ^ ω ^ 0, …

@[deprecated Ordinal.lt_epsilon_zero (since := "2026-02-02")]

theorem Ordinal.lt_epsilon0 {o : Ordinal.{u}} :

o < epsilon 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) => omega0 ^ a)^[n] 0

Alias of Ordinal.lt_epsilon_zero.

ε₀ is the limit of 0, ω ^ 0, ω ^ ω ^ 0, …

theorem Ordinal.iterate_omega0_opow_lt_epsilon_zero (n : ℕ) :

(fun (a : Ordinal.{u_1}) => omega0 ^ a)^[n] 0 < epsilon 0

ω ^ ω ^ … ^ 0 < ε₀

@[deprecated Ordinal.iterate_omega0_opow_lt_epsilon_zero (since := "2026-02-02")]

theorem Ordinal.iterate_omega0_opow_lt_epsilon0 (n : ℕ) :

(fun (a : Ordinal.{u_1}) => omega0 ^ a)^[n] 0 < epsilon 0

Alias of Ordinal.iterate_omega0_opow_lt_epsilon_zero.

ω ^ ω ^ … ^ 0 < ε₀

theorem Ordinal.omega0_lt_epsilon (o : Ordinal.{u_1}) :

omega0 < o.epsilon

theorem Ordinal.natCast_lt_epsilon (n : ℕ) (o : Ordinal.{u_1}) :

↑n < o.epsilon

theorem Ordinal.epsilon_pos (o : Ordinal.{u_1}) :

theorem Ordinal.invVeblen₁_epsilon {o : Ordinal.{u}} (h : o < o.epsilon) :

o.epsilon.invVeblen₁ = 1

theorem Ordinal.invVeblen₂_epsilon {o : Ordinal.{u}} (h : o < o.epsilon) :

o.epsilon.invVeblen₂ = o

Gamma function #

def Ordinal.gamma :

Ordinal.{u_1} → Ordinal.{u_1}

The gamma function enumerates the fixed points of veblen · 0.

Of particular importance is Γ₀ = gamma 0, the Feferman-Schütte ordinal.

Conventions for notations in identifiers:

The recommended spelling of Γ_ in identifiers is gamma.

Equations

Instances For

def Ordinal.termΓ_ :

Lean.ParserDescr

The gamma function enumerates the fixed points of veblen · 0.

Of particular importance is Γ₀ = gamma 0, the Feferman-Schütte ordinal.

Conventions for notations in identifiers:

The recommended spelling of Γ_ in identifiers is gamma.

Equations

Instances For

def Ordinal.termΓ₀ :

Lean.ParserDescr

The Feferman-Schütte ordinal Γ₀ is the smallest fixed point of veblen · 0, i.e. the supremum of veblen ε₀ 0, veblen (veblen ε₀ 0) 0, etc.

Conventions for notations in identifiers:

The recommended spelling of Γ₀ in identifiers is gamma_zero.

Equations

Instances For

theorem Ordinal.isNormal_gamma :

Order.IsNormal gamma

theorem Ordinal.mem_range_gamma {o : Ordinal.{u}} :

o ∈ Set.range gamma ↔ veblen o 0 = o

theorem Ordinal.strictMono_gamma :

StrictMono gamma

theorem Ordinal.monotone_gamma :

@[simp]

theorem Ordinal.gamma_lt_gamma {a b : Ordinal.{u}} :

a.gamma < b.gamma ↔ a < b

@[simp]

theorem Ordinal.gamma_le_gamma {a b : Ordinal.{u}} :

a.gamma ≤ b.gamma ↔ a ≤ b

@[simp]

theorem Ordinal.gamma_inj {a b : Ordinal.{u}} :

a.gamma = b.gamma ↔ a = b

@[simp]

theorem Ordinal.veblen_gamma_zero (o : Ordinal.{u_1}) :

veblen o.gamma 0 = o.gamma

theorem Ordinal.gamma_zero_eq_nfp :

gamma 0 = nfp (fun (x : Ordinal.{u_1}) => veblen x 0) 0

@[deprecated Ordinal.gamma_zero_eq_nfp (since := "2026-02-02")]

theorem Ordinal.gamma0_eq_nfp :

gamma 0 = nfp (fun (x : Ordinal.{u_1}) => veblen x 0) 0

Alias of Ordinal.gamma_zero_eq_nfp.

theorem Ordinal.gamma_succ_eq_nfp (o : Ordinal.{u_1}) :

(Order.succ o).gamma = nfp (fun (x : Ordinal.{u_1}) => veblen x 0) (Order.succ o.gamma)

theorem Ordinal.gamma_zero_le_of_veblen_le {o : Ordinal.{u}} (h : veblen o 0 ≤ o) :

@[deprecated Ordinal.gamma_zero_le_of_veblen_le (since := "2026-02-02")]

theorem Ordinal.gamma0_le_of_veblen_le {o : Ordinal.{u}} (h : veblen o 0 ≤ o) :

Alias of Ordinal.gamma_zero_le_of_veblen_le.

theorem Ordinal.lt_gamma_zero {o : Ordinal.{u}} :

o < gamma 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) => veblen a 0)^[n] 0

Γ₀ is the limit of 0, veblen 0 0, veblen (veblen 0 0) 0, …

@[deprecated Ordinal.lt_gamma_zero (since := "2026-02-02")]

theorem Ordinal.lt_gamma0 {o : Ordinal.{u}} :

o < gamma 0 ↔ ∃ (n : ℕ), o < (fun (a : Ordinal.{u}) => veblen a 0)^[n] 0

Alias of Ordinal.lt_gamma_zero.

Γ₀ is the limit of 0, veblen 0 0, veblen (veblen 0 0) 0, …

theorem Ordinal.iterate_veblen_lt_gamma_zero (n : ℕ) :

(fun (a : Ordinal.{u_1}) => veblen a 0)^[n] 0 < gamma 0

veblen (veblen … (veblen 0 0) … 0) 0 < Γ₀

@[deprecated Ordinal.iterate_veblen_lt_gamma_zero (since := "2026-02-02")]

theorem Ordinal.iterate_veblen_lt_gamma0 (n : ℕ) :

(fun (a : Ordinal.{u_1}) => veblen a 0)^[n] 0 < gamma 0

Alias of Ordinal.iterate_veblen_lt_gamma_zero.

veblen (veblen … (veblen 0 0) … 0) 0 < Γ₀

theorem Ordinal.epsilon_zero_lt_gamma (o : Ordinal.{u_1}) :

epsilon 0 < o.gamma

@[deprecated Ordinal.epsilon_zero_lt_gamma (since := "2026-02-02")]

theorem Ordinal.epsilon0_lt_gamma (o : Ordinal.{u_1}) :

epsilon 0 < o.gamma

Alias of Ordinal.epsilon_zero_lt_gamma.

theorem Ordinal.omega0_lt_gamma (o : Ordinal.{u_1}) :

omega0 < o.gamma

theorem Ordinal.natCast_lt_gamma {o : Ordinal.{u}} (n : ℕ) :

↑n < o.gamma

@[simp]

theorem Ordinal.gamma_pos {o : Ordinal.{u}} :

@[simp]

theorem Ordinal.gamma_ne_zero {o : Ordinal.{u}} :

@[simp]

theorem Ordinal.invVeblen₁_gamma (o : Ordinal.{u_1}) :

o.gamma.invVeblen₁ = o.gamma

@[simp]

theorem Ordinal.invVeblen₂_gamma (o : Ordinal.{u_1}) :

o.gamma.invVeblen₂ = 0

theorem Ordinal.invVeblen₁_eq_iff {o : Ordinal.{u}} :

o.invVeblen₁ = o ↔ o = 0 ∨ o ∈ Set.range gamma

theorem Ordinal.invVeblen₁_lt_iff {o : Ordinal.{u}} :

o.invVeblen₁ < o ↔ o ≠ 0 ∧ o ∉ Set.range gamma