mem_pow — Mathlib

English

For a language l and a word x, x belongs to the n-th power l^n if and only if x can be written as the concatenation of n blocks, each block belonging to l. Equivalently, there exists S = (S_1, ..., S_n) with each S_j a word in l, such that x = S_1 ++ ... ++ S_n.

Русский

Для языка l и слова x верно: x ∈ l^n тогда и только тогда, когда x может быть представлено как конкатенация n блоков, каждый блок принадлежит l. Эквивалентно: существует последовательность S = (S_1, ..., S_n), где каждый S_j ∈ l, такая что x = S_1 ⧺ ... ⧺ S_n.

LaTeX

$$$x \\in l^n \\iff \\exists S : \\text{List}(\\text{List}(\\alpha)), x = S.flatten \\, \\land \\, S.length = n \\, \\land \\, \\forall y \\in S, y \\in l$$$

Lean4

theorem mem_pow {l : Language α} {x : List α} {n : ℕ} :
    x ∈ l ^ n ↔ ∃ S : List (List α), x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l := by
  induction n generalizing x with
  | zero => simp
  | succ n ihn =>
    simp only [pow_succ', mem_mul, ihn]
    constructor
    · rintro ⟨a, ha, b, ⟨S, rfl, rfl, hS⟩, rfl⟩
      exact ⟨a :: S, rfl, rfl, forall_mem_cons.2 ⟨ha, hS⟩⟩
    · rintro ⟨_ | ⟨a, S⟩, rfl, hn, hS⟩ <;> cases hn
      rw [forall_mem_cons] at hS
      exact ⟨a, hS.1, _, ⟨S, rfl, rfl, hS.2⟩, rfl⟩

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