Pushforward ultrafilter (source code)

= Pushforward ultrafilter
{title2=$g_*U=\{B\subseteq Y:g^{-1}[B]\in U\}$}

For an <ultrafilter> $U$ on $X$ and a <function> $g:X\to Y$, define $g_*U=\{B\subseteq Y:g^{-1}[B]\in U\}$. This is an <ultrafilter> and inherits countable completeness from a <countably complete ultrafilter>. It is nonprincipal exactly when no single fibre of $g$ belongs to $U$. Restricting $U$ to a member of $U$ before pushing forward preserves these properties.