neg_ball

Mathlib.Analysis.Seminorm

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

← MathLib Explorer

English

-ball p x r = ball p (-x) r

Русский

-ball p x r = ball p (-x) r

LaTeX

$$$-\mathrm{ball}(p,x,r) = \mathrm{ball}(p,-x,r)$$$

Lean4

@[simp]
theorem neg_ball (p : Seminorm 𝕜 E) (r : ℝ) (x : E) : -ball p x r = ball p (-x) r :=
  by
  ext
  rw [Set.mem_neg, mem_ball, mem_ball, ← neg_add', sub_neg_eq_add, map_neg_eq_map]

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

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

Разделы

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

Аффилиация

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