Definition talk:Well-Defined

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)