mathlib3
ed33fcf8 - feat(order/filter/*): a family of pairwise disjoint filters has a family of pairwise disjoint members (#16504)

Commit
3 years ago
feat(order/filter/*): a family of pairwise disjoint filters has a family of pairwise disjoint members (#16504)
Author
Parents
Loading