Zulip Chat Archive

Stream: new members

Topic: Set builder for finset

Bjørn Kjos-Hanssen (Sep 13 2021 at 07:02):

This seemed hard to find by searching... how do we get {k : ℕ | k < x ∧ condition k}, where x: ℕ and condition is just some condition, as a finset?

Bjørn Kjos-Hanssen (Sep 13 2021 at 07:04):

(deleted)

Mario Carneiro (Sep 13 2021 at 07:10):

You have to use finset.filter

Last updated: Dec 20 2023 at 11:08 UTC