English
Ball equality for gauge seminorms holds as in the previous gaugeBall statement.
Русский
Справедливость равенства шаров для шкалы-гейнджа сохраняется как и ранее.
LaTeX
$$$(gaugeSeminormFamily 𝕜 E s).ball 0 1 = (s : Set E)$$$
Lean4
/-- The topology of a locally convex space is induced by the gauge seminorm family. -/
theorem with_gaugeSeminormFamily : WithSeminorms (gaugeSeminormFamily 𝕜 E) :=
by
refine SeminormFamily.withSeminorms_of_hasBasis _ ?_
refine (nhds_hasBasis_absConvex_open 𝕜 E).to_hasBasis (fun s hs => ?_) fun s hs => ?_
· refine ⟨s, ⟨?_, rfl.subset⟩⟩
convert (gaugeSeminormFamily _ _).basisSets_singleton_mem ⟨s, hs⟩ one_pos
rw [gaugeSeminormFamily_ball, Subtype.coe_mk]
refine ⟨s, ⟨?_, rfl.subset⟩⟩
rw [SeminormFamily.basisSets_iff] at hs
rcases hs with ⟨t, r, hr, rfl⟩
rw [Seminorm.ball_finset_sup_eq_iInter _ _ _ hr]
-- We have to show that the intersection contains zero, is open, balanced, and convex
refine
⟨mem_iInter₂.mpr fun _ _ => by simp [hr], isOpen_biInter_finset fun S _ => ?_,
balanced_iInter₂ fun _ _ => Seminorm.balanced_ball_zero _ _, convex_iInter₂ fun _ _ => Seminorm.convex_ball ..⟩
-- The only nontrivial part is to show that the ball is open
have hr' : r = ‖(r : 𝕜)‖ * 1 := by simp [abs_of_pos hr]
have hr'' : (r : 𝕜) ≠ 0 := by simp [hr.ne']
rw [hr', ← Seminorm.smul_ball_zero hr'', gaugeSeminormFamily_ball]
exact S.coe_isOpen.smul₀ hr''
