toSeminorm_ball_zero

Mathlib.Analysis.LocallyConvex.WeakDual

URI: https://scilib.ai/kg/mathlib#LinearMap.toSeminorm_ball_zero

← MathLib Explorer

English

polar ∅ = StrongDual 𝕜 M; actually polar of empty is the whole dual space.

Русский

Поляр ∅ равен всему двойственному пространству.

LaTeX

$$$\operatorname{polar}_{\mathbb{K}}(\emptyset) = \mathrm{StrongDual}_{\mathbb{K}}(M)$$$

Lean4

theorem toSeminorm_ball_zero {f : E →ₗ[𝕜] 𝕜} {r : ℝ} : Seminorm.ball f.toSeminorm 0 r = {x : E | ‖f x‖ < r} := by
  simp only [Seminorm.ball_zero_eq, toSeminorm_apply]

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

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

Разделы

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

Аффилиация

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