Users' Mathboxes 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 40043
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 40042 . 2 class prefix
2 vs . . 3 setvar 𝑠
3 vl . . 3 setvar 𝑙
4 cvv 3172 . . 3 class V
5 cn0 11139 . . 3 class 0
62cv 1473 . . . 4 class 𝑠
7 cc0 9792 . . . . 5 class 0
83cv 1473 . . . . 5 class 𝑙
97, 8cop 4130 . . . 4 class ⟨0, 𝑙
10 csubstr 13096 . . . 4 class substr
116, 9, 10co 6527 . . 3 class (𝑠 substr ⟨0, 𝑙⟩)
122, 3, 4, 5, 11cmpt2 6529 . 2 class (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr ⟨0, 𝑙⟩))
131, 12wceq 1474 1 wff prefix = (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr ⟨0, 𝑙⟩))
Colors of variables: wff setvar class
This definition is referenced by:  pfxval  40044  pfx00  40045  pfx0  40046  pfxcl  40047
  Copyright terms: Public domain W3C validator