balancedCore_empty

Mathlib.Analysis.LocallyConvex.BalancedCoreHull

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

English

The balanced core of the empty set is empty.

Русский

Балансированное ядро пустого множества равно пустому множеству.

LaTeX

$$$balancedCore 𝕜 (\\emptyset) = \\emptyset$$$

Lean4

theorem balancedCore_empty : balancedCore 𝕜 (∅ : Set E) = ∅ :=
  eq_empty_of_subset_empty (balancedCore_subset _)

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

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

Разделы

Аффилиация

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