balancedHull_add_subset — Mathlib

English

For NormOneClass 𝕜, balancedHull 𝕜 (s + t) ⊆ balancedHull 𝕜 s + balancedHull 𝕜 t.

Русский

Для нормальной единичной нормы 𝕜: balancedHull 𝕜 (s + t) ⊆ balancedHull 𝕜 s + balancedHull 𝕜 t.

LaTeX

$$$[NormOneClass 𝕜]\\ balancedHull\\ 𝕜 (s + t) \\subseteq balancedHull\\ 𝕜\\ s + balancedHull\\ 𝕜\\ t$$$

Lean4

theorem balancedHull_add_subset [NormOneClass 𝕜] {t : Set E} :
    balancedHull 𝕜 (s + t) ⊆ balancedHull 𝕜 s + balancedHull 𝕜 t :=
  balancedHull_subset_of_subset (add (balancedHull.balanced _) (balancedHull.balanced _))
    (add_subset_add (subset_balancedHull _) (subset_balancedHull _))

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