mem_closedBall

Mathlib.Analysis.Seminorm

URI: https://scilib.ai/kg/mathlib#Seminorm.mem_closedBall

English

For any p, x, r, and y, y belongs to closedBall p x r exactly when p(y − x) ≤ r.

Русский

Членство y в замкнутом шаре по p вокруг x радиуса r эквивалентно p(y − x) ≤ r.

LaTeX

$$$y \\in \\mathrm{closedBall}_p(x,r) \\iff p(y - x) \\le r$$$

Lean4

@[simp]
theorem mem_closedBall : y ∈ closedBall p x r ↔ p (y - x) ≤ r :=
  Iff.rfl

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

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

Разделы

Аффилиация

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