balanced — Mathlib

English

The balanced hull of any set s is itself a balanced set.

Русский

Сбалансированная оболочка любого множества s является сбалансированным множеством.

LaTeX

$$$Balanced\\ 𝕜\\ (balancedHull\\ 𝕜\\ s)$$$

Lean4

theorem balanced (s : Set E) : Balanced 𝕜 (balancedHull 𝕜 s) :=
  by
  intro a ha
  simp_rw [balancedHull, smul_set_iUnion₂, subset_def, mem_iUnion₂]
  rintro x ⟨r, hr, hx⟩
  rw [← smul_assoc] at hx
  exact ⟨a • r, (norm_mul_le _ _).trans (mul_le_one₀ ha (norm_nonneg r) hr), hx⟩

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