English
In a space whose topology is induced by a family of seminorms p, a set U is a neighborhood of x iff U contains some seminorm ball around x, determined by a finite subfamily of the seminorms.
Русский
В пространстве с топологией, индуцированной семейством семиноморфов p, множество U является окрестностью точки x тогда и только тогда, когда оно содержит некую шар seminom(x, r), определяемый по конечному подмножству семиноморфов.
LaTeX
$$$\text{WithSeminorms}\,p \Rightarrow \forall x,U,\; U\in \mathcal{N}(x) \iff \exists s\in Finset(\iota),\; \exists r>0,\; (s.sup p).ball(x,r) \subseteq U$$$
Lean4
/-- The `x`-neighbourhoods of a space whose topology is induced by a family of seminorms
are exactly the sets which contain seminorm balls around `x`. -/
theorem mem_nhds_iff (hp : WithSeminorms p) (x : E) (U : Set E) :
U ∈ 𝓝 x ↔ ∃ s : Finset ι, ∃ r > 0, (s.sup p).ball x r ⊆ U := by rw [hp.hasBasis_ball.mem_iff, Prod.exists]
