complement of finset

Stream: new members

[Heather Macbeth]

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?

[Adam Topaz]

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...

[Reid Barton]

I guess eventually is for things like this.

[Heather Macbeth]

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

[Adam Topaz]

Does mathlib know that cofinite sets form a filter?

[Reid Barton]

I haven't used it myself

[Reid Barton]

yes, should be cofinite

[Reid Barton]

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

[Heather Macbeth]

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

[Patrick Massot]

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