subset_balancedCore_of_subset — Mathlib

English

If s is balanced and s ⊆ t, then s ⊆ balancedCore 𝕜 t.

Русский

Если s сбалансировано и s ⊆ t, то s ⊆ balancedCore 𝕜 t.

LaTeX

$$$s \\subseteq balancedCore 𝕜 t$ при $Balanced 𝕜 s$ и $s \\subseteq t$$$

Lean4

/-- The balanced core of `t` is maximal in the sense that it contains any balanced subset
`s` of `t`. -/
theorem subset_balancedCore_of_subset (hs : Balanced 𝕜 s) (h : s ⊆ t) : s ⊆ balancedCore 𝕜 t :=
  subset_sUnion_of_mem ⟨hs, h⟩

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