Ultrafilter with finite-sums members (source code)

= Ultrafilter with finite-sums members

= IP ultrafilter
{c}
{synonym}

An ultrafilter with finite-sums members is an <ultrafilter> on the <positive integers> all of whose members are <IP sets>. Such an <ultrafilter> exists by extending the <IP-star filter> using the <ultrafilter lemma>. If a member were not IP, its complement would be an <IP-star set> and hence another member, contradicting properness. Conversely, every such ultrafilter contains the entire IP-star filter, since it cannot contain the non-IP complement of an IP-star set. This characterization does not assert that the ultrafilter is idempotent.