Structure embedding (source code)

= Structure embedding
{title2=$f:\mathcal M\hookrightarrow\mathcal N$}

A structure embedding is an injective map respecting constants and operations and preserving and reflecting relations. Equivalently it preserves all <atomic formulas> and their negations. It identifies the source with a <substructure> of the target. An <elementary embedding> additionally preserves every <first-order formula>.