isVonNBounded_neg

Mathlib.Analysis.LocallyConvex.Bounded

URI: https://scilib.ai/kg/mathlib#Bornology.isVonNBounded_neg

English

If s and t are von Neumann bounded, then their difference s − t is von Neumann bounded.

Русский

Если s и t VN‑ограничены, то их разность s − t VN‑ограничена.

LaTeX

$$hs : IsVonNBounded 𝕜 s, ht : IsVonNBounded 𝕜 t ⇒ IsVonNBounded 𝕜 (s - t)$$

Lean4

@[simp]
theorem isVonNBounded_neg : IsVonNBounded 𝕜 (-s) ↔ IsVonNBounded 𝕜 s :=
  ⟨fun h ↦ neg_neg s ▸ h.neg, fun h ↦ h.neg⟩

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

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

Разделы

Аффилиация

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