Theorems · Definition · order theory
RelSeries.reverse
{α : Type u_1} → {r : SetRel α α} → RelSeries r → RelSeries r.invA relation series a₀ -r→ a₁ -r→ ... -r→ aₙ of r gives a relation series of the reverse of r
by reversing the series aₙ ←r- aₙ₋₁ ←r- ... ←r- a₁ ←r- a₀.
- Defined in
- Mathlib.Order.RelSeries
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 52 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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.toFunproof · cited by 114
- SetRel.invstatement · cited by 36
Cited by11
Results whose statement or proof uses this declaration.
- Order.krullDim_orderDualproof · cited by 7
- RelSeries.reverse_lengthstatement and proof · cited by 4
- RelSeries.last_reversestatement · cited by 3
- RelSeries.reverse_reversestatement and proof · cited by 2
- RelSeries.head_reversestatement and proof · cited by 2
- Order.coheight_eqproof · cited by 1
- Order.coheight_eq_iSup_head_eqproof · cited by 1
- Order.coheight_eq_top_iffproof · cited by 1
- Order.exists_series_of_le_coheightproof · cited by 1
- Order.rev_index_le_coheightproof · cited by 0
- RelSeries.reverse_applystatement · cited by 0