Finite set over infinite type

Stream: mathlib4

[Sebastian Zivota]

Is there a theorem asserting that for infinite α, ∀ (s : Finset α), ∃ (x : α), x ∉ s? If not, how would one go about proving that?

[Mario Carneiro]

if not then the set is finite by definition

[Sebastian Zivota]

For the sake of a concrete example, can I prove ∀ (s : Finset String), ∃ (x : α), x ∉ s?

[Mario Carneiro]

Oh I was assuming you have an actual assumption of the form Infinite A

[Mario Carneiro]

which probably exists for string, not sure

[Sebastian Zivota]

Thanks, that helps a lot already

[Mario Carneiro]

hm, docs4#Set.Infinite.exists_not_mem_finset looks close to what you want

[Mario Carneiro]

there is a proof that Nat and List A are infinite, but not String. It shouldn't be hard by applying the isomorphism from List Char

[Mario Carneiro]

oh, docs4#Infinite.exists_not_mem_finset is exactly the theorem you want

[Sebastian Zivota]

Excellent, thank you very much

[Sebastian Zivota]

Although there does indeed not seem to be an instance of Infinite String

[Kevin Buzzard]

I wouldn't get your hopes up regarding the existence of too many theorems about strings in mathlib4 :-)

[Mario Carneiro]

yeah, the people who care about strings don't talk to the people who care about infinitude :grinning_face_with_smiling_eyes:

[Johan Commelin]

[string theorists leave the room]

[Sebastian Zivota]

Fortunately it's easy to prove, should I open a PR?

[Mario Carneiro]

sure

[Kevin Buzzard]

to which repo? I'm not sure mathlib4 wants new material which isn't in mathlib3 right now

[Mario Carneiro]

yes, mathlib4 wants new material

[Kevin Buzzard]

This was not my understanding of what was going on right now. I thought the idea was to keep mathlib3 and mathlib4 in exact sync.

[Eric Wieser]

Why not put it in both?

[Kevin Buzzard]

Right -- that was the answer I was expecting.

[Eric Wieser]

If people want to not have to worry about mathlib3 any more, they should help with the port!

[Mario Carneiro]

I really do not want to encourage backports for everything, this is a lot more work and counterproductive besides

[Johan Commelin]

If you are starting a new file, I don't see any reason why it should be backported to ml3.

[Mario Carneiro]

if nothing in mathlib3 depends on it there is no need for a backport

[Kevin Buzzard]

I'm not sure we're starting a new file just containing the result that String is an infinite type!

[Ruben Van de Velde]

Well, why not? It's easy enough to merge it into some other file after the port is done

[Mario Carneiro]

mathlib4 is already not exactly 1-1 with align statements. The whole discussion seems silly to me, of course we should allow new material - there is already quite a bit of new material, in addition to tons of upstream new material

[Ruben Van de Velde]

Would std4 take the definition of Infinite? :innocent:

[Mario Carneiro]

and not allowing new material will set us back more than necessary

[Mario Carneiro]

Ruben Van de Velde said:

Would std4 take the definition of Infinite? :innocent:

the real question is whether it would be able to disentangle all the dependencies

[Mario Carneiro]

the definition of infinite itself isn't so bad but it depends on all the finiteness stuff

[Mario Carneiro]

James Gallicchio 's List.Perm PR is just one small part of this, it will take a while to work through all of it

[Sebastian Zivota]

https://github.com/leanprover-community/mathlib4/pull/1973

I put the mathlib4 version into Data.Fintype.Card, where the Infinite ℤ instance also lives. The proof can't be backported one-to-one because, as far as I can tell, Lean3/Mathlib3 doesn't have the String.replicate function.

[Ruben Van de Velde]

Anything called replicate in 4 was probably called repeat in 3

[Ruben Van de Velde]

Mario Carneiro said:

the definition of infinite itself isn't so bad but it depends on all the finiteness stuff

I wasn't really serious, but it's not that bad. It doesn't depend on Fintype, just Finite, which needs only Nat/Fin n (which are in core, I think) and Equiv (including Function.Left/RightInverse)