isVonNBounded_pi_iff — Mathlib

English

A set S of functions from a index set ι to spaces E_i is VN bounded iff every projection, eval i, of S is VN bounded.

Русский

Множество функций S: ∀ i, E_i VN‑ограничено ⇔ ∀ i, eval_i''S VN‑ограничено.

LaTeX

$$IsVonNBounded 𝕜 S ↔ ∀ i, IsVonNBounded 𝕜 (eval i '' S)$$

Lean4

theorem isVonNBounded_pi_iff {𝕜 ι : Type*} {E : ι → Type*} [NormedDivisionRing 𝕜] [∀ i, AddCommGroup (E i)]
    [∀ i, Module 𝕜 (E i)] [∀ i, TopologicalSpace (E i)] {S : Set (∀ i, E i)} :
    IsVonNBounded 𝕜 S ↔ ∀ i, IsVonNBounded 𝕜 (eval i '' S) := by
  simp_rw [isVonNBounded_iff_tendsto_smallSets_nhds, nhds_pi, Filter.pi, smallSets_iInf, smallSets_comap_eq_comap_image,
    tendsto_iInf, tendsto_comap_iff, Function.comp_def, ← image_smul, image_image, eval, Pi.smul_apply, Pi.zero_apply]

Похожие утверждения