Theorems · Definition · order theory
RelSeries.head
{α : Type u_1} → {r : SetRel α α} → RelSeries r → αStart of a series, i.e. for a₀ -r→ a₁ -r→ ... -r→ aₙ, its head is a₀.
Since a relation series is assumed to be non-empty, this is well defined.
- Defined in
- Mathlib.Order.RelSeries
- Cited by
- 89 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext
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.
- SetRelstatement and proof · cited by 581
- RelSeriesstatement and proof · cited by 129
- RelSeries.toFunproof · cited by 114
Cited by94
Results whose statement or proof uses this declaration.
- RelSeries.consstatement and proof · cited by 18
- RelSeries.smashstatement and proof · cited by 15
- RelSeries.appendstatement and proof · cited by 11
- Module.length_ne_top_iffproof · cited by 8
- RelSeries.cons_lengthstatement and proof · cited by 7
- Module.length_eq_add_of_exactproof · cited by 6
- RelSeries.smash_lengthstatement and proof · cited by 5
- RelSeries.toList_consstatement and proof · cited by 5
- RelSeries.head_snocstatement and proof · cited by 4
- RelSeries.last_smashstatement and proof · cited by 4
- Module.length_compositionSeriesstatement and proof · cited by 4
- isFiniteLength_iff_exists_compositionSeriesstatement and proof · cited by 4