mem_ball_self

Mathlib.Analysis.InnerProductSpace.EuclideanDist

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

English

restating that a center belongs to its own ball for positive radius.

Русский

повтор: центр принадлежит своей собственной шаровой окрестности при положительном радиусе.

LaTeX

$$x ∈ ball x r$$

Lean4

theorem mem_ball_self {x : E} {r : ℝ} (hr : 0 < r) : x ∈ ball x r :=
  Metric.mem_ball_self hr

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

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

Разделы

Аффилиация

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