Theorem Ultrafilter.eventually_exists_mem_iff

Modification history

2025-01-21 12:39
Mathlib/Order/Filter/Ultrafilter/Basic.lean
chore: split Mathlib.Order.Filter.Ultrafilter (#20848)
Modified Ultrafilter.eventually_exists_mem_iffView on Github →
2025-01-02 11:03
Mathlib/Order/Filter/Ultrafilter.lean
feat(Order/Filter): add `Ultrafilter.eventually_exists_iff` (#20280)
Added Ultrafilter.eventually_exists_mem_iffView on Github →