English
Characterization of l* membership: x ∈ l* iff there exists a finite collection S of nonempty words from l whose concatenation equals x.
Русский
Характеризация принадлежности x l*: существует конечная коллекция S непустых слов из l such that конкатенация слов из S равна x.
LaTeX
$$$ x \in l^* \iff \exists S : List (List \alpha), x = S.flatten \wedge \forall y \in S, y \in l \wedge y \neq [] $$$
Lean4
theorem mem_kstar_iff_exists_nonempty {x : List α} :
x ∈ l∗ ↔ ∃ S : List (List α), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ [] :=
by
constructor
· rintro ⟨S, rfl, h⟩
refine ⟨S.filter fun l ↦ !List.isEmpty l, by simp [List.flatten_filter_not_isEmpty], fun y hy ↦ ?_⟩
simp only [mem_filter, Bool.not_eq_eq_eq_not, Bool.not_true, isEmpty_eq_false_iff, ne_eq] at hy
exact ⟨h y hy.1, hy.2⟩
· rintro ⟨S, hx, h⟩
exact ⟨S, hx, fun y hy ↦ (h y hy).1⟩
