Zulip Chat Archive

Stream: new members

Topic: complement of finset


view this post on Zulip Heather Macbeth (Jun 27 2020 at 01:05):

I have a type ι and functions f : ι → ℝ and g : ι → ℝ. I want to state that for all but finitely many x : ι, it is true that f x ≤ g x. I can see one way of doing this,

 (s : finset ι) (h :  (i:ι), i  s  f i  g i)

but is there a more idiomatic way?

view this post on Zulip Adam Topaz (Jun 27 2020 at 01:23):

You could say that the set of i for which the condition does not hold is the coersion of some finset. I'm not sure which one would be better...

view this post on Zulip Reid Barton (Jun 27 2020 at 01:33):

I guess eventually is for things like this.

view this post on Zulip Heather Macbeth (Jun 27 2020 at 01:34):

Reid, can you tell me the syntax? I had that idea but could not figure out how to phrase it.

view this post on Zulip Adam Topaz (Jun 27 2020 at 01:37):

Does mathlib know that cofinite sets form a filter?

view this post on Zulip Reid Barton (Jun 27 2020 at 01:37):

I haven't used it myself

view this post on Zulip Reid Barton (Jun 27 2020 at 01:37):

yes, should be cofinite

view this post on Zulip Reid Barton (Jun 27 2020 at 01:38):

Maybe ∀ᶠ i in cofinite, f i <= g i

view this post on Zulip Heather Macbeth (Jun 27 2020 at 01:40):

Yup, I was just off trying that and it works. Thank you!

view this post on Zulip Patrick Massot (Jun 27 2020 at 07:35):

Very soon you'll be able to use https://github.com/leanprover-community/mathlib/pull/3172/files#diff-63a3fd7051270b9139b68fd8b4e04bc0R51-R54 (not in mathlib yet).


Last updated: May 08 2021 at 08:12 UTC