English
Let p be a family of seminorms on a topological space E which induces its topology. A subset U ⊆ E is open if and only if for every x ∈ U there exists a finite set S ⊆ I and a radius r > 0 such that the seminorm-ball given by the supremum over S, centered at x with radius r, lies inside U. Equivalently, every point of U has a seminorm-ball contained in U.
Русский
Пусть p — семейство семинорм на топологическом пространстве E, порождающее его топологию. Подмножество U ⊆ E открыто тогда и только тогда, когда для каждого x ∈ U существует конечное множество S ⊆ I и радиус r > 0 such that (s.sup p).ball x r ⊆ U, где s = S. Эквивалентно: вокруг каждой точки U существует шар по некоторой конечной смеси семинорм.
LaTeX
$$$hp \;:\\; WithSeminorms\\ p\\ \\Rightarrow\\ \\ IsOpen(U) \\iff \\forall x\\in U, \\exists S\\subseteq \\iota\\text{ finite}, \\exists r>0,\\ (S\\sup p).ball\\; x\\; r \\subseteq U,$$$
Lean4
/-- The open sets of a space whose topology is induced by a family of seminorms
are exactly the sets which contain seminorm balls around all of their points. -/
theorem isOpen_iff_mem_balls (hp : WithSeminorms p) (U : Set E) :
IsOpen U ↔ ∀ x ∈ U, ∃ s : Finset ι, ∃ r > 0, (s.sup p).ball x r ⊆ U := by
simp_rw [← WithSeminorms.mem_nhds_iff hp _ U, isOpen_iff_mem_nhds]
/- Note that through the following lemmas, one also immediately has that separating families
of seminorms induce T₂ and T₃ topologies by `IsTopologicalAddGroup.t2Space`
and `IsTopologicalAddGroup.t3Space` -/
