English
IsVonNBounded s is equivalent to: for every finite set I of indices, there exists r>0 such that for all x in s, (I.sup p) x < r.
Русский
IsVonNBounded s эквивалентно: для каждого конечного множества индексов I существует r>0 такое, что для всех x∈s, (I.sup p) x < r.
LaTeX
$$$IsVonNBounded\\ 𝕜\\ s \\iff\\forall I : Finset\\ ι,\\exists r>0,\\forall x\\in s, (I.sup\\ p) x < r$$$
Lean4
theorem isVonNBounded_iff_finset_seminorm_bounded {s : Set E} (hp : WithSeminorms p) :
IsVonNBounded 𝕜 s ↔ ∀ I : Finset ι, ∃ r > 0, ∀ x ∈ s, I.sup p x < r :=
by
rw [hp.hasBasis.isVonNBounded_iff]
constructor
· intro h I
simp only [id] at h
specialize h ((I.sup p).ball 0 1) (p.basisSets_mem I zero_lt_one)
rcases h.exists_pos with ⟨r, hr, h⟩
obtain ⟨a, ha⟩ := NormedField.exists_lt_norm 𝕜 r
specialize h a (le_of_lt ha)
rw [Seminorm.smul_ball_zero (norm_pos_iff.1 <| hr.trans ha), mul_one] at h
refine ⟨‖a‖, lt_trans hr ha, ?_⟩
intro x hx
specialize h hx
exact (Finset.sup I p).mem_ball_zero.mp h
intro h s' hs'
rcases p.basisSets_iff.mp hs' with ⟨I, r, hr, hs'⟩
rw [id, hs']
rcases h I with ⟨r', _, h'⟩
simp_rw [← (I.sup p).mem_ball_zero] at h'
refine Absorbs.mono_right ?_ h'
exact (Finset.sup I p).ball_zero_absorbs_ball_zero hr
