Def Filter.pi

Modification history

2024-12-06 13:50

Mathlib/Order/Filter/Defs.lean

chore(Filter/Bases): split (#18450)

Modified Filter.pi View on Github →

2023-01-24 09:31

Mathlib/Order/Filter/Pi.lean

feat: port Order.Filter.Pi (#1802)

Added Filter.pi View on Github →