complementary sequences

Stream: maths

[Johan Commelin]

Suppose I have a strictly monotonous f : nat → nat. How hard is it to define g : nat → nat that is the strictly monotonous sequence of numbers that don't occur in the sequence f...

[Johan Commelin]

Can we define the Figure Figure sequences? https://en.wikipedia.org/wiki/Hofstadter_sequence#Hofstadter_Figure-Figure_sequences

[Floris van Doorn]

You need additional assumptions on f, right? You cannot define g when f = id.

[Chris Hughes]

I constructively proved at some point that every infinite subset of nat was denumerable.

[Chris Hughes]

It's in mathlib. It was part of the denumerability of Q proof.

[Floris van Doorn]

The Figure Figure sequences is a bit tricky since it is a mutual definition. I would probably define them mutually, together with R_list which is equal to (list.range n).map R

[Patrick Massot]

What's the point of this sequence? I skimmed through the wikipedia page without understand why it could be interesting

[Kevin Buzzard]

Just because it's in the OEIS doesn't mean it's interesting to someone who doesn't care about sequences. The OEIS contains huge collections of uninteresting sequences now, which to be honest is really really good, because whenever someone like me runs into a sequence it's now very likely it will be there. Someone like you is I guess far less likely to be running into sequences of positive integers in your day job.

[Kevin Buzzard]

"This is the lexicographically earliest sequence that together with its first differences contains every positive integer exactly once". If that floats your boat, then that's the point of the sequence.