Theorem Filter.mem_pure

Modification history

2024-10-19 06:27

Mathlib/Order/Filter/Basic.lean

refactor(Order/Filter): don't use `generate` for `CompleteLattice` (#17799)

Modified Filter.mem_pure View on Github →

2023-01-23 08:16

Mathlib/Order/Filter/Basic.lean

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

Added Filter.mem_pure View on Github →