Assembling null sequences from countably many finite sets

In a seminormed group, countably many finite sets whose norms are bounded by a sequence tending to 0, together with one further finite set, can all be listed in the range of a single sequence tending to 0. This is how null sequences are built from finite nets at shrinking scales, as in Grothendieck's compactness lemma.

theorem TauCeti.exists_tendsto_zero_union_iUnion_subset_range {E : Type u_1} [SeminormedAddGroup E] {A : Set E} {B : ℕ → Set E} {r : ℕ → ℝ} (hA : A.Finite) (hB : ∀ (k : ℕ), (B k).Finite) (hBr : ∀ (k : ℕ), ∀ z ∈ B k, ‖z‖ ≤ r k) (hr : Filter.Tendsto r Filter.atTop (nhds 0)) : ∃ (x : ℕ → E), Filter.Tendsto x Filter.atTop (nhds 0) ∧ A ∪ ⋃ (k : ℕ), B k ⊆ Set.range x

Countably many finite sets, the k-th inside the closed ball of radius r k → 0 about the origin, together with one further finite set, lie in the range of a single sequence tending to 0.