Homotopy Type Theory algebraic limit field > history (Rev #1)

Idea
Definition
See also

Idea

A general structure where the various concepts in scalar calculus makes sense.

Definition

Let $F$ be a Heyting field and a function limit space. $F$ is a calculus field if the algebraic limit theorems are satisfied, i.e. if the limit preserves the field operations:

z:\prod_{c:S} \left(\lim_{x \to c} 0(x) = 0\right)

a:\prod_{c:S} \prod_{f:FuncWithLim(S, T)(c)} \prod_{g:FuncWithLim(S, T)(c)} \left(\lim_{x \to c} f(x) + g(x) = \lim_{x \to c} f(x) + \lim_{x \to c} g(x)\right)

n:\prod_{c:S} \prod_{f:FuncWithLim(S, T)(c)} \left(\lim_{x \to c} -f(x) = -\lim_{x \to c} f(x) \right)

s:\prod_{c:S} \prod_{f:FuncWithLim(S, T)(c)} \prod_{g:FuncWithLim(S, T)(c)} \left(\lim_{x \to c} f(x) - g(x) = \lim_{x \to c} f(x) - \lim_{x \to c} g(x)\right)

\alpha:\prod_{c:S} \prod_{f:FuncWithLim(S, T)(c)} \prod_{a:\mathbf{Z}} \left(\lim_{x \to c} a f(x) = a \left(\lim_{x \to c} f(x)\right) \right)

o:\prod_{c:S} \left(\lim_{x \to c} 1(x) = 1\right)

m:\prod_{c:S} \prod_{f:FuncWithLim(S, T)(c)} \prod_{g:FuncWithLim(S, T)(c)} \left(\lim_{x \to c} f(x) \cdot g(x) = \lim_{x \to c} f(x) \cdot \lim_{x \to c} g(x)\right)

p:\prod_{c:S} \prod_{f:FuncWithLim(S, T)(c)} \prod_{n:\mathbf{N}} \left(\lim_{x \to c} {f(x)}^n = {\left(\lim_{x \to c} f(x)\right)}^n \right)

r:\prod_{c:S} \prod_{f:FuncWithLim(S, T)(c)} \left(\left(\lim_{x \to c} f(x)\right) \# 0\right) \to \left(\lim_{x \to c} {f(x)}^{-1} = {\left(\lim_{x \to c} f(x)\right)}^{-1}\right)

Homotopy Type Theory algebraic limit field > history (Rev #1)

Contents

Idea

Definition

See also