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

Definition df-lpad 32367
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
1 clpad 32366 . 2 class leftpad
2 vc . . 3 setvar 𝑐
3 vw . . 3 setvar 𝑤
4 cvv 3408 . . 3 class V
5 vl . . . 4 setvar 𝑙
6 cn0 12090 . . . 4 class 0
7 cc0 10729 . . . . . . 7 class 0
85cv 1542 . . . . . . . 8 class 𝑙
93cv 1542 . . . . . . . . 9 class 𝑤
10 chash 13896 . . . . . . . . 9 class
119, 10cfv 6380 . . . . . . . 8 class (♯‘𝑤)
12 cmin 11062 . . . . . . . 8 class
138, 11, 12co 7213 . . . . . . 7 class (𝑙 − (♯‘𝑤))
14 cfzo 13238 . . . . . . 7 class ..^
157, 13, 14co 7213 . . . . . 6 class (0..^(𝑙 − (♯‘𝑤)))
162cv 1542 . . . . . . 7 class 𝑐
1716csn 4541 . . . . . 6 class {𝑐}
1815, 17cxp 5549 . . . . 5 class ((0..^(𝑙 − (♯‘𝑤))) × {𝑐})
19 cconcat 14125 . . . . 5 class ++
2018, 9, 19co 7213 . . . 4 class (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)
215, 6, 20cmpt 5135 . . 3 class (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤))
222, 3, 4, 4, 21cmpo 7215 . 2 class (𝑐 ∈ V, 𝑤 ∈ V ↦ (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)))
231, 22wceq 1543 1 wff leftpad = (𝑐 ∈ V, 𝑤 ∈ V ↦ (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)))
Colors of variables: wff setvar class
This definition is referenced by:  lpadval  32368
  Copyright terms: Public domain W3C validator