Formalization of Eberlein–Šmulian theorem

Stream: mathlib4

[Michal Swietek]

I opened a PR with Eberlein–Šmulian theorem. It's intentionally a draft as it's too big to merge in one go. It will be split into smaller parts and merged incrementally. The first part is already under review #34209. The proof follows the basic-sequence approach of Pełczyński, so as part of the formalization I introduce a basic theory of basic sequences. There are two ingredients, that I missed during the fromalization:

• Definition of countable compactness. The full version of Eberlein–Šmulian states equivalence among compactess, sequentiall compactness and countable compactness, so I wanted to add the missing piece here.
• Some basic facts about inclusion of a normed space in it's double dual link. I needed that the inclusion is a homeomorphism onto it's image. Seems like the whole module is a leftover after some bigger refactor NormedSpace -> Normed.

I'm happy to open PRs for the above but first wanted to ask if I missed sth or is someone working on sth similar? I mean

• adding definition of countable compactness and basic facts like relation to compactness and sequential compactness
• finishing the refactor of NormedSpaces and adding missing basic facts about inclusion in double dual.