MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-word Structured version   Visualization version   GIF version

Definition df-word 13331
Description: Define the class of words over a set. A word (sometimes also called a string) is a finite sequence of symbols from a set (alphabet) 𝑆. Definition in section 9.1 of [AhoHopUll] p. 318. The domain is forced to be an initial segment of 0 so that two words with the same symbols in the same order be equal. The set Word 𝑆 is sometimes denoted by S*, using the Kleene star, although the Kleene star, or Kleene closure, is sometimes reserved to denote an operation on languages. The set Word 𝑆 is the free monoid over 𝑆, where the monoid law is concatenation and the monoid unit is the empty word (see frmdval 17435). (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 14-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
df-word Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆}
Distinct variable group:   𝑤,𝑙,𝑆

Detailed syntax breakdown of Definition df-word
StepHypRef Expression
1 cS . . 3 class 𝑆
21cword 13323 . 2 class Word 𝑆
3 cc0 9974 . . . . . 6 class 0
4 vl . . . . . . 7 setvar 𝑙
54cv 1522 . . . . . 6 class 𝑙
6 cfzo 12504 . . . . . 6 class ..^
73, 5, 6co 6690 . . . . 5 class (0..^𝑙)
8 vw . . . . . 6 setvar 𝑤
98cv 1522 . . . . 5 class 𝑤
107, 1, 9wf 5922 . . . 4 wff 𝑤:(0..^𝑙)⟶𝑆
11 cn0 11330 . . . 4 class 0
1210, 4, 11wrex 2942 . . 3 wff 𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆
1312, 8cab 2637 . 2 class {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆}
142, 13wceq 1523 1 wff Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆}
Colors of variables: wff setvar class
This definition is referenced by:  iswrd  13339  wrdval  13340  nfwrd  13365  csbwrdg  13366
  Copyright terms: Public domain W3C validator