A subset of a given set is a set that may be viewed as contained within .
In material set theory, a subset of a set is a set with the property that
for any object whatsoever. One writes or (depending on the author) if has this property. Set theory's axiom of extensionality says that if (and only if) and (although this is only strong enough for well-founded set?s).
In structural foundations of mathematics, this definition doesn't make sense, because there is no global membership predicate (and there may not be a global equality predicate either). Accordingly, we define a subset of to be a set with the structure of an injection
We can still define a local membership predicate as follows: Given an element of and a subset (technically, ) of ,
Similarly, we can define a local containment predicate as follows: Given subsets and of ,
We can also define a local equality predicate on subsets of :
In foundations that already have a global equality predicate on sets (and functions between equal sets), this local equality predicate must be interpreted as an equivalence relation; then a subset of is technically an equivalence class of injections to rather than simply an injection to .
In any case, if is a subset of , then is a superset of .
In homotopy type theory, the inclusion relation between two types and is defined as
A subset of a set is a set with a term .
Every subset of in a universe comes with a choice of injection if and only if the axiom of choice holds for sets in the universe:
As a result, subsets equipped with an injection are typically used when doing mathematics in homotopy type theory.
As you can see from the right-hand sides of the above sequence of definitions, one usually suppresses the subscript from the notation. Even the right-hand side of (1) may use a local equality relation on elements of . It may be necessary to distinguish (the typing declaration introducing a variable for an element of a given set ) from (the proposition that a given element of a given set is a member of a given subset of ). Some authors may use for either or both of these, trusting on context (particularly whether has been introduced before) to distinguish them. Another notational convenience is to suppress the injection , writing instead of .
The concept of subset as it appears here generalises to subobject in category theory. To be precise, a subset of is exactly a subobject of when is thought of as an object of the category Set. The concept of superset then generalises to a notion of extension analogous to that of field extension.
When the abstract set is fixed, a subset of may be thought of as a concrete set.
Last revised on May 26, 2022 at 19:46:41. See the history of this page for a list of all contributions to it.