Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-pfx Structured version   Visualization version   GIF version

Definition df-pfx 41884
 Description: Define an operation which extracts prefixes of words, i.e. subwords starting at the beginning of a word. Definition in section 9.1 of [AhoHopUll] p. 318. "pfx" is used as label fragment. (Contributed by AV, 2-May-2020.)
Assertion
Ref Expression
df-pfx prefix = (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr ⟨0, 𝑙⟩))
Distinct variable group:   𝑠,𝑙

Detailed syntax breakdown of Definition df-pfx
StepHypRef Expression
1 cpfx 41883 . 2 class prefix
2 vs . . 3 setvar 𝑠
3 vl . . 3 setvar 𝑙
4 cvv 3332 . . 3 class V
5 cn0 11476 . . 3 class 0
62cv 1623 . . . 4 class 𝑠
7 cc0 10120 . . . . 5 class 0
83cv 1623 . . . . 5 class 𝑙
97, 8cop 4319 . . . 4 class ⟨0, 𝑙
10 csubstr 13473 . . . 4 class substr
116, 9, 10co 6805 . . 3 class (𝑠 substr ⟨0, 𝑙⟩)
122, 3, 4, 5, 11cmpt2 6807 . 2 class (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr ⟨0, 𝑙⟩))
131, 12wceq 1624 1 wff prefix = (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr ⟨0, 𝑙⟩))
 Colors of variables: wff setvar class This definition is referenced by:  pfxval  41885  pfx00  41886  pfx0  41887  pfxcl  41888
 Copyright terms: Public domain W3C validator