Commit 2024-05-17 17:53 f933e98b
View on Github →feat(Order/RelSeries): add snoc
construction (#12915)
Given a series a₀ -r→ a₁ -r→ ... -r→ aₙ
and an a
such that aₙ -r→ a
holds, there is
a series of length n+1
: a₀ -r→ a₁ -r→ ... -r→ aₙ -r→ a
.
These and some other lemmas in this PR are all extracted from Order/JordanHolder.lean