balancedHull_mono — Mathlib

English

If s ⊆ t then balancedHull 𝕜 s ⊆ balancedHull 𝕜 t.

Русский

Если s ⊆ t, то balancedHull 𝕜 s ⊆ balancedHull 𝕜 t.

LaTeX

$$$s \\subseteq t\\Rightarrow balancedHull\\ 𝕜\\ s \\subseteq balancedHull\\ 𝕜\\ t$$$

Lean4

@[mono, gcongr]
theorem balancedHull_mono (hst : s ⊆ t) : balancedHull 𝕜 s ⊆ balancedHull 𝕜 t :=
  by
  intro x hx
  rw [mem_balancedHull_iff] at *
  obtain ⟨r, hr₁, hr₂⟩ := hx
  use r
  exact ⟨hr₁, smul_set_mono hst hr₂⟩

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