symbols_mul — Mathlib

English

The symbol set of a product is the union of symbol sets: symbols(a b) = symbols(a) ∪ symbols(b).

Русский

Множество символов произведения равно объединению множеств символов: symbols(a b) = symbols(a) ∪ symbols(b).

LaTeX

$$$\\mathrm{symbols}(a \\cdot b) = \\mathrm{symbols}(a) \\cup \\mathrm{symbols}(b).$$$

Lean4

@[to_additive (attr := simp)]
theorem symbols_mul {a b : FreeMonoid α} : symbols (a * b) = symbols a ∪ symbols b :=
  List.toFinset_append

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