isVonNBounded_add_self

Mathlib.Analysis.LocallyConvex.Bounded

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

← MathLib Explorer

English

IsVonNBounded(s+s) is equivalent to IsVonNBounded(s).

Русский

IsVonNBounded(s+s) эквивалентно IsVonNBounded(s).

LaTeX

$$$\text{IsVonNBounded}_{𝕜}(s+s) \iff \text{IsVonNBounded}_{𝕜}(s)$$$

Lean4

@[simp]
theorem isVonNBounded_add_self : IsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s := by
  rcases s.eq_empty_or_nonempty with rfl | hs <;> simp [isVonNBounded_add_of_nonempty, *]

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

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

Разделы

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

Аффилиация

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