Commit dbf0edb5 authored by Dennis Müller's avatar Dennis Müller

update

parent 824ec60b
......@@ -73,7 +73,7 @@ theory QuasiGroup : base:?Logic =
theory CancellativeMagma : base:?Logic =
include ?Magma ❙
/T MiKo: use this to make a view into quasisgroup Theory: they are cancellative
/T MiKo: use this to make a view into quasisgroup Theory: they are cancellative
theory cancellativemagma_theory : base:?Logic =
include ?Magma/magma_theory ❙
axiom_leftCancellative : ⊦ prop_leftCancellative op ❙
......
......@@ -27,7 +27,7 @@ theory Module : base:?Logic =
axiom_unit_scalars : ⊦ prop_unit_scalars scalarmult (scalars.rone) ❙
module = [R : ring] Mod `?Module/module_theory , R ❙
module = [R : ring] Mod `?Module/module_theory R ❙
distributive_right : {R : ring} ⊦ prop_dist2 (R.rtimes) (R.rplus) (R.rplus) ❘ # distributive_right 1 ❙
......@@ -68,7 +68,7 @@ theory Vectorspace : base:?Logic =
include ?Module/module_theory (scalars) ❙
bminus : U ⟶ U ⟶ U ❘ = [a,b] op a (inverse b) ❘ # 1 - 2❙
vectorspace : field ⟶ kind ❘ = [F : field] Mod `?Vectorspace/vectorspace_theory , F ❙
vectorspace : field ⟶ kind ❘ = [F : field] Mod `?Vectorspace/vectorspace_theory F ❙
include ?Module ❙
......@@ -160,6 +160,6 @@ theory LinearMaps : base:?Logic =
.. ❙
linearMap : field ⟶ ℕ+ ⟶ ℕ+ ⟶ type ❘ = [K : field][n1 : ℕ+,n2 : ℕ+] Mod `?LinearMaps/linearMap_theory , K , n1 , n2 ❘ # linearMap 1 2 3❙
linearMap : field ⟶ ℕ+ ⟶ ℕ+ ⟶ type ❘ = [K : field][n1 : ℕ+,n2 : ℕ+] Mod `?LinearMaps/linearMap_theory K n1 n2 ❘ # linearMap 1 2 3❙
// L : linearMap realfield 2 3 ❙
......@@ -6,7 +6,7 @@ import arith http://mathhub.info/MitM/smglom/arithmetics ❚
theory FinSequences : base:?Logic =
include arith:?NaturalArithmetics ❙
below : ℕ ⟶ type ❙
below : ℕ ⟶ type ❘ = [n] ⟨ x : ℕ | ⊦ x < n ⟩
toBelow : {n : ℕ} below (Succ n) ❘# toB 1❙
succBelow : {n : ℕ} below n ⟶ below (Succ n) ❘# succB 2❙
......@@ -38,5 +38,5 @@ theory FinSequences : base:?Logic =
belowShift : {n : ℕ , m : ℕ} below n ⟶ below (n + m)❙
// belowShift_base : {n, b} ⊦ belowShift n 0 b ≐ b❙
// finSeqSum : {n : ℕ , b : below n}
// finSeqSum : {n : ℕ , b : below n}
......@@ -32,7 +32,7 @@ theory Partition : base:?Logic =
axiom_nonEmpty : ⊦ ¬ (∅ ∈ coll) ❙
axiom_pairwisedisjoint : ⊦ pairwiseDisjoint coll ❙
partition = [X : type] Mod `?Partition/partition_theory , X
partition = [X : type] Mod `?Partition/partition_theory (X)
// theory TaggedPartition : base:?Logic =
......
......@@ -38,7 +38,7 @@ theory Measure : base:?Logic =
axiom_emptyiszero : ⊦ μ (elem (A.coll) ∅ ) ≐ 0 ❙
axiom_sigmaadditivity : ⊦ prop_sigmaAdditive (A.coll) measure ❙
measure = [X : type, A : sigmaAlgebra X] Mod `?Measure/measure_theory , X , A ❙
measure = [X : type, A : sigmaAlgebra X] Mod `?Measure/measure_theory X A ❙
measureSpace = {'
universe : type ,
sigma_algebra : sigmaAlgebra universe ,
......
......@@ -21,7 +21,7 @@ theory SetAlgebra : base:?Logic =
lemma_finiteUnion : ⊦ prop_finiteUnion coll ❘ = sketch "by de Morgan" ❙
lemma_empty : ⊦ prop_emptyInColl coll ❘ = sketch "$∅$ is the complement of $X$" ❙
setAlgebra = [X : type] Mod `?SetAlgebra/setAlgebra_theory , X ❙
setAlgebra = [X : type] Mod `?SetAlgebra/setAlgebra_theory X ❙
theory SigmaAlgebra : base:?Logic =
......@@ -45,7 +45,7 @@ theory SigmaAlgebra : base:?Logic =
sigmaAlgebra = [X : type] Mod `?SigmaAlgebra/sigmaAlgebra_theory , X ❙
sigmaAlgebra = [X : type] Mod `?SigmaAlgebra/sigmaAlgebra_theory X ❙
theory Measurable : base:?Logic =
......
......@@ -159,7 +159,7 @@ theory SetCollection : base:?Logic =
coll : collection X ❙
colltype = setastype coll ❙
setColl = [X : type] Mod `?SetCollection/setColl_theory , X
setColl = [X : type] Mod `?SetCollection/setColl_theory (X)
emptySetInType : {T, S : setColl T, emptyincoll : ⊦ ∅ ∈ (S.coll) } S.colltype ❘ # ∅t %I1 %I2 %I3 ❙
fullSetInType : {T, S : setColl T, fullincoll : ⊦ (fullset T) ∈ (S.coll) } S.colltype ❘ # fullt %I1 %I2 %I3 ❙
......
......@@ -17,7 +17,7 @@ theory OpenSetTopology : base:?Logic =
axiom_intersection: ⊦ prop_finiteIntersection coll ❙
topology = [X : type] Mod `?OpenSetTopology/topology_theory , X
topology = [X : type] Mod `?OpenSetTopology/topology_theory (X)
topologicalSpace : kind ❘ = {'
universe : type ,
topology : topology universe
......@@ -136,7 +136,7 @@ theory HausdorffTopology : base:?Logic =
include ?OpenSetTopology/topology_theory (X) ❙
ishausdorff : ⊦ hausdorffProperty X coll ❙
hausdorffTopology : type ⟶ type ❘ = [X : type] Mod `?HausdorffTopology/hausdorff_theory , X
hausdorffTopology : type ⟶ type ❘ = [X : type] Mod `?HausdorffTopology/hausdorff_theory (X)
hausdorffSpace : kind ❘= {'
universe : type ,
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment