Zulip Chat Archive

Stream: general

Topic: list of filters

Yury G. Kudryashov (Aug 14 2020 at 05:19):

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 (Aug 14 2020 at 09:08):

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 (Aug 14 2020 at 13:37):

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 (Aug 14 2020 at 14:02):

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

Last updated: Dec 20 2023 at 11:08 UTC