map_kstar — Mathlib

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

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