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 15: | Line 15: | ||
>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)$ |