Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-pfx | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-pfx | ⊢ prefix = (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr 〈0, 𝑙〉)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cpfx 14235 | . 2 class prefix | |
2 | vs | . . 3 setvar 𝑠 | |
3 | vl | . . 3 setvar 𝑙 | |
4 | cvv 3408 | . . 3 class V | |
5 | cn0 12090 | . . 3 class ℕ0 | |
6 | 2 | cv 1542 | . . . 4 class 𝑠 |
7 | cc0 10729 | . . . . 5 class 0 | |
8 | 3 | cv 1542 | . . . . 5 class 𝑙 |
9 | 7, 8 | cop 4547 | . . . 4 class 〈0, 𝑙〉 |
10 | csubstr 14205 | . . . 4 class substr | |
11 | 6, 9, 10 | co 7213 | . . 3 class (𝑠 substr 〈0, 𝑙〉) |
12 | 2, 3, 4, 5, 11 | cmpo 7215 | . 2 class (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr 〈0, 𝑙〉)) |
13 | 1, 12 | wceq 1543 | 1 wff prefix = (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr 〈0, 𝑙〉)) |
Colors of variables: wff setvar class |
This definition is referenced by: pfxnndmnd 14237 pfxval 14238 pfx00 14239 pfx0 14240 pfxcl 14242 |
Copyright terms: Public domain | W3C validator |