Ciro Santilli @cirosantilli 37

Much of this section will be dumped at Section "Website front-end for a mathematical formal proof system" instead.

A proof in some system for the formalization of mathematics.

A theorem that is not very important on its own, often an intermediate step to proving something that the author feels deserves the name "theorem".

Intuitively: unordered container where all the values are unique, just like C++ std::set.

More precisely for set theory formalization of mathematics:

Set of ordered pairs. That's it! This is illustrated at: math.stackexchange.com/questions/1480651/is-fx-x-1-x-2-a-function/1481099#1481099

Most notable example: $L^2$.

An ordered pair of two real numbers with the complex addition and multiplication defined.

Forms both a:

Sets are unordered, but we can use them to create ordered objects, which are of fundamental importance. Notably, they are used in the definition of functions.