Theorem Filter.isOpen_setOf_mem

Modification history

2026-07-17 09:57

Mathlib/Topology/Filter.lean

chore(Data): rename `setOf` to `Set.ofPred` (#41507) …

Deleted Filter.isOpen_setOf_mem View on Github →

2023-02-08 05:05

Mathlib/Topology/Filter.lean

feat: port Topology.Filter (#2117)

Added Filter.isOpen_setOf_mem View on Github →