logo

Context: proveit.logic.set_theory.comprehension

Subset comprehension is a way to define a subset of a set by listing properties/conditions of the elements of the subset. For example, $\{x~|~Q(x)\}_{x \in S}$, is the subset of $S$ for which every element $x$ satisfies the condition $Q(x)$. It is important that no universal set be defined or it would be possible to define Russel's set which would introduce a parodox into the system (and allow $\top = \bot$ to be proven). As long as all sets are properly defined, subset comprehension will be safe.

More generally, comprehension may define a set by mapping subset elements via some function. For example, $\{f(x)~|~Q(x)\}_{x \in S}$ is the set that contains only and all $f(x)$ elements such that $x \in S$ and $Q(x)$ is TRUE. This furthermore generalizes to mapping any number of elements and specifying any number of conditions. For example, $\{f(x, y)~|~Q(x, y), R(x, y)\}_{x, y \in S}$ is the set that contains only and all of $f(x, y)$ elements such that $x \in S$, $y \in S$, $Q(x, y)$, and $R(x, y)$. It is also possible not to specify any conditions and simply define a direct map of a set: $\{f(x)\}_{x \in S}$ or $\{f(x, y)\}_{x, y \in S}$.

In [1]:
import proveit
%context