If we represent infinite set of A as their characteristic functions A -> bool, what are the conditions on A so that the problem of testing if a set is empty actually decidable?
A
A -> bool
Let's build a simple proof assistant using built-in ocaml GADTs
Fourrier is nice, but do there exist two periodic functions $f,g : \mathbb{R} \to \mathbb{R}$ such that $\forall x \in \mathbb{R},\ f(x)+g(x)=x$? Well, with the axiom of choice, that is the case! This and more.