Def Filter.rmap

Modification history

2023-02-12 15:02

Mathlib/Order/Filter/Partial.lean

chore: tidy various files (#2236)

Modified Filter.rmap View on Github →

2023-02-05 12:15

Mathlib/Order/Filter/Partial.lean

feat: port Order.Filter.Partial (#2059)

Added Filter.rmap View on Github →