Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lpad Structured version   Visualization version   GIF version

 Description: Define the leftpad function. (Contributed by Thierry Arnoux, 7-Aug-2023.)
Assertion
Ref Expression
df-lpad leftpad = (𝑐 ∈ V, 𝑤 ∈ V ↦ (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)))
Distinct variable group:   𝑐,𝑙,𝑤

Detailed syntax breakdown of Definition df-lpad
StepHypRef Expression
2 vc . . 3 setvar 𝑐
3 vw . . 3 setvar 𝑤
4 cvv 3441 . . 3 class V
5 vl . . . 4 setvar 𝑙
6 cn0 11887 . . . 4 class 0
7 cc0 10528 . . . . . . 7 class 0
85cv 1537 . . . . . . . 8 class 𝑙
93cv 1537 . . . . . . . . 9 class 𝑤
10 chash 13688 . . . . . . . . 9 class
119, 10cfv 6324 . . . . . . . 8 class (♯‘𝑤)
12 cmin 10861 . . . . . . . 8 class
138, 11, 12co 7135 . . . . . . 7 class (𝑙 − (♯‘𝑤))
14 cfzo 13030 . . . . . . 7 class ..^
157, 13, 14co 7135 . . . . . 6 class (0..^(𝑙 − (♯‘𝑤)))
162cv 1537 . . . . . . 7 class 𝑐
1716csn 4525 . . . . . 6 class {𝑐}
1815, 17cxp 5517 . . . . 5 class ((0..^(𝑙 − (♯‘𝑤))) × {𝑐})
19 cconcat 13915 . . . . 5 class ++
2018, 9, 19co 7135 . . . 4 class (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)
215, 6, 20cmpt 5110 . . 3 class (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤))
222, 3, 4, 4, 21cmpo 7137 . 2 class (𝑐 ∈ V, 𝑤 ∈ V ↦ (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)))
231, 22wceq 1538 1 wff leftpad = (𝑐 ∈ V, 𝑤 ∈ V ↦ (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)))
 Colors of variables: wff setvar class This definition is referenced by:  lpadval  32069
 Copyright terms: Public domain W3C validator