benjub
commented
3 weeks ago /!\ Spoiler alert below the dots /!\
...
...
...
Forward implication: Given a proposition $f \colon \omega \to 2$, define $g \in \mathbb{N}_\infty$ by $g(n) \coloneqq \min ( f(i) \mid i \leq n)$. Then, $g$ is the point at infinity iff $\forall n \in \omega f(n)=1$.
Backward implication: Decidability of equality with the point at infinity follows from the fact that $\mathbb{N}_\infty \subseteq \Omega$, and decidability of equality in $\mathbb{N}$ has been proved.
This is mentioned as background knowledge at https://mathstodon.xyz/@MartinEscardo/113001536506411322 but I don't see it proved in iset.mm, or an issue for it.
In iset.mm notation this would be