English
A map f preserves Kleene star: applying f to every word in l^* yields the Kleene star of the mapped language: map f (l^*) = (map f l)^*.
Русский
Образ отображения f сохраняет звёздочку Клейна: образ языка l^* равен звёздочке образа языка l: map f (l^*) = (map f l)^* .
LaTeX
$$$\\mathrm{map}\n f\\; l^{\\ast} = (\\mathrm{map}\\ f\\; l)^{\\ast}$$$
Lean4
@[simp]
theorem map_kstar (f : α → β) (l : Language α) : map f l∗ = (map f l)∗ :=
by
rw [kstar_eq_iSup_pow, kstar_eq_iSup_pow]
simp_rw [← map_pow]
exact image_iUnion