English
The topology of a locally convex space is induced by the gauge seminorm family.
Русский
Топология локально выпуклого пространства индуцирована семинормами шкалы.
LaTeX
$$$\\text{with_gaugeSeminormFamily} \\Rightarrow \\text{WithSeminorms}(gaugeSeminormFamily 𝕜 E)$$$
Lean4
theorem gaugeSeminormFamily_ball (s : AbsConvexOpenSets 𝕜 E) : (gaugeSeminormFamily 𝕜 E s).ball 0 1 = (s : Set E) :=
by
dsimp only [gaugeSeminormFamily]
rw [Seminorm.ball_zero_eq]
simp_rw [gaugeSeminorm_toFun]
exact gauge_lt_one_eq_self_of_isOpen s.coe_convex s.coe_zero_mem s.coe_isOpen