matches'_map — Mathlib

English

Mapping twice is the same as mapping once with the composed function: map g (map f P) = map (g ∘ f) P.

Русский

Покрытие дважды отображением эквивалентно отображению через композицию функций: map g (map f P) = map (g ∘ f) P.

LaTeX

$$$$ \\mathrm{map}\\; g (\\mathrm{map}\\; f P) = \\mathrm{map}\\; (g \\circ f) P. $$$$

Lean4

/-- The language of the map is the map of the language. -/
@[simp]
theorem matches'_map (f : α → β) : ∀ P : RegularExpression α, (P.map f).matches' = Language.map f P.matches'
  | 0 => (map_zero _).symm
  | 1 => (map_one _).symm
  | char a => by
    rw [eq_comm]
    exact image_singleton
  | R + S => by simp only [matches'_map, map, matches'_add, map_add]
  | R * S => by simp [matches'_map]
  | star R => by simp [matches'_map]

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