Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
grothendieck_universe [2014/12/07 22:33] nikolaj |
grothendieck_universe [2015/08/24 19:32] nikolaj |
||
---|---|---|---|
Line 5: | Line 5: | ||
| @#FFFDDD: forall | @#FFFDDD: $X\in{\mathfrak G}$ | | | @#FFFDDD: forall | @#FFFDDD: $X\in{\mathfrak G}$ | | ||
| @#55EE55: postulate | @#55EE55: $\mathcal{P}(X) \subseteq{\mathfrak G}$ | | | @#55EE55: postulate | @#55EE55: $\mathcal{P}(X) \subseteq{\mathfrak G}$ | | ||
+ | | @#FFFDDD: forall | @#FFFDDD: $x\in X$ | | ||
+ | | @#55EE55: postulate | @#55EE55: $x\in{\mathfrak G}$ | | ||
| @#FFFDDD: exists | @#FFFDDD: $P\in{\mathfrak G}$ | | | @#FFFDDD: exists | @#FFFDDD: $P\in{\mathfrak G}$ | | ||
| @#55EE55: postulate | @#55EE55: $\mathcal{P}(X) \subseteq P$ | | | @#55EE55: postulate | @#55EE55: $\mathcal{P}(X) \subseteq P$ | | ||
Line 10: | Line 12: | ||
| @#55EE55: postulate | @#55EE55: $Y \subseteq {\mathfrak G} \implies Y\ {\approx}\ {\mathfrak G}\lor Y \in {\mathfrak G} $ | | | @#55EE55: postulate | @#55EE55: $Y \subseteq {\mathfrak G} \implies Y\ {\approx}\ {\mathfrak G}\lor Y \in {\mathfrak G} $ | | ||
- | ==== Discussion ==== | + | ----- |
- | === Formalities === | + | === Discussion === |
+ | == 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. | + | >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$. | ||
+ | |||
+ | >strangely, to me, the metamath defintion doesn't include transitivity in an obvious way, and I can't see it... I added it here anyway, since it's part of any other definition I've seen. | ||
=== Reference === | === Reference === | ||
Line 29: | Line 34: | ||
[[http://us.metamath.org/mpeuni/grothprim.html|grothprim]] (long), | [[http://us.metamath.org/mpeuni/grothprim.html|grothprim]] (long), | ||
[[http://us.metamath.org/mpeuni/axgroth5.html|axgroth5]] (the one above) | [[http://us.metamath.org/mpeuni/axgroth5.html|axgroth5]] (the one above) | ||
- | ==== Parents ==== | + | |
+ | nLab: | ||
+ | [[http://ncatlab.org/nlab/show/Grothendieck+universe|Grothendieck universe]] | ||
+ | |||
+ | ----- | ||
=== Requirements === | === Requirements === | ||
[[Bijective function]], [[Power set]] | [[Bijective function]], [[Power set]] |