ball_eq_preimage

Mathlib.Analysis.InnerProductSpace.EuclideanDist

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

English

Around any point x in E, the neighborhood filter has a basis consisting of closed balls with radii > 0.

Русский

Окружение в окрестности точки x образуется базисом замкнутых шаров радиуса > 0.

LaTeX

$$(𝓝 x).HasBasis (fun r => 0 < r) (closedBall x)$$

Lean4

theorem ball_eq_preimage (x : E) (r : ℝ) : ball x r = toEuclidean ⁻¹' Metric.ball (toEuclidean x) r :=
  rfl

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

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

Разделы

Аффилиация

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