Description: Define a structure with
components in 𝑀...𝑁. 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 6560, such classes cannot be functions. Without
the empty set,
however, a structure must be a function, see structn0fun 17093:
𝐹
Struct 𝑋 → Fun (𝐹 ∖ {∅}).
Allowing an extensible structure to contain the empty set ensures that
expressions like {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} are structures
without asserting or implying that 𝐴, 𝐵, 𝐶 and 𝐷 are
sets (if 𝐴 or 𝐵 is a proper class, then
⟨𝐴,
𝐵⟩ = ∅,
see opprc 4891). This is used critically in strle1 17100, strle2 17101,
strle3 17102 and strleun 17099 to avoid sethood hypotheses on the
"payload"
sets: without this, ipsstr 17290 and theorems like it will have many sethood
assumptions, and may not even be usable in the empty context. Instead,
the sethood assumption is deferred until it is actually needed, e.g.,
ipsbase 17291, which requires that the base set be a set
but not any of the
other components. Usually, a concrete structure like ℂfld does not
contain the empty set, and therefore is a function, see cnfldfun 21254.
(Contributed by Mario Carneiro, 29-Aug-2015.) |