The finite set of symbols in a FreeMonoid element

This is separated from the main FreeMonoid file, as it imports the finiteness hierarchy

def FreeMonoid.symbols {α : Type u_1} [DecidableEq α] (a : FreeMonoid α) : Finset α

the set of unique symbols in a free monoid element

Equations

• a.symbols = List.toFinset a

def FreeAddMonoid.symbols {α : Type u_1} [DecidableEq α] (a : FreeAddMonoid α) : Finset α

The set of unique symbols in an additive free monoid element

Equations

• a.symbols = List.toFinset a

@[simp]

theorem FreeMonoid.symbols_one {α : Type u_1} [DecidableEq α] : symbols 1 = ∅

@[simp]

theorem FreeAddMonoid.symbols_zero {α : Type u_1} [DecidableEq α] : symbols 0 = ∅

@[simp]

theorem FreeMonoid.symbols_of {α : Type u_1} [DecidableEq α] {m : α} : (of m).symbols = {m}

@[simp]

theorem FreeAddMonoid.symbols_of {α : Type u_1} [DecidableEq α] {m : α} : (of m).symbols = {m}

@[simp]

theorem FreeMonoid.symbols_mul {α : Type u_1} [DecidableEq α] {a b : FreeMonoid α} : (a * b).symbols = a.symbols ∪ b.symbols

@[simp]

theorem FreeAddMonoid.symbols_add {α : Type u_1} [DecidableEq α] {a b : FreeAddMonoid α} : (a + b).symbols = a.symbols ∪ b.symbols

@[simp]

theorem FreeMonoid.mem_symbols {α : Type u_1} [DecidableEq α] {m : α} {a : FreeMonoid α} : m ∈ a.symbols ↔ m ∈ a

@[simp]

theorem FreeAddMonoid.mem_symbols {α : Type u_1} [DecidableEq α] {m : α} {a : FreeAddMonoid α} : m ∈ a.symbols ↔ m ∈ a