Definition talk:Well-Defined

From ProofWiki
Jump to navigation Jump to search

If an "unambiguous" relation is different from a "well-defined" relation, why the need to disambiguate? --prime mover (talk) 21:19, 6 February 2013 (UTC)

I've seen "well defined" to mean "unambiguous", like in Definition:Inversion Mapping. Or is that using well-defined like it is on this page? --GFauxPas (talk) 21:27, 6 February 2013 (UTC)
Strictly speaking, the meaning as on Definition:Inversion Mapping is the same as for quotient relations - but with the admittedly trivial case of the diagonal equivalence relation. Perhaps we could say a "multifunction $f$ is well-defined (for $\mathcal R$) iff $(x,y) \in \mathcal R$ implies $f(x) = f(y)$" where $\mathcal R$ is an equivalence. --Lord_Farin (talk) 22:07, 6 February 2013 (UTC)
Okay, so maybe not "disambiguate", but add an "also defined as" to indicate that it means the same as "unambiguous". But you then have to go and define what "unambiguous" means - no such definition exists on this site, and I for one have no intuitive idea as to what it might mean. --prime mover (talk) 22:20, 6 February 2013 (UTC)

General Concept

Would it be fair to say that the essential concept here is that the notation:

Let $a$ be the object such that $P(a)$
Lemma: $a$ is well-defined.
Proof: $\cdots \vdash (\exists x: P(x)) \land (\forall y: (P(y) \implies y = x))$

is just another way of saying:

Lemma: There exists a unique object $x$ such that $P(x)$
Proof: $\cdots \vdash (\exists x: P(x)) \land (\forall y: (P(y) \implies y = x))$
Let $a$ be the object such that $P(a)$. (where we presumably do something with uniqueness to allow $a$ to break free from the existential instantiation).

-- Dfeuer (talk) 19:18, 12 March 2013 (UTC)

Not really.
It is a specific statement about mappings and operations on equivalence classes.
What "well-defined" means is: for all elements of a given set, performing operation $f$ on those elements always results in the same result. "$f$ is well-defined on $S$" means: $\exists y: \forall x \in S: f \left({x}\right) = y$.
In the context within which it is used, $S$ is usually an equivalence class; in its rawest form, that equivalence class is that induced by the mapping. --prime mover (talk) 19:47, 12 March 2013 (UTC)
More adequate would be, in the usual case of an equivalence relation $\sim$ with quotient map $q: S \to S / \sim$, to say that a proof of well-definedness is a proof that a map $f: S \to T$ factors through $q$, i.e. there is $\tilde f: S / \sim \to T$ such that $f = \tilde f \circ q$. It is usual to define $\tilde f$ in terms of $f$ because of conceptual simplicity. — Lord_Farin (talk) 21:53, 12 March 2013 (UTC)