matches'_pow — Mathlib

English

For any P and n, the language of P^n equals the n-fold concatenation of the language of P, i.e., (P^n).matches' = (P.matches')^n.

Русский

Для любого регулярного выражения P и натурального n множество строк, удовлетворяющих P^n, равно n-кратному конкатенированию языка P: (P^n).matches' = (P.matches')^n.

LaTeX

$$$$ (P^n).matches' = (P.matches')^n \\quad (n \\in \\mathbb{N}). $$$$

Lean4

@[simp]
theorem matches'_pow (P : RegularExpression α) : ∀ n : ℕ, (P ^ n).matches' = P.matches' ^ n
  | 0 => matches'_epsilon
  | n + 1 =>
    (matches'_mul _ _).trans <|
      Eq.trans (congrFun (congrArg HMul.hMul (matches'_pow P n)) (matches' P)) (pow_succ _ n).symm

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