define a recursive function inside a proof

Stream: general

[Miguel Marco]

I am trying to prove that in a first countable space, for every cluster point x of a sequence, there is a subsequence for which x is a limit.

I have managed to construct a decreasing sequence of neighborhoods that form a a basis, so i can use it to construct the subsequence using the axiom of choice... but my problem is how to make sure that the indices in the subsequence are increasing.

So I basically have the following:

X: Type
s: ℕ → X
x: X
f: ℕ → set X
hf: ∀ (n : ℕ), f n ⊆ ⋂₀ {_x : set X | ∃ (j : ℕ) (H : j < n), f j = _x}
haux: ∀ (n : ℕ), ∃ (n0 : ℕ), n < n0 ∧ s n0 ∈ f n

and I need to construct a sequence k : ℕ → ℕ as follows:

• k 0 should be the n0 that is ensured to exists by haux with n = 0
• k (succ n1) should be the n0 that exists because of haux with n = k n1

I am trying to define such a sequence, but apparently Lean doesn't like to define recursive functions inside a tactic proof.

What is the right way to do this?

[Yaël Dillies]

Why do you care about it being increasing in the first place?

[Miguel Marco]

It is part of the definition of subsequence.

[Kyle Miller]

The choose tactic might be useful, since it can take haux and give you a function Nat -> Nat, but you might need to transform it more.

[Miguel Marco]

Yes, that was my idea, but as you said, it doesn't work right away. Somehow I need the previous values of the chosing function to define the next one.

[Kevin Buzzard]

You could just use the recursor Nat.rec directly in the proof, or make an auxiliary definition outside the proof which takes f and haux as inputs and spits out the function.

[Patrick Massot]

@Miguel Marco this is almost surely in Mathlib already. Are you doing that as an exercise or would you be happy to get it from Mathlib?

[Miguel Marco]

I am happy to get it from mathlib, but didn't find it.

I mean, I am happy to get the subsequence from mathlib. The fact that cluster points are limit points of a subsquence is the exercise I want to do.

[Patrick Massot]

You probably want to play with docs#Filter.extraction_forall_of_frequently and surrounding lemmas then.

[Patrick Massot]

Maybe docs@Filter.extraction_forall_of_eventually'

[Patrick Massot]

There are tons of variations in that file.

[Miguel Marco]

I see... It looks like the exact variation I need is missing: docs#Filter.extraction_forall_of_eventually' requires a stronger hypothesis, and docs#Filter.extraction_forall_of_frequently , which would be the one I need (I think), has the hypothesis written in terms of filters instead of sequences.

I guess I will need to do some work translating from filter language to sequences.

[Patrick Massot]

There should be a lemma doing the translation already. Something like Filter.frequently_atTop (only guessing the name).

[Miguel Marco]

It did work, thank you!

Do you think it would be worth adding the version with sequences to mathlib?