Coinduction works on some uncountable set, for example, streams (or infinite list) which are A^{nat}, where A is the type of the elements in the stream. It looks a bit like induction on finite list, but slightly different.
2
Is there a form of mathematical induction that works for uncountable sets? | Spyke
I'm not an expert on the topic, but I did find this paper laying out an induction flavored technique for proving things over an interval in the reals:
https://tomrocksmaths.com/wp-content/uploads/2021/05/real_induction.pdf
Coinduction works on some uncountable set, for example, streams (or infinite list) which are A^{nat}, where A is the type of the elements in the stream. It looks a bit like induction on finite list, but slightly different.