balancedCore_eq_iInter — Mathlib

English

If 0 ∈ s, then balancedCore 𝕜 s = ⋂_{r∈𝕜, 1≤‖r‖} r•s.

Русский

Пусть 0 ∈ s. Тогда balancedCore 𝕜 s равно пересечению всех множеств r•s при 1≤‖r‖.

LaTeX

$$If\\ (0 \\in s)\\ then\\ balancedCore\\ 𝕜\\ s = \\bigcap_{r:\\\\ 𝕜,\\ 1\\le\\|r\\|}(r\\cdot s)$$

Lean4

theorem balancedCore_eq_iInter (hs : (0 : E) ∈ s) : balancedCore 𝕜 s = ⋂ (r : 𝕜) (_ : 1 ≤ ‖r‖), r • s :=
  by
  refine balancedCore_subset_balancedCoreAux.antisymm ?_
  refine (balancedCoreAux_balanced ?_).subset_balancedCore_of_subset (balancedCoreAux_subset s)
  exact balancedCore_subset_balancedCoreAux (balancedCore_zero_mem hs)

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