map_map — Mathlib

English

Applying a map to a regex followed by taking an nth power equals taking the nth power after mapping the regex: map g (P^n) = (map g P)^n.

Русский

Применение отображения к регулярному выражению с последующим возведением в степень n равносильно возведению в степень уже после отображения: map g (P^n) = (map g P)^n.

LaTeX

$$$$ \\mathrm{map}\; g (\\mathrm{P})^n = (\\mathrm{map}\\; g \\; \\mathrm{P})^n, \\quad n \\in \\mathbb{N}. $$$$

Lean4

@[simp]
theorem map_map (g : β → γ) (f : α → β) : ∀ P : RegularExpression α, (P.map f).map g = P.map (g ∘ f)
  | 0 => rfl
  | 1 => rfl
  | char _ => rfl
  | R + S => by simp only [map, map_map]
  | R * S => by simp only [map, map_map]
  | star R => by simp only [map, map_map]

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