English
If s and t are nonempty, von Neumann boundedness of s+t is equivalent to the conjunction of von Neumann boundedness of s and t.
Русский
Если s и t непустые, то von Neumann ограниченность s+t эквивалентна сочетанию von Neumann ограниченности s и t.
LaTeX
$$$s\neq \varnothing \land t\neq \varnothing \Rightarrow \text{IsVonNBounded}_{𝕜}(s+t) \iff \text{IsVonNBounded}_{𝕜}(s) \land \text{IsVonNBounded}_{𝕜}(t)$$$
Lean4
/-- Given any sequence `ε` of scalars which tends to `𝓝[≠] 0`, we have that a set `S` is bounded
if and only if for any sequence `x : ℕ → S`, `ε • x` tends to 0. This actually works for any
indexing type `ι`, but in the special case `ι = ℕ` we get the important fact that convergent
sequences fully characterize bounded sets. -/
theorem isVonNBounded_iff_smul_tendsto_zero {ε : ι → 𝕜} {l : Filter ι} [l.NeBot] (hε : Tendsto ε l (𝓝[≠] 0))
{S : Set E} : IsVonNBounded 𝕜 S ↔ ∀ x : ι → E, (∀ n, x n ∈ S) → Tendsto (ε • x) l (𝓝 0) :=
⟨fun hS _ hxS => hS.smul_tendsto_zero (Eventually.of_forall hxS) (le_trans hε nhdsWithin_le_nhds),
isVonNBounded_of_smul_tendsto_zero (by exact hε self_mem_nhdsWithin)⟩
