## Stream: new members

### Topic: complement of finset

#### 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?

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

#### Reid Barton (Jun 27 2020 at 01:33):

I guess eventually is for things like this.

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

#### Adam Topaz (Jun 27 2020 at 01:37):

Does mathlib know that cofinite sets form a filter?

#### Reid Barton (Jun 27 2020 at 01:37):

I haven't used it myself

#### Reid Barton (Jun 27 2020 at 01:37):

yes, should be cofinite

#### Reid Barton (Jun 27 2020 at 01:38):

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

#### Heather Macbeth (Jun 27 2020 at 01:40):

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

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