Zulip Chat Archive

Stream: new members

Topic: making a well-defined definition


view this post on Zulip Ali Sever (Aug 05 2018 at 08:13):

I have two sets A B and I want to define f A B = g A b(another set) for some b ∈ B. I have the fact that ∃ b, b ∈ B, but I'm not allowed to use Exists.dcases_on. Also, how/when do I prove this is well-defined and doesn't depend on the choice of b?

view this post on Zulip Chris Hughes (Aug 05 2018 at 08:49):

You can use classical.some in which case you don't have to prove that it's well defined. Alternatively, if the possible values for B form a partition, you could use quotients.

view this post on Zulip Ali Sever (Aug 05 2018 at 08:50):

I can prove that every value gives the same result.

view this post on Zulip Chris Hughes (Aug 05 2018 at 08:56):

Presumably then, it isn't defined or at least used on any sets, just sets that meet some criteria?

view this post on Zulip Ali Sever (Aug 05 2018 at 09:10):

Yep, (lines)

view this post on Zulip Chris Hughes (Aug 05 2018 at 09:15):

If you want it to be defined on the set you pretty much have to use classical.some

view this post on Zulip Kevin Buzzard (Aug 05 2018 at 09:15):

You can't get data (the set) from a proof (the fact that there exists a b) constructively -- even if you can prove uniqueness results. I've been using cases (classical.indefinite_description _ H) with b Hb to get b out of the hypothesis H that b exists, recently, but I found a glitch with this idiom recently; it doesn't always do quite what I want it to. Might work here though.

view this post on Zulip Kevin Buzzard (Aug 05 2018 at 09:18):

The problem is that if you imagine a function as a computer program, the proof that a number exists (like Waring's number G(3) in my Monday talk) doesn't give you the right to be able to compute it for free.

view this post on Zulip Chris Hughes (Aug 05 2018 at 09:22):

A lot of the time when you know something exists, you can compute it however, because that's how you proved it exists. I'm guessing Ali might be in this situation.

view this post on Zulip Ali Sever (Aug 05 2018 at 09:23):

I just want to use the existence to show the set is non-empty. I think I might have to define the thing I want in a different way, and show it's equal to what I wanted.

view this post on Zulip Kevin Buzzard (Aug 05 2018 at 10:20):

Computing the set can't be done constructively, but I should think that proving it's non-empty might be possible. If your goal is the assertion that some set is non-empty then you'll be able to uses cases on the exists normally, because your goal is to prove a proposition, not to construct some data.


Last updated: May 18 2021 at 17:44 UTC