add — Mathlib

English

If s and t are balanced, then their sum s+t is balanced.

Русский

Если множества s и t сбалансированы, то их сумма s+t сбалансирована.

LaTeX

$$$\text{Balanced}_{\mathfrak{k}}(s) \wedge \text{Balanced}_{\mathfrak{k}}(t) \Rightarrow \text{Balanced}_{\mathfrak{k}}(s+t)$$$

Lean4

theorem add (hs : Balanced 𝕜 s) (ht : Balanced 𝕜 t) : Balanced 𝕜 (s + t) := fun _a ha =>
  (smul_add _ _ _).subset.trans <| add_subset_add (hs _ ha) <| ht _ ha

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