Def Filter.comap

Modification history

2024-10-09 04:43

Mathlib/Order/Filter/Basic.lean

chore(Filter): move defs to a new file (#17552)

Modified Filter.comap View on Github →

2024-05-17 19:31

Mathlib/Order/Filter/Basic.lean

style: remove all isolated `where` (#12991)

Modified Filter.comap View on Github →

2023-01-23 08:16

Mathlib/Order/Filter/Basic.lean

Feat: port Order.Filter.Basic (#1750)

Added Filter.comap View on Github →