balanced_univ

Mathlib.Analysis.LocallyConvex.Basic

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

English

The entire space E (or the set E) is balanced.

Русский

Всякое пространство E сбалансировано.

LaTeX

$$Balanced 𝕜 Set.univ$$

Lean4

@[simp]
theorem balanced_univ : Balanced 𝕜 (univ : Set E) := fun _a _ha => subset_univ _

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

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

Разделы

Аффилиация

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