mem_ball

Mathlib.Analysis.Seminorm

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

English

The relation y ∈ ball p x r is equivalent to p(y − x) < r, in a form convenient for rewriting rules.

Русский

Отношение y ∈ ball p x r эквивалентно p(y − x) < r в виде, удобном для правил перезаписи.

LaTeX

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

Lean4

@[simp]
theorem mem_ball : y ∈ ball p x r ↔ p (y - x) < r :=
  Iff.rfl

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

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

Разделы

Аффилиация

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