balancedCore

Mathlib.Analysis.LocallyConvex.BalancedCoreHull

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

English

There exists a nonempty AbsConvexOpenSets 𝕜 E.

Русский

Существует ненулевой AbsConvexOpenSets 𝕜 E.

LaTeX

$$$\\text{Nonempty }(AbsConvexOpenSets 𝕜 E)$$$

Lean4

/-- The largest balanced subset of `s`. -/
def balancedCore (s : Set E) :=
  ⋃₀ {t : Set E | Balanced 𝕜 t ∧ t ⊆ s}

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

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

Разделы

Аффилиация

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