Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-08 22:15 ce999a89

View on Github →

feat(topology/basic): add is_open_iff_ultrafilter (#4529) Requested on Zulip by Adam Topaz

Estimated changes

Modified src/order/filter/ultrafilter.lean

added theorem filter.le_iff_ultrafilter

added theorem filter.mem_iff_ultrafilter

Modified src/topology/basic.lean

added theorem is_open_iff_ultrafilter