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

Definition df-pfx 14027
 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 14026 . 2 class prefix
2 vs . . 3 setvar 𝑠
3 vl . . 3 setvar 𝑙
4 cvv 3441 . . 3 class V
5 cn0 11888 . . 3 class 0
62cv 1537 . . . 4 class 𝑠
7 cc0 10529 . . . . 5 class 0
83cv 1537 . . . . 5 class 𝑙
97, 8cop 4531 . . . 4 class ⟨0, 𝑙
10 csubstr 13996 . . . 4 class substr
116, 9, 10co 7136 . . 3 class (𝑠 substr ⟨0, 𝑙⟩)
122, 3, 4, 5, 11cmpo 7138 . 2 class (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr ⟨0, 𝑙⟩))
131, 12wceq 1538 1 wff prefix = (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr ⟨0, 𝑙⟩))
 Colors of variables: wff setvar class This definition is referenced by:  pfxnndmnd  14028  pfxval  14029  pfx00  14030  pfx0  14031  pfxcl  14033
 Copyright terms: Public domain W3C validator