English
Let 𝕜 be a field with a seminormed space E and an absorbent set s ⊆ E. If for every x ∈ s the family {p_i(x)} is bounded above, then the whole range {p_i} is bounded above.
Русский
Пусть 𝕜 — поле, E — модуль над 𝕜, и s ⊆ E абсорбируемо. Если для каждого x ∈ s множество значений {p_i(x)} по всем i ограничено сверху, то множество значений всей семьи p_i (для всех i) ограничено сверху.
LaTeX
$$$\forall p : \iota \to \mathrm{Seminorm}_{\mathbb{k}}(E),\ s \subseteq E,\ hs : \mathrm{Absorbent}\ 𝕜\ s \;\to\; (\forall x \in s,\ \mathrm{BddAbove}(\{ p(i)(x) : i \in \iota \})) \Rightarrow \mathrm{BddAbove}(\{ p(i) : i \in \iota \}).$$$
Lean4
/-- Let `p i` be a family of seminorms on `E`. Let `s` be an absorbent set in `𝕜`.
If all seminorms are uniformly bounded at every point of `s`,
then they are bounded in the space of seminorms. -/
theorem bddAbove_of_absorbent {ι : Sort*} {p : ι → Seminorm 𝕜 E} {s : Set E} (hs : Absorbent 𝕜 s)
(h : ∀ x ∈ s, BddAbove (range (p · x))) : BddAbove (range p) :=
by
rw [Seminorm.bddAbove_range_iff]
intro x
obtain ⟨c, hc₀, hc⟩ : ∃ c ≠ 0, (c : 𝕜) • x ∈ s := (eventually_mem_nhdsWithin.and (hs.eventually_nhdsNE_zero x)).exists
rcases h _ hc with ⟨M, hM⟩
refine ⟨M / ‖c‖, forall_mem_range.mpr fun i ↦ (le_div_iff₀' (norm_pos_iff.2 hc₀)).2 ?_⟩
exact hM ⟨i, map_smul_eq_mul ..⟩
