Theorems · Theorem · order theory
RelSeries.last_reverse
∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r), p.reverse.last = p.head- Defined in
- Mathlib.Order.RelSeries
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 53 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SetRelstatement and proof · cited by 581
- RelSeries.lengthproof · cited by 195
- RelSeriesstatement and proof · cited by 129
- RelSeries.laststatement · cited by 114
- RelSeries.toFunproof · cited by 114
- RelSeries.headstatement · cited by 89
- SetRel.invstatement · cited by 36
- RelSeries.reversestatement · cited by 11
Cited by3
Results whose statement or proof uses this declaration.
- Order.coheight_eq_top_iffproof · cited by 1
- Order.length_le_coheightproof · cited by 1
- Order.coheight_eq_index_of_length_eq_head_coheightproof · cited by 0