Description: Define the rank function.
See rankval 8287, rankval2 8289, rankval3 8311, or
rankval4 8338 its value. The rank is a kind of
"inverse" of the cumulative
hierarchy of sets function : given a set, it returns an ordinal
number telling us the smallest layer of the hierarchy to which the set
belongs. Based on Definition 9.14 of [TakeutiZaring] p. 79. Theorem
rankid 8304 illustrates the "inverse" concept.
Another nice theorem
showing the relationship is rankr1a 8307. (Contributed by NM,
11-Oct-2003.) |