balancedCore_subset

Mathlib.Analysis.LocallyConvex.BalancedCoreHull

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

English

If s is balanced and s ⊆ t, then s ⊆ balancedCore 𝕜 t (i.e., the balanced core contains s).

Русский

Если s сбалансировано и s ⊆ t, то s ⊆ balancedCore 𝕜 t.

LaTeX

$$$s \\subseteq balancedCore 𝕜 t$ given $Balanced 𝕜 s$ and $s \\subseteq t$$$

Lean4

theorem balancedCore_subset (s : Set E) : balancedCore 𝕜 s ⊆ s :=
  sUnion_subset fun _ ht => ht.2

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

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

Разделы

Аффилиация

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