image_isVonNBounded_iff_seminorm_bounded

English

For a function f: G → E, IsVonNBounded 𝕜 (f'' s) is equivalent to: for every i there exists r>0 s.t. p_i(f x) < r for all x ∈ s.

Русский

Для отображения f: G → E IsVonNBounded 𝕜 (f'' s) эквивалентно: для каждого i существует r>0, такой что p_i(f x) < r для всех x∈s.

LaTeX

$$$IsVonNBounded 𝕜 (f'' s) \\iff ∀ i, ∃ r>0, ∀ x∈s, p_i (f x) < r$$$

Lean4

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

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