image_isVonNBounded_iff_finset_seminorm_bounded

English

If f: G → E and hp is WithSeminorms p, then IsVonNBounded 𝕜 (f'' s) is equivalent to: for every finite I there exists r>0 s.t. all p_i(f x) < r for x ∈ s and i ∈ I.

Русский

Если f: G → E и hp — WithSeminorms p, то IsVonNBounded 𝕜 (f'' s) эквивалентно: для каждого конечного I существует r>0, такой что для всех x в s и i ∈ I выполняется p_i(f x) < r.

LaTeX

$$$WithSeminorms\\ imageBounded:\\; IsVonNBounded 𝕜 (f'' s) \\iff ∀ I : Finset ι, ∃ r>0, ∀ x∈s, p_i (f x) < r$$$

Lean4

theorem image_isVonNBounded_iff_finset_seminorm_bounded (f : G → E) {s : Set G} (hp : WithSeminorms p) :
    IsVonNBounded 𝕜 (f '' s) ↔ ∀ I : Finset ι, ∃ r > 0, ∀ x ∈ s, I.sup p (f x) < r := by
  simp_rw [hp.isVonNBounded_iff_finset_seminorm_bounded, Set.forall_mem_image]

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