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

Definition df-pfx 13714
Description: Define an operation which extracts prefixes of words, i.e. subwords (or substrings) starting at the beginning of a word (or string). In other words, (𝑆 prefix 𝐿) is the prefix of the word 𝑆 of length 𝐿. Definition in Section 9.1 of [AhoHopUll] p. 318. See also Wikipedia "Substring" https://en.wikipedia.org/wiki/Substring#Prefix. (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 13713 . 2 class prefix
2 vs . . 3 setvar 𝑠
3 vl . . 3 setvar 𝑙
4 cvv 3385 . . 3 class V
5 cn0 11580 . . 3 class 0
62cv 1652 . . . 4 class 𝑠
7 cc0 10224 . . . . 5 class 0
83cv 1652 . . . . 5 class 𝑙
97, 8cop 4374 . . . 4 class ⟨0, 𝑙
10 csubstr 13664 . . . 4 class substr
116, 9, 10co 6878 . . 3 class (𝑠 substr ⟨0, 𝑙⟩)
122, 3, 4, 5, 11cmpt2 6880 . 2 class (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr ⟨0, 𝑙⟩))
131, 12wceq 1653 1 wff prefix = (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr ⟨0, 𝑙⟩))
Colors of variables: wff setvar class
This definition is referenced by:  pfxnndmnd  13715  pfxval  13716  pfx00  13717  pfx0  13718  pfxcl  13720
  Copyright terms: Public domain W3C validator