Theorems · Theorem · logic and foundations
WellOrder.mk.sizeOf_spec
∀ (α : Type u) (r : α → α → Prop) (wo : IsWellOrder α r), sizeOf { α := α, r := r, wo := wo } = 1 + sizeOf α + sizeOf wo- Defined in
- Mathlib.SetTheory.Ordinal.Basic
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
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.
- IsWellOrderstatement and proof · cited by 171
- WellOrderstatement · cited by 12
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.