Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Convergent subsequence of countable family of ...

Email Gateway (Aug 22 2022 at 15:37):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear HOL-Analysis experts,

Suppose I have a countable family (f_j)_j of bounded sequences of the reals, say

f :: nat => nat => real

with a <= f n x <= b for all n, x. Here, f's first argument is the family index and the
second argument is the sequence index. Then, there should be a subsequence of f that
converges pointwise for every family index, i.e., a k :: nat => nat such that subseq k and
(%n. f j (k n)) converges for every j. (See, e.g., https://math.stackexchange.com/a/709495
for a proof).

Is there already somewhere in the Isabelle library a proof of this fact? Or something that
makes a short proof? Or do I have to formalise the diagonalisation argument myself?

Thanks,
Andreas

Email Gateway (Aug 22 2022 at 15:38):

From: Johannes Hölzl <johannes.hoelzl@gmx.de>
Hi Andreas,

I didn't look at it in details, but does Fabian's diagonal subsequence
in

src/HOL/Library/Diagonal_Subsequence.thy

help you? It looks similar.

- Johannes

Email Gateway (Aug 22 2022 at 15:38):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Fabian and Johannes,

Thanks for the pointer. This works nicely.

Andreas

Last updated: Apr 26 2024 at 16:20 UTC