Description: Define a structure with
components in ![M M](_cm.gif) ![... ...](ldots.gif) . This is not a
requirement for groups, posets, etc., but it is a useful assumption for
component extraction theorems.
As mentioned in the section header, an "extensible structure should
be
implemented as a function (a set of ordered pairs)". The current
definition, however, is less restrictive: it allows for classes which
contain the empty set to be extensible structures. Because of
0nelfun 5149, such classes cannot be functions. Without
the empty set,
however, a structure must be a function, see structn0fun 12011:
Struct ![( (](lp.gif) ![{ {](lbrace.gif) ![(/) (/)](varnothing.gif) ![}
}](rbrace.gif) .
Allowing an extensible structure to contain the empty set ensures that
expressions like ![{ {](lbrace.gif) ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![>. >.](rangle.gif) ![<. <.](langle.gif) ![C C](_cc.gif) ![D D](_cd.gif) ![>. >.](rangle.gif) are structures
without asserting or implying that , ,
and are
sets (if or
is a proper class,
then ![<. <.](langle.gif) ![A A](_ca.gif) ![B B](_cb.gif) ,
see opprc 3734). (Contributed by Mario Carneiro,
29-Aug-2015.) |