Implementation of mathematics in set theory: Difference between revisions

Content deleted Content added
Line 422:
as the collection of functions from A to B, we note that this is three types higher than A or B,
so it is reasonable to define <math>|B|^{|A|}</math> as <math>T^{-3}(|B^A|)</math> so that it
is the same type as A or B (<math>T^{-1}</math> replaces <math>T^{-3}</math> if we use a type-level pair). An effect of this is that the exponential operation is partial: for example, <math>2^{|V|}</math> is undefined.
 
Now the usual theorems of cardinal arithmetic with the axiom of choice can be proved, including