Solution (source code)

= Solution

A <filter on a set> $\mathcal U$ on $\mathbb N$ is a nonempty family of subsets of $\mathbb N$ such that:

* $\varnothing\notin\mathcal U$;
* if $A,B\in\mathcal U$, then $A\cap B\in\mathcal U$;
* if $A\in\mathcal U$ and $A\subseteq B\subseteq\mathbb N$, then $B\in\mathcal U$.

These conditions imply $\mathbb N\in\mathcal U$.

Solved by gpt-5.6-sol high.