English
A simplified lemma: the finitary bound for von Neumann boundedness reduces to finite-index seminorm bounds.
Русский
Упрощённая лемма: ограниченность по конечной подмножество индексов сводится к ограниченности по каждому конкретному i.
LaTeX
$$$WithSeminorms\\ p \\Rightarrow IsVonNBounded 𝕜 s \\iff ∀ i, ∃ r>0, ∀ x∈s, p_i x < r$$$
Lean4
theorem isVonNBounded_iff_seminorm_bounded {s : Set E} (hp : WithSeminorms p) :
IsVonNBounded 𝕜 s ↔ ∀ i : ι, ∃ r > 0, ∀ x ∈ s, p i x < r :=
by
rw [hp.isVonNBounded_iff_finset_seminorm_bounded]
constructor
· intro hI i
convert hI { i }
rw [Finset.sup_singleton]
intro hi I
by_cases hI : I.Nonempty
· choose r hr h using hi
have h' : 0 < I.sup' hI r := by
rcases hI with ⟨i, hi⟩
exact lt_of_lt_of_le (hr i) (Finset.le_sup' r hi)
refine ⟨I.sup' hI r, h', fun x hx => finset_sup_apply_lt h' fun i hi => ?_⟩
refine lt_of_lt_of_le (h i x hx) ?_
simp only [Finset.le_sup'_iff]
exact ⟨i, hi, (Eq.refl _).le⟩
simp only [Finset.not_nonempty_iff_eq_empty.mp hI, Finset.sup_empty, coe_bot, Pi.zero_apply]
exact ⟨1, zero_lt_one, fun _ _ => zero_lt_one⟩
