Homotopy Type Theory algebraic limit field > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Contents

Idea

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

Definition

Let FF be a Heyting field and a function limit space . , whereFx 1 F x^{-1} is another notation for 1x\frac{1}{x}. FF is a calculus field if the algebraic limit theorems are satisfied, i.e. if the limit preserves the field operations:

z: c:S(lim xc0(x)=0)z:\prod_{c:S} \left(\lim_{x \to c} 0(x) = 0\right)
a: c:S f:FuncWithLim(S,F)(c) g:FuncWithLim(S,F)(c)(lim xcf(x)+g(x)=lim xcf(x)+lim xcg(x))a:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{g:FuncWithLim(S, F)(c)} \left(\lim_{x \to c} f(x) + g(x) = \lim_{x \to c} f(x) + \lim_{x \to c} g(x)\right)
n: c:S f:FuncWithLim(S,F)(c)(lim xcf(x)=lim xcf(x))n:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \left(\lim_{x \to c} -f(x) = -\lim_{x \to c} f(x) \right)
s: c:S f:FuncWithLim(S,F)(c) g:FuncWithLim(S,F)(c)(lim xcf(x)g(x)=lim xcf(x)lim xcg(x))s:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{g:FuncWithLim(S, F)(c)} \left(\lim_{x \to c} f(x) - g(x) = \lim_{x \to c} f(x) - \lim_{x \to c} g(x)\right)
α: c:S f:FuncWithLim(S,F)(c) a:(lim xcaf(x)=a(lim xcf(x)))\alpha:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{a:\mathbb{Z}} \left(\lim_{x \to c} a f(x) = a \left(\lim_{x \to c} f(x)\right) \right)
α: c:S f:FuncWithLim(S,F)(c) a:S(lim xcaf(x)=a(lim xcf(x)))\alpha:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{a:S} \left(\lim_{x \to c} a f(x) = a \left(\lim_{x \to c} f(x)\right) \right)
o: c:S(lim xc1(x)=1)o:\prod_{c:S} \left(\lim_{x \to c} 1(x) = 1\right)
m: c:S f:FuncWithLim(S,F)(c) g:FuncWithLim(S,F)(c)(lim xcf(x)g(x)=lim xcf(x)lim xcg(x))m:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{g:FuncWithLim(S, F)(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: c:S f:FuncWithLim(S,F)(c) n:(lim xcf(x) n=(lim xcf(x)) n)p:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{n:\mathbb{N}} \left(\lim_{x \to c} {f(x)}^n = {\left(\lim_{x \to c} f(x)\right)}^n \right)
r: c:S f:FuncWithLim(S,F)(c)((lim xc f g(x))#0)(lim xcf(x) 1=(lim xcf(x)) 1) r:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \left(\left(\lim_{x \to c} f(x)\right) g(x)\right) \# 0\right) \to \left(\lim_{x \to c} {f(x)}^{-1} = {\left(\lim_{x \to c} f(x)\right)}^{-1}\right)
i: c:S f:FuncWithLim(S,F)(c)((lim xcx)#0)(lim xcf(x)f(x) 1=1)i:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \left(\left(\lim_{x \to c} x\right) \# 0\right) \to \left(\lim_{x \to c} f(x) \cdot {f(x)}^{-1} = 1\right)

See also

Revision on April 16, 2022 at 14:59:31 by Anonymous?. See the history of this page for a list of all contributions to it.