Theorems · Definition · logic and foundations
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.
- Defined in
- Mathlib.SetTheory.Ordinal.Veblen
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 44 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ordinalstatement and proof · cited by 1,688
- Ordinal.veblenproof · cited by 64
- Ordinal.derivproof · cited by 26
Cited by27
Results whose statement or proof uses this declaration.
- Ordinal.gamma_zero_eq_nfpstatement · cited by 4
- Ordinal.strictMono_gammastatement · cited by 3
- Ordinal.isNormal_gammastatement · cited by 2
- Ordinal.iterate_veblen_lt_gamma_zerostatement · cited by 2
- Ordinal.epsilon_zero_lt_gammastatement and proof · cited by 2
- Ordinal.veblen_gamma_zerostatement · cited by 2
- Ordinal.mem_range_gammastatement · cited by 1
- Ordinal.omega0_lt_gammastatement · cited by 1
- Ordinal.gamma_le_gammastatement · cited by 1
- Ordinal.gamma_ne_zerostatement · cited by 1
- Ordinal.gamma_posstatement · cited by 1
- Ordinal.gamma_zero_le_of_veblen_lestatement · cited by 1