Theorems · Definition · logic and foundations
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.
- Defined in
- Mathlib.SetTheory.Ordinal.Veblen
- Cited by
- 18 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.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ordinalstatement · cited by 1,688
- Ordinal.veblenproof · cited by 64
Cited by18
Results whose statement or proof uses this declaration.
- Ordinal.epsilon_zero_eq_nfpstatement · cited by 4
- Ordinal.epsilon_eq_derivstatement · cited by 3
- Ordinal.omega0_lt_epsilonstatement and proof · cited by 2
- Ordinal.iterate_omega0_opow_lt_epsilon_zerostatement · cited by 2
- Ordinal.epsilon_zero_lt_gammastatement · cited by 2
- Ordinal.lt_epsilon_zerostatement · cited by 1
- Ordinal.epsilon_zero_le_of_omega0_opow_lestatement · cited by 1
- Ordinal.iterate_omega0_opow_lt_epsilon0statement · cited by 0
- Ordinal.omega0_opow_epsilonstatement · cited by 0
- Ordinal.lt_epsilon0statement · cited by 0
- Ordinal.invVeblen₁_epsilonstatement and proof · cited by 0
- Ordinal.invVeblen₂_epsilonstatement and proof · cited by 0