English
Bounded-above of a set of seminorms is equivalent to bounded-above of the real-valued range at each vector.
Русский
Сверхограниченность множества семинорм эквивалентна сверхограниченности диапазона значений при каждом векторе.
LaTeX
$$BddAbove(range p) ↔ ∀ x, BddAbove(range (λ i, p_i(x)))$$
Lean4
protected theorem bddAbove_iff {s : Set <| Seminorm 𝕜 E} : BddAbove s ↔ BddAbove ((↑) '' s : Set (E → ℝ)) :=
⟨fun ⟨q, hq⟩ => ⟨q, forall_mem_image.2 fun _ hp => hq hp⟩, fun H =>
⟨sSup s, fun p hp x => by
dsimp
rw [Seminorm.coe_sSup_eq' H, iSup_apply]
rcases H with ⟨q, hq⟩
exact le_ciSup ⟨q x, forall_mem_range.mpr fun i : s => hq (mem_image_of_mem _ i.2) x⟩ ⟨p, hp⟩⟩⟩
