Lemma search

Stream: new members

[Jakub Kądziołka]

Hi, is there a way to ask Lean, say, "show me all lemmas that mention finset and the existential quantifier"? I'm trying to remove a specific element from a finset, and I can't see any function that would remove an element, so if the functionality is available, I'd assume it's in the form of some of existential statement

[Adam Topaz]

We have the #find command, but in this case, you could use docs#finset.filter and filter out everything equal to the element you want to drop.

[Adam Topaz]

I don't know off the top of my head if we have a better way to remove a single element from a finset.

[Adam Topaz]

Oh, nevermind, we have docs#finset.erase

[Adam Topaz]

Note that finset.erase shows up with this code:

import data.finset.basic

#find finset _ → _ → finset _