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 32806
 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 32805 . 2 class
2 vf . . 3 setvar 𝑓
3 cc 10251 . . . 4 class
4 cpm 8124 . . . 4 class pm
53, 3, 4co 6906 . . 3 class (ℂ ↑pm ℂ)
6 vx . . . 4 setvar 𝑥
7 vy . . . . . . . 8 setvar 𝑦
87cv 1657 . . . . . . 7 class 𝑦
9 c1 10254 . . . . . . 7 class 1
10 caddc 10256 . . . . . . 7 class +
118, 9, 10co 6906 . . . . . 6 class (𝑦 + 1)
122cv 1657 . . . . . . 7 class 𝑓
1312cdm 5343 . . . . . 6 class dom 𝑓
1411, 13wcel 2166 . . . . 5 wff (𝑦 + 1) ∈ dom 𝑓
1514, 7, 13crab 3122 . . . 4 class {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓}
166cv 1657 . . . . . . 7 class 𝑥
1716, 9, 10co 6906 . . . . . 6 class (𝑥 + 1)
1817, 12cfv 6124 . . . . 5 class (𝑓‘(𝑥 + 1))
1916, 12cfv 6124 . . . . 5 class (𝑓𝑥)
20 cmin 10586 . . . . 5 class
2118, 19, 20co 6906 . . . 4 class ((𝑓‘(𝑥 + 1)) − (𝑓𝑥))
226, 15, 21cmpt 4953 . . 3 class (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓𝑥)))
232, 5, 22cmpt 4953 . 2 class (𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓𝑥))))
241, 23wceq 1658 1 wff △ = (𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓𝑥))))
 Colors of variables: wff setvar class This definition is referenced by:  fwddifval  32809
 Copyright terms: Public domain W3C validator