Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
grothendieck_universe [2014/12/07 22:33] nikolaj |
grothendieck_universe [2014/12/07 22:33] nikolaj |
||
|---|---|---|---|
| Line 13: | Line 13: | ||
| === Formalities === | === Formalities === | ||
| The symbol ${\approx}$ in the last postulate is an abbreviation. For subsets $Y$ of ${\mathfrak G}$, equinumerosity can be defined as the existence of a set of pairs, $f=\{\{y,u\},\{y',u'\},\dots\}$, which puts elements $y\in Y$ uniquely in correspondence with $u\in{\mathfrak G}$: | The symbol ${\approx}$ in the last postulate is an abbreviation. For subsets $Y$ of ${\mathfrak G}$, equinumerosity can be defined as the existence of a set of pairs, $f=\{\{y,u\},\{y',u'\},\dots\}$, which puts elements $y\in Y$ uniquely in correspondence with $u\in{\mathfrak G}$: | ||
| + | |||
| + | >I reverse-engineered this from the metamath page, so it needs to be checked. | ||
| + | |||
| $Y\ {\approx}\ {\mathfrak G}\equiv\exists f. \forall x.\left((x \in Y) \implies \exists!u.\ \{x, u\} \in f\right) \land \left((x \in {\mathfrak G}\setminus Y) \implies \exists(y \in Y).\ \{y,x\} \in f\right)$ | $Y\ {\approx}\ {\mathfrak G}\equiv\exists f. \forall x.\left((x \in Y) \implies \exists!u.\ \{x, u\} \in f\right) \land \left((x \in {\mathfrak G}\setminus Y) \implies \exists(y \in Y).\ \{y,x\} \in f\right)$ | ||
| The first clause says $f$ corresponds to a function $F$ and moreover implies $F(b) \in Y \implies F(F(b))=b$. The second says $F$ is surjective into ${\mathfrak G}\setminus Y$. | The first clause says $f$ corresponds to a function $F$ and moreover implies $F(b) \in Y \implies F(F(b))=b$. The second says $F$ is surjective into ${\mathfrak G}\setminus Y$. | ||
| - | |||
| - | >I reverse-engineered this from the metamath page, so it needs to be checked. | ||
| === Reference === | === Reference === | ||
