Def Filter.germSetoid

Modification history

2023-08-10 19:52

Mathlib/Order/Filter/Germ.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified Filter.germSetoid View on Github →

2023-02-15 08:14

Mathlib/Order/Filter/Germ.lean

feat: port Order.Filter.Germ (#1799)

Added Filter.germSetoid View on Github →