Theorem Filter.hasBasis_pure

Modification history

2023-11-16 19:44

Mathlib/Order/Filter/Bases.lean

style: cleanup by putting `by` on the same line as `:=` (#8407)

Modified Filter.hasBasis_pure View on Github →

2023-01-24 07:28

Mathlib/Order/Filter/Bases.lean

Feat: port Order.Filter.Bases (#1791)

Added Filter.hasBasis_pure View on Github →