nLab bottom

Idea

In a poset $P$, a bottom is a least element: an element $\bot$ of $P$ such that $\bot \leq a$ for every element $a$. Such a bottom may not exist; if it does, then it is unique.

In a proset, a bottom may be defined similarly, but it need not be unique. (However, it is still unique up the natural equivalence in the proset.)

A bottom of $P$ can also be understood as a join of zero elements in $P$.

A poset that has both top and bottom is called bounded.

As a poset is a special kind of category, a bottom is simply an initial object in that category.

The bottom of the poset of subsets or subobjects of a given set or object $A$ is called the empty subset or subobject. In a category (such as Set) with a strict initial object $\varnothing$, this will always serve as the bottom of any subobject poset.

Related concepts

$\phantom{-}$symbol$\phantom{-}$	$\phantom{-}$in logic$\phantom{-}$
$\phantom{A}$$\in$	$\phantom{A}$element relation
$\phantom{A}$$\,:$	$\phantom{A}$typing relation
$\phantom{A}$$=$	$\phantom{A}$equality
$\phantom{A}$$\vdash$$\phantom{A}$	$\phantom{A}$entailment / sequent$\phantom{A}$
$\phantom{A}$$\top$$\phantom{A}$	$\phantom{A}$true / top$\phantom{A}$
$\phantom{A}$$\bot$$\phantom{A}$	$\phantom{A}$false / bottom$\phantom{A}$
$\phantom{A}$$\Rightarrow$	$\phantom{A}$implication
$\phantom{A}$$\Leftrightarrow$	$\phantom{A}$logical equivalence
$\phantom{A}$$\not$	$\phantom{A}$negation
$\phantom{A}$$\neq$	$\phantom{A}$negation of equality / apartness$\phantom{A}$
$\phantom{A}$$\notin$	$\phantom{A}$negation of element relation $\phantom{A}$
$\phantom{A}$$\not \not$	$\phantom{A}$negation of negation$\phantom{A}$
$\phantom{A}$$\exists$	$\phantom{A}$existential quantification$\phantom{A}$
$\phantom{A}$$\forall$	$\phantom{A}$universal quantification$\phantom{A}$
$\phantom{A}$$\wedge$	$\phantom{A}$logical conjunction
$\phantom{A}$$\vee$	$\phantom{A}$logical disjunction
symbol	in type theory (propositions as types)
$\phantom{A}$$\to$	$\phantom{A}$function type (implication)
$\phantom{A}$$\times$	$\phantom{A}$product type (conjunction)
$\phantom{A}$$+$	$\phantom{A}$sum type (disjunction)
$\phantom{A}$$0$	$\phantom{A}$empty type (false)
$\phantom{A}$$1$	$\phantom{A}$unit type (true)
$\phantom{A}$$=$	$\phantom{A}$identity type (equality)
$\phantom{A}$$\simeq$	$\phantom{A}$equivalence of types (logical equivalence)
$\phantom{A}$$\sum$	$\phantom{A}$dependent sum type (existential quantifier)
$\phantom{A}$$\prod$	$\phantom{A}$dependent product type (universal quantifier)
symbol	in linear logic
$\phantom{A}$$\multimap$$\phantom{A}$	$\phantom{A}$linear implication$\phantom{A}$
$\phantom{A}$$\otimes$$\phantom{A}$	$\phantom{A}$multiplicative conjunction$\phantom{A}$
$\phantom{A}$$\oplus$$\phantom{A}$	$\phantom{A}$additive disjunction$\phantom{A}$
$\phantom{A}$$\&$$\phantom{A}$	$\phantom{A}$additive conjunction$\phantom{A}$
$\phantom{A}$$\invamp$$\phantom{A}$	$\phantom{A}$multiplicative disjunction$\phantom{A}$
$\phantom{A}$$\;!$$\phantom{A}$	$\phantom{A}$exponential conjunction$\phantom{A}$
$\phantom{A}$$\;?$$\phantom{A}$	$\phantom{A}$exponential disjunction$\phantom{A}$