Definition talk:Well-Defined
Jump to navigation
Jump to search
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)