∃A∃f((A⊂Real ∧ Aは開集合 ∧ f∈Map(A,Real)) ⇒ ∃B(B⊂Real ∧ Bは開集合 ∧ D(f)∈Map(B,Real)))
これが有限回つながるような(A,f,B)のセットで、微分方程式を調べる
そのつながる回数をnとすれば、n階の微分方程式を調べることができるかも

一般化した微分
D := { (f,g) | f∈Map(Real,Real) ∧ g⊂Prod(Real,Real) ∧ g={ (x,y) | x,y∈Real ∧ ∀φ((φ,x)∈Lim ⇒ ∃ψ(((f,x,φ),ψ)∈slope ∧ (ψ,y)∈Lim)) } }

D(f)は必ずしも関数になるとは限らないが、集合としての実体はある

ある点に収束する点列から指定関数の傾き値の列を求める
slope := { ((f,x,φ),ψ) | f∈Map(Real,Real) ∧ x∈Real ∧ φ,ψ∈Map(Nat,Real) ∧ (φ,x)∈Lim ∧ ψ={ (n,y) | n∈Nat ∧ y∈Real ∧ x≠φ(n) ∧ y=frac(sub(f(φ(n)),f(x)),sub(φ(n),x)) } }

(つづき)
id:={ (x,f) | x∈Univ(a) ∧ f∈MapClass ∧ { (y,y) | y∈x }=f }

このとき
(ob,ar,form,com,id)は圏、小さい圏と呼ぶ

Union({ { (a,(a,b)) | a∈A } | b∈B })は写像にはならない

F(b):={ (a,(a,b)) | a∈A }∈MapClass
F:={ (b,{ (a,(a,b)) | a∈A }) | b∈B }∈Map(B,MapClass)
Union({ Ran(f) | f∈Ran(F) })={ (a,b) | a∈A ∧ b∈B }
Union({ Ran(f) | f∈Ran(F) })=Union({ Ran(F(b)) | b∈B })

x∈On
Univ(x):=Intersect({ S | x∈S
∧ ∀u(u∈S ⇒ Pow(u),Union(u)∈S)
∧ ∀u∀v(u,v∈S ⇒ (u,v),{u,v}∈S)
∧ ∀u∀v(v∈u∈S ⇒ v∈S)
∧ ∀f((f∈MapClass ∧ Dom(f)∈S ∧ Ran(f)⊂S) ⇒ Ran(f)∈S) })

Prod(A,B):=Ran(Union({ { (a,(a,b)) | a∈A } | b∈B }))
∀A∀B(A,B∈Univ(x) ⇒ Prod(A,B)∈Univ(x))

∀A∀B(∀b(b∈B ⇒ { (a,(a,b)) | a∈A }∈MapClass))
∀A∀B({ { (a,(a,b)) | a∈A } | b∈B }⊂MapClass)
∀A∀B(Union({ { (a,(a,b)) | a∈A } | b∈B })∈MapClass)
Prod(A,B):=Ran(Union({ { (a,(a,b)) | a∈A } | b∈B }))
Dom(Union({ { (a,(a,b)) | a∈A } | b∈B }))=A
∀A∀B(A,B∈Univ ⇒ Prod(A,B)∈Univ)

Mat((m,n),R):= { (A|Seg(m)×Seg(n)) | A∈Mat(R) }
R成分の(m,n)行列全体

Seg(m):={ k | k∈Nat ∧ k<m }

E:=Cup({ ((i,i),1) | i∈Nat },{ ((i,j),0) | i,j∈Nat ∧ i≠j })
(Mat(R),+,O,×,E)は行列環

Zを整数全体として
NatをZに変えてもいけそう

x∈R, i,j∈Nat
emb((i,j),x):=Cup({ ((i,j),x) },{ ((i,j),0) | (i,j)∈Nat×Nat＼{(i,j)} })
emb((i,j),x)∈Mat(R):=Map*(Nat×Nat,R)
A∈Mat(R) ⇒ A=Σ{ ((i,j),emb((i,j),A(i,j))) | (i,j)∈Nat×Nat }　・・・①
emb((i,j),x)×emb((j,k),y):=emb((i,k),x×y)　･･･②
j≠k ⇒ emb((i,j),x)×emb((k,l),y):=O　･･･③
①②③で行列の乗法が定義