Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
grothendieck_universe [2014/12/07 22:34] nikolaj |
grothendieck_universe [2014/12/10 11:14] 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 19: | Line 21: | ||
| 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 33: | ||
| [[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) | ||
| + | |||
| + | nLab: | ||
| + | [[http://ncatlab.org/nlab/show/Grothendieck+universe|Grothendieck universe]] | ||
| ==== Parents ==== | ==== Parents ==== | ||
| === Requirements === | === Requirements === | ||
| [[Bijective function]], [[Power set]] | [[Bijective function]], [[Power set]] | ||
