list of filters

Stream: general

[Yury G. Kudryashov]

I've started a gist with two lists: a list of useful filters and a list of statements formulated with filters, then reformulated without filters. What do you think about including (an extended/improved version of) this list in some docs? @Patrick Massot @Sebastien Gouezel

[Patrick Massot]

The fist list uses the old notation for complement. I think both lists are useful, but the second one is a bit messy, and would be more useful if it included references to lemmas.

[Yury G. Kudryashov]

Notation: fixed. The second one is messy, not "a bit" messy. Probably it should be organized into some sections (especially if expanded). The goal is to have some dictionary that people who never used filters can use to (a) understand mathlib theorems; (b) formulate their statements with filters.

[Yury G. Kudryashov]

BTW, is there any (draft) text about filters for MIL?