Filtering the letters of a free monoid

FreeMonoid.filter p keeps the letters satisfying p and erases the others. It is the monoid endomorphism that List.filter p induces on FreeMonoid α, and unlike FreeMonoid.map it is erasing: it can send a nonempty word to 1.

Main definitions

• FreeMonoid.filter: the erasing endomorphism keeping the letters that satisfy p.

References

• [Pin]

def FreeMonoid.filter {α : Type u_1} (p : α → Bool) : FreeMonoid α →* FreeMonoid α

The endomorphism of the free monoid keeping the letters that satisfy p.

Equations

• FreeMonoid.filter p = { toFun := fun (w : FreeMonoid α) => FreeMonoid.ofList (List.filter p (FreeMonoid.toList w)), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem FreeMonoid.toList_filter {α : Type u_1} (p : α → Bool) (w : FreeMonoid α) : toList ((filter p) w) = List.filter p (toList w)

@[simp]

theorem FreeMonoid.filter_ofList {α : Type u_1} (p : α → Bool) (w : List α) : (filter p) (ofList w) = ofList (List.filter p w)