Def RelSeries.map

Modification history

2025-07-06 13:16

Mathlib/Order/RelSeries.lean

refactor: make `Rel` less see-through (#25587) …

Modified RelSeries.map View on Github →

2024-03-28 10:26

Mathlib/Order/RelSeries.lean

refactor(Order/RelSeries): Use `RelHom` in `RelSeries.map` (#11730) …

Modified RelSeries.map View 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.map View on Github →