kstar_def_nonempty — Mathlib

English

The Kleene star l* is the set of all strings that can be formed by concatenating a finite sequence of nonempty words from l.

Русский

Звезда Клине l* состоит из всех строк, которые можно получить конкатенацией конечной последовательности непустых слов из l.

LaTeX

$$$ l^* = \{ x : List \alpha \mid \exists S : List (List \alpha), x = S.flatten \wedge \forall y \in S, y \in l \wedge y \neq [] \}$$$

Lean4

theorem kstar_def_nonempty (l : Language α) : l∗ = {x | ∃ S : List (List α), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []} :=
  by ext x; apply mem_kstar_iff_exists_nonempty

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