Def interPairsFilter

Modification history

2026-10-13 14:51
Mathlib/Order/Filter/Ultrafilter/Cardinality.lean
refactor(Data): make `Set` a one-field structure (#41506) …
Deleted interPairsFilterView on Github →
2026-09-04 11:59
Mathlib/Order/Filter/Ultrafilter/Cardinality.lean
feat: cardinality of `Ultrafilter` (#41297) …
Added interPairsFilterView on Github →