balanced_closedBall_zero

Mathlib.Analysis.Seminorm

URI: https://scilib.ai/kg/mathlib#balanced_closedBall_zero

← MathLib Explorer

English

Closed balls centered at the origin are balanced.

Русский

Замкнутые шары с центром в 0 сбалансированы.

LaTeX

$$$\forall r:\; \text{Balanced } 𝕜 (\mathrm{Metric.closedBall}(0,E,r)).$$$

Lean4

/-- Closed balls at the origin are balanced. -/
theorem balanced_closedBall_zero : Balanced 𝕜 (Metric.closedBall (0 : E) r) :=
  by
  rw [← closedBall_normSeminorm 𝕜]
  exact (normSeminorm _ _).balanced_closedBall_zero r

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

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

Разделы

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

Аффилиация

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