neg

Mathlib.Analysis.LocallyConvex.Bounded

URI: https://scilib.ai/kg/mathlib#Bornology.IsVonNBounded.neg

← MathLib Explorer

English

The Von Neumann boundedness of a set s is equivalent to that of its negation −s.

Русский

VN‑ограниченность множества равносильна VN‑ограниченности множества −s.

LaTeX

$$IsVonNBounded 𝕜 (−s) ↔ IsVonNBounded 𝕜 s$$

Lean4

protected theorem neg (hs : IsVonNBounded 𝕜 s) : IsVonNBounded 𝕜 (-s) := fun U hU ↦
  by
  rw [← neg_neg U]
  exact (hs <| neg_mem_nhds_zero _ hU).neg_neg

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

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

Разделы

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

Аффилиация

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