map — Mathlib

English

Mapping the alphabet of a language by a function f yields a ring homomorphism between language algebras.

Русский

Отображение алфавита языка функцией f образует гомоморфизм колец между алгебрами языков.

LaTeX

$$$ \text{map} : (\alpha \to \beta) \to \text{RingHom}(\text{Language } \alpha, \text{Language } \beta) $$$

Lean4

/-- Maps the alphabet of a language. -/
def map (f : α → β) : Language α →+* Language β
    where
  toFun := image (List.map f)
  map_zero' := image_empty _
  map_one' := image_singleton
  map_add' := image_union _
  map_mul' _ _ := image_image2_distrib <| fun _ _ => map_append

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