symbols — Mathlib

English

The set of unique symbols in a FreeMonoid element a is the finite set of its letters, i.e., List.toFinset a.

Русский

Множество уникальных символов элемента FreeMonoid — это конечное множество его букв: List.toFinset a.

LaTeX

$$$\\mathrm{symbols}(a) = \\mathrm{List.toFinset}(a).$$$

Lean4

/-- the set of unique symbols in a free monoid element -/
@[to_additive /-- The set of unique symbols in an additive free monoid element -/
    ]
def symbols (a : FreeMonoid α) : Finset α :=
  List.toFinset a

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