| Description: Define indexed union.
Definition indexed union in [Stoll] p. 45. In
most applications, A
is independent of x (although
this is not
required by the definition), and B depends on x i.e. can be read
informally as B(x). We call x the index, A the index
set, and B the indexed
set. In most books, x ∈ A is
written as
a subscript or underneath a union symbol ∪. We use a special
union symbol ∪ to make
it easier to distinguish from plain class
union. In many theorems, you will see that x and A are in the
same distinct variable group (meaning A cannot depend on x) and
that B and x do not share a distinct variable
group (meaning
that can be thought of as B(x) i.e.
can be substituted with a
class expression containing x). An alternate definition tying
indexed union to ordinary union is dfiun2 4002. Theorem uniiun 4020 provides
a definition of ordinary union in terms of indexed union. Theorems
fniunfv 5467 and funiunfv 5468 are useful when B is a function.
(Contributed by NM, 27-Jun-1998.) |
