nhds_basis_closedBall

Mathlib.Analysis.InnerProductSpace.EuclideanDist

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

← MathLib Explorer

English

The Euclidean topology around any x is generated by closed balls centered at x.

Русский

Евклидова топология вокруг x задаётся замкнутыми шарами с центром в x.

LaTeX

$$nhds_basis_closedBall$$

Lean4

theorem nhds_basis_closedBall {x : E} : (𝓝 x).HasBasis (fun r : ℝ => 0 < r) (closedBall x) :=
  by
  rw [toEuclidean.toHomeomorph.nhds_eq_comap x]
  exact Metric.nhds_basis_closedBall.comap _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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