Real-valued functions of one variable

Uses Real numbers, Functions

The sum, difference, product, and quotient of two functions is another function:
 s:๐•Š, (s โ†’ โ„) + (s โ†’ โ„) : s โ†’ โ„
 s:๐•Š, (s โ†’ โ„) - (s โ†’ โ„) : s โ†’ โ„
 s:๐•Š, (s โ†’ โ„) ร— (s โ†’ โ„) : s โ†’ โ„
 s:๐•Š, (s โ†’ โ„) รท (s โ†’ โ„) : s โ†’ โ„

Addition and multiplication are commutative and associative:
 s_:๐•Š, f:s_ โ†’ โ„, g:s_ โ†’ โ„, f + g = g + f
 s_:๐•Š, f:s_ โ†’ โ„, g:s_ โ†’ โ„, f ร— g = g ร— f
 s_:๐•Š, f:s_ โ†’ โ„, g:s_ โ†’ โ„, h:s_ โ†’ โ„, (f + g) + h = f + (g + h)
 s_:๐•Š, f:s_ โ†’ โ„, g:s_ โ†’ โ„, h:s_ โ†’ โ„, (f ร— g) ร— h = f ร— (g ร— h)

Addition is distributive over multiplication:
 s_:๐•Š, f:s_ โ†’ โ„, g:s_ โ†’ โ„, h:s_ โ†’ โ„, f ร— (g + h) = (f ร— g) + (f ร— h)

Function application is defined as:
 s_:๐•Š, f:s_ โ†’ โ„, g:s_ โ†’ โ„, x:s_, (f + g)[x] โ‡’ f[x] + g[x]
 s_:๐•Š, f:s_ โ†’ โ„, g:s_ โ†’ โ„, x:s_, (f - g)[x] โ‡’ f[x] - g[x]
 s_:๐•Š, f:s_ โ†’ โ„, g:s_ โ†’ โ„, x:s_, (f ร— g)[x] โ‡’ f[x] ร— g[x]
 s_:๐•Š, f:s_ โ†’ โ„, g:s_ โ†’ โ„, x:s_, (f รท g)[x] โ‡’ f[x] รท g[x]

The sum, difference, product, and quotient of a function and a number is a function:
 s:๐•Š, (s โ†’ โ„) + โ„ : s โ†’ โ„
 s:๐•Š, โ„ + (s โ†’ โ„) : s โ†’ โ„
 s:๐•Š, (s โ†’ โ„) - โ„ : s โ†’ โ„
 s:๐•Š, โ„ - (s โ†’ โ„) : s โ†’ โ„
 s:๐•Š, (s โ†’ โ„) ร— โ„ : s โ†’ โ„
 s:๐•Š, โ„ ร— (s โ†’ โ„) : s โ†’ โ„
 s:๐•Š, (s โ†’ โ„) รท โ„ : s โ†’ โ„
 s:๐•Š, โ„ รท (s โ†’ โ„) : s โ†’ โ„

Addition and multiplication are commutative and associative:
 s_:๐•Š, f:s_ โ†’ โ„, p:โ„, f + p = p + f
 s_:๐•Š, f:s_ โ†’ โ„, p:โ„, f ร— p = p ร— f

Addition is distributive over multiplication:
 s_:๐•Š, f:s_ โ†’ โ„, g:s_ โ†’ โ„, p:โ„, p ร— (f + g) = (p ร— f) + (p ร— g)

Function application is defined as:
 s_:๐•Š, f:s_ โ†’ โ„, p:โ„, x:s_, (f + p)[x] โ‡’ f[x] + p
 s_:๐•Š, f:s_ โ†’ โ„, p:โ„, x:s_, (p + f)[x] โ‡’ p + f[x]
 s_:๐•Š, f:s_ โ†’ โ„, p:โ„, x:s_, (f - p)[x] โ‡’ f[x] - p
 s_:๐•Š, f:s_ โ†’ โ„, p:โ„, x:s_, (p - f)[x] โ‡’ p - f[x]
 s_:๐•Š, f:s_ โ†’ โ„, p:โ„, x:s_, (f ร— p)[x] โ‡’ f[x] ร— p
 s_:๐•Š, f:s_ โ†’ โ„, p:โ„, x:s_, (p ร— f)[x] โ‡’ p ร— f[x]
 s_:๐•Š, f:s_ โ†’ โ„, p:โ„, x:s_, (f รท p)[x] โ‡’ f[x] รท p
 s_:๐•Š, f:s_ โ†’ โ„, p:โ„, x:s_, (p รท f)[x] โ‡’ p รท f[x]