Zulip Chat Archive

Stream: general

Topic: min_injective

Yaël Dillies (Jun 13 2021 at 18:51):

Is there any reason why min_injective is stated as
theorem min_injective (I : nonempty ι) : ∃ i, nonempty (∀ j, β i ↪ β j) :=
and not
theorem min_injective (I : nonempty ι) : ∃ i, ∀ j, nonempty (β i ↪ β j) :=
This came up in (unrelated) PR #7900.

Yaël Dillies (Jun 13 2021 at 20:14):

And what about the plain ∃ i, ∀ j, β i ↪ β j?

Patrick Massot (Jun 13 2021 at 20:16):

git blame says you should ask @Mario Carneiro

Patrick Massot (Jun 13 2021 at 20:17):

But it also says Mario wrote that in 2017 so maybe we'll need a time machine.

Eric Wieser (Jun 13 2021 at 20:18):

Exists can't contain data, which rules out the version without nonempty

Mario Carneiro (Jun 13 2021 at 20:18):

The first one is a stronger claim than the second

Mario Carneiro (Jun 13 2021 at 20:18):

well, classically they are equivalent but that's full choice right there

Patrick Massot (Jun 13 2021 at 20:19):

Mario Carneiro said:

well, classically they are equivalent but that's full choice right there

I should have guess that word would appear instead of scratching my head

Mario Carneiro (Jun 13 2021 at 20:19):

I don't even mean it in the constructive sense, this is pure set theory

Mario Carneiro (Jun 13 2021 at 20:20):

I mean AC the way mathematicians know it

Yaël Dillies (Jun 13 2021 at 20:20):

Ah yeah, quantification order, of course :grinning:

Mario Carneiro (Jun 13 2021 at 20:20):

plus I think this order is the version I needed for a proof

Yaël Dillies (Jun 13 2021 at 20:21):

I am just being a nonconstructivist fuss, forget me :smile:

Eric Rodriguez (Jun 13 2021 at 23:44):

i'm surprised this quantifier difference is choice, that's insanity

Mario Carneiro (Jun 14 2021 at 07:13):

Really? It's one of the more well known forms of choice: if for every x, A(x) is nonempty, then Pi x, A(x) is nonempty

Mario Carneiro (Jun 14 2021 at 07:13):

if you think about it for a bit it's really just a fancy way to say you can construct a function making an infinite family of choices

Mario Carneiro (Jun 14 2021 at 07:15):

https://en.wikipedia.org/wiki/Axiom_of_choice#Equivalents

The Cartesian product of any family of nonempty sets is nonempty.

Mario Carneiro (Jun 14 2021 at 07:16):

it's also fairly close to docs#classical.axiom_of_choice which is presented exactly as a quantifier commutation

Johan Commelin (Jun 14 2021 at 07:18):

@Eric Rodriguez This just shows the well-known fact that the axiom of choice is obviously true

Mario Carneiro (Jun 14 2021 at 07:20):

The axiom of choice is obviously true, the well-ordering principle obviously false, and who can tell about Zorn's lemma? — Jerry Bona

Last updated: Dec 20 2023 at 11:08 UTC