Theorems · Definition · order theory

RelSeries.last

{α : Type u_1} → {r : SetRel α α} → RelSeries r → α

End of a series, i.e. for a₀ -r→ a₁ -r→ ... -r→ aₙ, its last element is aₙ. Since a relation series is assumed to be non-empty, this is well defined.

Defined in

Mathlib.Order.RelSeries

Cited by

114 results in Mathlib

Foundations

Depth 11 from the axioms, rests on 37 definitions · uses no axioms