sub — Mathlib

English

If s and t are balanced, then the difference 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 sub (hs : Balanced 𝕜 s) (ht : Balanced 𝕜 t) : Balanced 𝕜 (s - t) :=
  by
  simp_rw [sub_eq_add_neg]
  exact hs.add ht.neg

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