gaugeSeminormFamily_ball — Mathlib

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

Похожие утверждения