Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
ordered_pair [2013/09/05 02:31] nikolaj |
ordered_pair [2013/09/06 21:49] nikolaj |
||
---|---|---|---|
Line 13: | Line 13: | ||
See also [[http://en.wikipedia.org/wiki/Ordered_pair#Kuratowski_definition|Wikipedia: Ordered pair, Kuratowski defintion]]. In calculations, only this property of it should be used. | See also [[http://en.wikipedia.org/wiki/Ordered_pair#Kuratowski_definition|Wikipedia: Ordered pair, Kuratowski defintion]]. In calculations, only this property of it should be used. | ||
- | === Definitions === | + | Now Let $x_i$ be indexed sets and define $p \equiv \langle x_1,x_2\rangle$. |
- | + | ||
- | Let | + | |
- | + | ||
- | ^ $x_i$ ^ | + | |
- | + | ||
- | and define | + | |
- | + | ||
- | ^ $p \equiv \langle x_1,x_2\rangle$ ^ | + | |
//Canonical projection//: Using [[arbitrary union]] and [[arbitrary intersection]], we can extract the first and second component of the pair: | //Canonical projection//: Using [[arbitrary union]] and [[arbitrary intersection]], we can extract the first and second component of the pair: | ||
Line 39: | Line 31: | ||
=== Reference === | === Reference === | ||
- | Mizar files: [[http://markun.cs.shinshu-u.ac.jp/mirror/mizar/JFM/Axiomatics/tarski.html|TARSKI]], [[http://markun.cs.shinshu-u.ac.jp/mirror/mizar/JFM/Vol1/relat_1.html|RELAT_1]], [[http://mizar.org/JFM/Vol1/mcart_1.html|MCART_1]] | ||
- | |||
Wikipedia: [[http://en.wikipedia.org/wiki/Ordered_pair|Ordered pair]] | Wikipedia: [[http://en.wikipedia.org/wiki/Ordered_pair|Ordered pair]] | ||
- | + | ==== Parents ==== | |
- | ==== Context ==== | + | |
=== Requirements === | === Requirements === | ||
[[Unordered pair]] | [[Unordered pair]] | ||