nLab empty family

Contents

Contents

Idea

Given any set XX, there is a unique empty family of elements of XX. Formally, this is given by the empty function to XX, the unique function to XX from the empty set. As the empty set is finite and (a fortiori) countable, this empty family counts as a list (or tuple) and a stream; in such a guise it is known as the empty list (or 00-tuple) or the empty stream (or empty sequence if the term ‘sequence’ is used in a sufficiently general sense).

When treating it as an element of the free monoid on XX, the empty list may be written ()(), **, or ϵ\epsilon, perhaps with a subscript XX if desired. (Thinking of all empty lists, regardless of the underlying set, as equal is like thinking of all empty subsets as equal.)

Besides empty families of elements of sets, we have the notions of the empty family of elements of a given proper class, the empty family of elements of a given preset, the empty family of term of a given type, the empty family of objects and the empty family of morphisms of a given category, and more generally the empty family of whatever you want.

Last revised on October 4, 2019 at 08:59:27. See the history of this page for a list of all contributions to it.