ball_mem_nhds

Mathlib.Analysis.InnerProductSpace.EuclideanDist

URI: https://scilib.ai/kg/mathlib#Euclidean.ball_mem_nhds

English

For every x ∈ E and every r > 0, the open ball B(x,r) is a neighborhood of x.

Русский

Для каждой точки x ∈ E и каждого r > 0 открытый шар B(x,r) является окрестностью x.

LaTeX

$$$ \forall x \in E, \forall r > 0: \ ball(x,r) \in \mathcal{N}(x) $$$

Lean4

theorem ball_mem_nhds {x : E} {r : ℝ} (hr : 0 < r) : ball x r ∈ 𝓝 x :=
  nhds_basis_ball.mem_of_mem hr

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru