Conservativity of set products on totally supported families

ID: conservativity-of-set-products-on-totally-supported-families

If some is not injective, extend two distinct equal-image elements to tuples using common choices at all other coordinates; the product is not injective. If some is not surjective, extend a missing target element to a tuple; the product is not surjective. The axiom of choice supplies these extensions. Thus the set-product functor reflects isomorphisms between families whose coordinates are all nonempty.

New to topics? Read the docs here!