The approximating sequence of Henkel's open mapping theorem

TauCeti/Topology/Algebra/OpenMapping/Basic.lean proves one step of Henkel's approximation: a point in closure (f '' U) is brought inside closure (f '' V) by subtracting the image of some x ∈ U. Iterating that step down a sequence of sets produces a sequence of approximants whose residuals shrink, and this file builds it.

Nothing here converges anything: the sequence exists in any topological additive group, with no completeness and no first countability. Summing it — which is what finally removes the closure from f '' U — is a separate step, and the two hypotheses enter there separately: completeness sums the resulting null sequence, while countable generation of 𝓝 0 is what produces the sequence of subgroups to sum along. TauCeti.mem_image_of_mem_closure_image takes that sequence as an explicit HasAntitoneBasis hypothesis rather than synthesising it, so it assumes completeness but no first-countability instance.

Main results

• TauCeti.exists_seq_mem_and_sub_sum_mem: the approximating sequence, with its partial sums driving the residual into closure (f '' V (n + 1)) at every stage.

References

• L. Henkel, An Open Mapping Theorem for rings which have a zero sequence of units, arXiv:1407.5647.

theorem TauCeti.exists_seq_mem_and_sub_sum_mem {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [AddGroup N] [TopologicalSpace N] [ContinuousSub N] {F : Type u_3} [FunLike F M N] [AddHomClass F M N] (f : F) (V : ℕ → Set M) (hV : ∀ (n : ℕ), closure (⇑f '' V (n + 1)) ∈ nhds 0) {y : N} (hy : y ∈ closure (⇑f '' V 0)) : ∃ (x : ℕ → M), (∀ (n : ℕ), x n ∈ V n) ∧ ∀ (n : ℕ), y - f (∑ i ∈ Finset.range (n + 1), x i) ∈ closure (⇑f '' V (n + 1))

Henkel's approximating sequence. If each closure (f '' V (n + 1)) is a neighbourhood of zero and y lies in closure (f '' V 0), there are approximants x n ∈ V n whose partial sums drive the residual down the sequence: y - f (x 0 + ⋯ + x n) lies in closure (f '' V (n + 1)).

No completeness or first countability is used: those are what let the sequence be summed, which is what finally removes the closure from f '' U, and neither is needed to obtain the approximants.