balancedCore_eq — Mathlib

English

If a subset s of a normed-ring module is balanced, then its balanced core coincides with the set itself.

Русский

Пусть s — подмножество векторного пространства над нормированным полем, и оно сбалансировано. Тогда сбалансированное ядро s равно самому s.

LaTeX

$$$Balanced\\ Core\\ 𝕜\\ s \\;\\Rightarrow\\; balancedCore\\ 𝕜\\ s = s$$$

Lean4

theorem balancedCore_eq (h : Balanced 𝕜 s) : balancedCore 𝕜 s = s :=
  le_antisymm (balancedCore_subset _) (h.subset_balancedCore_of_subset subset_rfl)

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