Def RelSeries.append

Modification history

2025-07-06 13:16
Mathlib/Order/RelSeries.lean
refactor: make `Rel` less see-through (#25587) …
Modified RelSeries.appendView on Github →
2023-12-28 07:15
Mathlib/Order/RelSeries.lean
feat: add some constructions about `RelSeries` (`append`, `insert_nth`, `map`, `comap`) (#3858) …
Added RelSeries.appendView on Github →