Looking for a name

[Thomas Brendan Leahy]

So while working on one of my lemmata for something else, I realized I would need something like this statement seven times (y allowed in C):

( ( A e. Fin /\ A ~~ B ) -> ( A. x e. A E. y e. B  x = C -> A. x e. A E* y e. B x = C ) )

And that this might be useful elsewhere, so I decided to take it out of my naming scheme, but the best I can come up with is "finenralrexinvrmo," which seems a bit much.  I guess it could be considered a version of the pigeonhole principle, if you squint...?  (And yes, I realize that the restriction on the universal in the consequent is unnecessary, but the only way I could work out to prove that has this as an intermediate step, and it's relatively easy from there, so I figured it was best left here.)

[Benoit]

( ( A e. Fin /\ A ~~ B ) -> ( A. x e. A E. y e. B  x = C -> A. x e. A E* y e. B x = C ) )

I think this lemma is natural enough to be in the main part of set.mm.  I would replace E* with E! : it strengthens the result, and more importantly, E! is standard throughout mathematics, whereas E* is not. The way I view it is to consider C as a function of y, and then it says: if a function between two equinumerous finite sets is surjective, then it is bijective.  So maybe ~ finsurjbij ?

Benoît

[Mario Carneiro]

if you make the RHS a E!, then you can also make it a biconditional, which I think is nicer here. It's starting to look a lot like the pigeonhole principle now; there's a little group of these facts around php3 or so and you could crib the name from one of them.

Mario

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b3fe812d-ffbc-4c76-986a-d235736fe210%40googlegroups.com.

[Thomas Brendan Leahy]

While I can see the argument for going with uniqueness, I have to question the utility in making it a biconditional, since it's so obvious (and quick to show) in that case that the consequent implies the antecedent.

I probably won't go with anything that implies a function, since the fact that it's not syntactically a function is ultimately what made this fact unwieldy enough to split off in the first place.

On Tuesday, October 22, 2019 at 8:28:53 AM UTC-4, Mario Carneiro wrote:

if you make the RHS a E!, then you can also make it a biconditional, which I think is nicer here. It's starting to look a lot like the pigeonhole principle now; there's a little group of these facts around php3 or so and you could crib the name from one of them.

Mario

On Tue, Oct 22, 2019 at 8:02 AM Benoit <benoi...@gmail.com> wrote:

( ( A e. Fin /\ A ~~ B ) -> ( A. x e. A E. y e. B  x = C -> A. x e. A E* y e. B x = C ) )

I think this lemma is natural enough to be in the main part of set.mm.  I would replace E* with E! : it strengthens the result, and more importantly, E! is standard throughout mathematics, whereas E* is not. The way I view it is to consider C as a function of y, and then it says: if a function between two equinumerous finite sets is surjective, then it is bijective.  So maybe ~ finsurjbij ?

Benoît

--
You received this message because you are subscribed to the Google Groups "Metamath" group.

To unsubscribe from this group and stop receiving emails from it, send an email to meta...@googlegroups.com.

[Benoit]

Actually, I would go for the biconditional, as Mario suggests, since it's always nicer to have a characterization.  The useful part is indeed the forward implication, since the reverse implication is always true and obvious and easy to prove, but I think this is not a reason to keep it out of set.mm

Benoît