mem_symbols

Mathlib.Algebra.FreeMonoid.Symbols

URI: https://scilib.ai/kg/mathlib#FreeMonoid.mem_symbols

English

An element m is in the symbol set of a if and only if m is contained in a.

Русский

Элемент m принадлежит множеству символов a тогда и только тогда, когда m содержится в a.

LaTeX

$$$m \\in \\mathrm{symbols}(a) \\iff m \\in a$$$

Lean4

@[to_additive (attr := simp)]
theorem mem_symbols {m : α} {a : FreeMonoid α} : m ∈ symbols a ↔ m ∈ a :=
  List.mem_toFinset

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru