Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-fwddif Structured version   Visualization version   GIF version

Definition df-fwddif 31238
Description: Define the forward difference operator. This is a discrete analogue of the derivative operator. Definition 2.42 of [GramKnuthPat], p. 47. (Contributed by Scott Fenton, 18-May-2020.)
Assertion
Ref Expression
df-fwddif △ = (𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓𝑥))))
Distinct variable group:   𝑥,𝑓,𝑦

Detailed syntax breakdown of Definition df-fwddif
StepHypRef Expression
1 cfwddif 31237 . 2 class
2 vf . . 3 setvar 𝑓
3 cc 9786 . . . 4 class
4 cpm 7718 . . . 4 class pm
53, 3, 4co 6523 . . 3 class (ℂ ↑pm ℂ)
6 vx . . . 4 setvar 𝑥
7 vy . . . . . . . 8 setvar 𝑦
87cv 1473 . . . . . . 7 class 𝑦
9 c1 9789 . . . . . . 7 class 1
10 caddc 9791 . . . . . . 7 class +
118, 9, 10co 6523 . . . . . 6 class (𝑦 + 1)
122cv 1473 . . . . . . 7 class 𝑓
1312cdm 5024 . . . . . 6 class dom 𝑓
1411, 13wcel 1975 . . . . 5 wff (𝑦 + 1) ∈ dom 𝑓
1514, 7, 13crab 2895 . . . 4 class {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓}
166cv 1473 . . . . . . 7 class 𝑥
1716, 9, 10co 6523 . . . . . 6 class (𝑥 + 1)
1817, 12cfv 5786 . . . . 5 class (𝑓‘(𝑥 + 1))
1916, 12cfv 5786 . . . . 5 class (𝑓𝑥)
20 cmin 10113 . . . . 5 class
2118, 19, 20co 6523 . . . 4 class ((𝑓‘(𝑥 + 1)) − (𝑓𝑥))
226, 15, 21cmpt 4633 . . 3 class (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓𝑥)))
232, 5, 22cmpt 4633 . 2 class (𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓𝑥))))
241, 23wceq 1474 1 wff △ = (𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓𝑥))))
Colors of variables: wff setvar class
This definition is referenced by:  fwddifval  31241
  Copyright terms: Public domain W3C validator