# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: infinite sequence

#### Chase Norman (Oct 18 2020 at 07:59):

I have a function of type `X → X`

and I want to create some representation of the infinite sequence starting from one element of X through the repeated application of the function.

I intend to prove that there is a duplicate element in the list since X is a `fintype`

and then create a finite sublist between those two elements.

What constructs, if any, would exist to make this sort of thing easier? I've seen `seq`

, but I'm not sure how to make it apply to my situation. Thanks!

#### Floris van Doorn (Oct 18 2020 at 08:07):

The infinite sequence is defined by docs#stream.iterate (note: `stream α`

is just `ℕ → α`

). I don't know how much lemmas about it are useful for you.

#### Floris van Doorn (Oct 18 2020 at 08:09):

The duplicate element should come from an cardinality argument. You want that a function from `nat`

into a `fintype`

is not injective...

#### Floris van Doorn (Oct 18 2020 at 08:10):

Searching for `not_injective_nat_fintype`

gave docs#not_injective_infinite_fintype.

#### Floris van Doorn (Oct 18 2020 at 08:13):

Then the finite sublist can be created in different ways, depending on what you exactly want to do with that list. If you want to make sure you get a minimal list back (with no more duplicates), docs#nat.find will be useful at some point.

#### Chase Norman (Oct 18 2020 at 08:19):

Thanks so much for your response! Right now I have a statement (in a proof) that for `∀ (x : X), ∃ (y : X), useful_property x y`

, do you have any ideas on how to construct the associated function to create the stream?

#### Floris van Doorn (Oct 18 2020 at 08:23):

It will be something like `λ x, classical.some (my_lemma x)`

(and the property can be proven by `λ x, classical.some_spec (my_lemma x)`

).

(if you are in the middle of a proof you can do this with the tactic tactic#choose, but it is often better to separate things out in separate definitions/lemmas).

#### Kenny Lau (Oct 18 2020 at 09:18):

there's also `nat.iterate`

notated as `f ^[n]`

#### Yury G. Kudryashov (Oct 18 2020 at 12:18):

And there is docs#function.is_periodic_pt

#### Yury G. Kudryashov (Oct 18 2020 at 12:19):

This file doesn't have a theorem `[fintype α] (f : α → α) : periodic_pts f = univ`

yet. Feel free to PR it.

Last updated: May 16 2021 at 05:21 UTC