map_pow — Mathlib

English

The mapping operation commutes with exponentiation of regular expressions: map f (P^n) = (map f P)^n for all n.

Русский

Отображение сохраняет операцию возведения регулярного выражения в степень: map f (P^n) = (map f P)^n.

LaTeX

$$$\\operatorname{map} f (P^n) = (\\operatorname{map} f P)^n$.$$

Lean4

@[simp]
protected theorem map_pow (f : α → β) (P : RegularExpression α) : ∀ n : ℕ, map f (P ^ n) = map f P ^ n
  | 0 => by unfold map; rfl
  | n + 1 => (congr_arg (· * map f P) (RegularExpression.map_pow f P n) :)

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