ThmDex – An index of mathematical definitions, results, and conjectures.
Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Binary cartesian set product
Binary relation
Map
Definition D43
Inclusion map
Formulation 0
Let $X$ be a D11: Set such that
(i) $E \subseteq X$
The inclusion map from $E$ to $X$ is the D18: Map \begin{equation} E \to X, \quad x \mapsto x \end{equation}
Subdefinitions
D440: Identity map