English
Let f : α → β and L be a list of pairs (a, b) with a ∈ α and b ∈ {true, false}. Then applying the map f to the element of the free group represented by L is the same as representing the image list by applying f to the first component of each pair. In symbols: map f (mk L) = mk (List.map (λ x, (f x.1, x.2)) L).
Русский
Пусть f : α → β и L — список пар (a, b) с a ∈ α и b ∈ {true, false}. Применение отображения f к элементу свободной группы, представленному L, эквивалентно представлению изображения списка, полученному применением f к первой компоненте каждой пары: map f (mk L) = mk (List.map (λ x, (f x.1, x.2)) L).
LaTeX
$$$ \\operatorname{map} f (\\operatorname{mk} L) = \\operatorname{mk} \\bigl(\\operatorname{List.map} (\\lambda x:(\\alpha \\times \\text{Bool}). (f\\,x.1, x.2))\\, L\\bigr)$$$
Lean4
@[to_additive (attr := simp)]
theorem mk : map f (mk L) = mk (L.map fun x => (f x.1, x.2)) :=
rfl
