Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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:34]
nikolaj
Line 14: Line 14:
 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)$
Link to graph
Log In
Improvements of the human condition