Get ℕ that is ∉ finset

Stream: new members

[Marcus Rossel]

Given f : finset ℕ, how can one obtain an x : ℕ with x ∉ f?
Since f is finite, there must exists such an x, but I'm struggling to obtain one.
My idea would be to get the maximal element m in f and then set x := m + 1. One could then prove that all elements in f have the property of being less than m, and since x does not, it can't be an element in f.
But this seems pretty contrived to me.
Is there an easier way, that I'm overlooking?

[Johan Commelin]

Well, you'll have to use that nat is infinite.

[Johan Commelin]

That's in data.fintype.basic

[Johan Commelin]

docs#finset.not_mem_range_self

[Johan Commelin]

together with docs#finset.subset_range_sup_succ

[Mario Carneiro]

That should be a theorem about infinite

[Mario Carneiro]

And it already exists: docs#infinite.exists_not_mem_finset

[Marcus Rossel]

Ah dang it, I was almost done with the lemma :D

[Marcus Rossel]

Thanks!

[Mario Carneiro]

It's pretty easy to prove by contrapositive, since otherwise f enumerates the type

[Marcus Rossel]

Mario Carneiro said:

It's pretty easy to prove by contrapositive, since otherwise f enumerates the type

How would one prove that kind of thing?

[Mario Carneiro]

lemma exists_not_mem_finset [infinite α] (s : finset α) : ∃ x, x ∉ s :=
not_forall.1 $ λ h, not_fintype ⟨s, h⟩

[Mario Carneiro]

not_forall is proving exists by contradiction, not_fintype is the definition of infinite, and the "meat" of the proof is literally the constructor for fintype, hence ⟨s, h⟩

[Marcus Rossel]

I have much to learn :D

[Ruben Van de Velde]

That's what we call a proof that's not optimized for reading :)

The thing I still missed after the explanation is that fintype is defined as "there's a finset (s) that contains all the values of the type (h)"

[Mario Carneiro]

I prefer the term "slick proof" :)

[Kevin Buzzard]

The thing I like about slick proofs is that they are perfect for situations where the statement you're proving is mathematically trivial, because they say "yes, our system and our library makes this a triviality just as it should be", and furthermore it doesn't matter if the proof is obfuscated because the result is trivial so you will not learn anything mathematically from the proof anyway, hence it doesn't need to be read