Homotopy Type Theory
algebraic limit field > history (Rev #2, changes)
Showing changes from revision #1 to #2:
Added | Removed | Changed
Contents
Idea
A general structure where the various concepts in scalar calculus makes sense.
Definition
Let F F Heyting field and a function limit space . F F calculus field if the algebraic limit theorems are satisfied, i.e. if the limit preserves the field operations:
z : ∏ c : S ( lim x → c 0 ( x ) = 0 ) z:\prod_{c:S} \left(\lim_{x \to c} 0(x) = 0\right) a : ∏ c : S ∏ f : FuncWithLim ( S , T F ) ( c ) ∏ g : FuncWithLim ( S , T F ) ( c ) ( lim x → c f ( x ) + g ( x ) = lim x → c f ( x ) + lim x → c g ( x ) ) a:\prod_{c:S} \prod_{f:FuncWithLim(S, T)(c)} F)(c)} \prod_{g:FuncWithLim(S, T)(c)} 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 , T F ) ( c ) ( lim x → c − f ( x ) = − lim x → c f ( x ) ) n:\prod_{c:S} \prod_{f:FuncWithLim(S, T)(c)} F)(c)} \left(\lim_{x \to c} -f(x) = -\lim_{x \to c} f(x) \right) s : ∏ c : S ∏ f : FuncWithLim ( S , T F ) ( c ) ∏ g : FuncWithLim ( S , T F ) ( c ) ( lim x → c f ( x ) − g ( x ) = lim x → c f ( x ) − lim x → c g ( x ) ) s:\prod_{c:S} \prod_{f:FuncWithLim(S, T)(c)} F)(c)} \prod_{g:FuncWithLim(S, T)(c)} 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 , T F ) ( c ) ∏ a : Z ℤ ( lim x → c a f ( x ) = a ( lim x → c f ( x ) ) ) \alpha:\prod_{c:S} \prod_{f:FuncWithLim(S, T)(c)} F)(c)} \prod_{a:\mathbf{Z}} \prod_{a:\mathbb{Z}} \left(\lim_{x \to c} a f(x) = a \left(\lim_{x \to c} f(x)\right) \right) o α : ∏ c : S ( lim x → c 1 ( x ) = 1 ) ∏ f : FuncWithLim ( S , F ) ( c ) ∏ a : S ( lim x → c a f ( x ) = a ( lim x → c f ( x ) ) ) o:\prod_{c:S} \alpha:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(c)} \prod_{a:S} \left(\lim_{x \to c} 1(x) a f(x) = 1\right) a \left(\lim_{x \to c} f(x)\right) \right) m o : ∏ c : S ∏ f : FuncWithLim ( S , T ) ( c ) ( lim x → c 1 ( x ) = 1 ) ∏ g : FuncWithLim ( S , T ) ( c ) ( lim x → c f ( x ) ⋅ g ( x ) = lim x → c f ( x ) ⋅ lim x → c g ( x ) ) m:\prod_{c:S} o:\prod_{c:S} \prod_{f:FuncWithLim(S, T)(c)} \prod_{g:FuncWithLim(S, T)(c)} \left(\lim_{x \to c} f(x) 1(x) \cdot g(x) = \lim_{x 1\right) \to c} f(x) \cdot \lim_{x \to c} g(x)\right) p m : ∏ c : S ∏ f : FuncWithLim ( S , T F ) ( c ) ∏ n g : N FuncWithLim ( S , F ) ( c ) ( lim x → c f ( x ) n f ( x ) ⋅ g ( x ) = ( lim x → c f ( x ) ) n lim x → c f ( x ) ⋅ lim x → c g ( x ) ) p:\prod_{c:S} m:\prod_{c:S} \prod_{f:FuncWithLim(S, T)(c)} F)(c)} \prod_{n:\mathbf{N}} \prod_{g:FuncWithLim(S, F)(c)} \left(\lim_{x \to c} {f(x)}^n f(x) \cdot g(x) = {\left(\lim_{x \lim_{x \to c} f(x)\right)}^n f(x) \right) \cdot \lim_{x \to c} g(x)\right) r p : ∏ c : S ∏ f : FuncWithLim ( S , T F ) ( c ) ( ( lim x → c f ( x ) ) # 0 ) ∏ n : ℕ → ( lim x → c f ( x ) n = ( lim x → c f ( x ) ) n ) ( lim x → c f ( x ) − 1 = ( lim x → c f ( x ) ) − 1 ) r:\prod_{c:S} p:\prod_{c:S} \prod_{f:FuncWithLim(S, T)(c)} F)(c)} \left(\left(\lim_{x \prod_{n:\mathbb{N}} \to c} f(x)\right) \# 0\right) \to \left(\lim_{x \to c} {f(x)}^{-1} {f(x)}^n = {\left(\lim_{x \to c} f(x)\right)}^{-1}\right) f(x)\right)}^n \right) r : ∏ c : S ∏ f : FuncWithLim ( S , F ) ( c ) ( ( lim x → c f ( x ) ) # 0 ) → ( lim x → c f ( x ) − 1 = ( lim x → c f ( x ) ) − 1 ) r:\prod_{c:S} \prod_{f:FuncWithLim(S, F)(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) See also
Revision on April 16, 2022 at 13:07:51 by
Anonymous? .
See the history of this page for a list of all contributions to it.