balancedHull_subset_of_subset — Mathlib

English

If t is balanced and s ⊆ t, then balancedHull 𝕜 s ⊆ t; i.e., the balanced hull of s is contained in any balanced superset of s.

Русский

Если t сбалансировано и s ⊆ t, то сбалансированная оболочка s ⊆ t; то есть сбалансированная оболочка является минимальной по включению среди сбалансированных надмножеств.

LaTeX

$$$t\\text{ сбалансировано} \\; \\land \\; s \\subseteq t \\;\\Rightarrow\\; balancedHull\\ 𝕜\\ s \\subseteq t$$$

Lean4

/-- The balanced hull of `s` is minimal in the sense that it is contained in any balanced superset
`t` of `s`. -/
theorem balancedHull_subset_of_subset (ht : Balanced 𝕜 t) (h : s ⊆ t) : balancedHull 𝕜 s ⊆ t :=
  by
  intro x hx
  obtain ⟨r, hr, y, hy, rfl⟩ := mem_balancedHull_iff.1 hx
  exact ht.smul_mem hr (h hy)

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