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

fix

parent d57aaad5
......@@ -10,7 +10,7 @@ theory IdempotentMagma : base:?Logic =
include ?Magma/magma_theory ❙
axiom_idempotent : ⊦ prop_idempotent op ❙
idempotentMagma = Mod idempotent_theory ❘ role abbreviation ❙
idempotentMagma = Mod `?IdempotentMagma/idempotent_theory ❘ role abbreviation ❙
namespace http://mathhub.info/MitM/smglom/algebra/bands ❚
......@@ -23,7 +23,7 @@ theory Band : base:?Logic =
include ../algebra?IdempotentMagma/idempotent_theory ❙
include ../algebra?SemiGroup/semigroup_theory ❙
band = Mod band_theory ❘ role abbreviation❙
band = Mod `?Band/band_theory ❘ role abbreviation❙
theory Regular : base:?Logic =
......
......@@ -25,7 +25,7 @@ theory Magma : base:?Logic =
include sets:?SetStructures/setstruct_theory ❙
op : U ⟶ U ⟶ U ❘ # 1 ∘ 2 prec 19 ❙
magma = Mod magma_theory ❘ role abbreviation ❙
magma = Mod `?Magma/magma_theory ❘ role abbreviation ❙
baseset : magma ⟶ type ❘ = [m] (m.universe) ❘ # dom 1 ❙
operation : {G: magma} (G.universe ⟶ G.universe ⟶ G.universe) ❘ # 2 ∘ 3 prec 20 ❘ = [G] [a,b] (G.op) a b ❙
finite: magma ⟶ prop ❙
......@@ -38,7 +38,7 @@ theory SemiGroup : base:?Logic =
include ?Magma/magma_theory ❙
axiom_associative : ⊦ prop_associative op ❙
semigroup = Mod semigroup_theory ❙
semigroup = Mod `?SemiGroup/semigroup_theory ❙
theory Unital : base:?Logic =
......@@ -50,7 +50,7 @@ theory Unital : base:?Logic =
axiom_leftUnital : ⊦ prop_leftUnital op e ❙
axiom_rightUnital : ⊦ prop_rightUnital op e ❙
unital = Mod unital_theory ❙
unital = Mod `?Unital/unital_theory ❙
unitOf : {G: unital} dom G ❘ # %I1 e prec 5 ❘ = [G] (G.unit) ❙
......@@ -68,7 +68,7 @@ theory QuasiGroup : base:?Logic =
rightDivision : U ⟶ U ⟶ U ❘ = [a,b] that U ([x] x ∘ a ≐ b) (forallE (forallE qg2 a) b) ❙
quasigroup = Mod quasigroup_theory ❙
quasigroup = Mod `?QuasiGroup/quasigroup_theory ❙
theory CancellativeMagma : base:?Logic =
......@@ -80,7 +80,7 @@ theory CancellativeMagma : base:?Logic =
axiom_rightCancellative : ⊦ prop_rightCancellative op ❙
cancellativemagma = Mod cancellativemagma_theory ❙
cancellativemagma = Mod `?CancellativeMagma/cancellativemagma_theory ❙
/T MiKo: how to express the definitions? ❙
leftCancellative : magma ⟶ bool ❙
......@@ -98,7 +98,7 @@ theory Loop : base:?Logic =
inverse : U ⟶ U ❘ # 1 ⁻¹ prec 24 ❙
axiom_inverse : ⊦ prop_inverse op (inverse) e ❙
loop = Mod loop_theory ❙
loop = Mod `?Loop/loop_theory ❙
include ?Unital ❙
inverseElement : {U : unital} dom U ⟶ dom U ⟶ prop ❘ = [U][n,m] n ∘ m ≐ unitOf U ❙
......@@ -115,7 +115,7 @@ theory Monoid : base:?Logic =
include ?SemiGroup/semigroup_theory ❙
include ?Unital/unital_theory ❙
monoid = Mod monoid_theory ❙
monoid = Mod `?Monoid/monoid_theory ❙
......@@ -127,7 +127,7 @@ theory Group : base:?Logic =
include ?Monoid/monoid_theory ❙
include ?Loop/loop_theory ❙
group = Mod group_theory ❙
group = Mod `?Group/group_theory ❙
inverseOf : {G: group} dom G ⟶ dom G ❘ # 2 ⁻¹ prec 25 ❘ = [G] [a] (G.inverse) a ❙
......@@ -154,14 +154,14 @@ theory AbelianGroup : base:?Logic =
include ?Group/group_theory ❙
axiom_commutative : ⊦ prop_commutative op ❙
abeliangroup = Mod abeliangroup_theory ❘ role abbreviation ❙
abeliangroup = Mod `?AbelianGroup/abeliangroup_theory ❘ role abbreviation ❙
theory GroupHomomorphism : base:?Logic =
include ?Group❙
theory groupHomomorphism_theory : base:?Logic =
theory groupHomomorphism_theory : base:?Logic =
from : group ❘# A❙
to : group ❘# B❙
morph : dom A ⟶ dom B❙
......
......@@ -16,7 +16,7 @@ theory SemiLattice : base:?Logic =
// axiom_transitive : ⊦ transitive (order)❘ = sketch "trivial" ❙
// axiom_antisymmetric : ⊦ antisymmetric (order) ❘ = sketch "trivial" ❙
semilattice = Mod semilattice_theory ❘ role abbreviation ❙
semilattice = Mod `?SemiLattice/semilattice_theory ❘ role abbreviation ❙
......@@ -78,7 +78,7 @@ theory Lattice : base:?Logic =
prop_absorption2 : bool ❘ = prop_absorption join meet ❙
axiom_absorption : ⊦ prop_absorption1 ∧ prop_absorption2 ❙
lattice = Mod lattice_theory ❙
lattice = Mod `?Lattice/lattice_theory ❙
theory DistributiveLattice : base:?Logic =
......@@ -92,7 +92,7 @@ theory DistributiveLattice : base:?Logic =
times = meet ❙
distributiveLattice = Mod distributiveLattice_theory ❙
distributiveLattice = Mod `?DistributiveLattice/distributiveLattice_theory ❙
theory BoundedLattice : base:?Logic =
......@@ -104,7 +104,7 @@ theory BoundedLattice : base:?Logic =
// axiom_top : ⊦ ∀[a] a ≼ ⊤ ❙ // imported implicitly via SemilatticeIsPOSet ❙
// axiom_bot : ⊦ ∀[a] ⊥ ≼ a ❙
boundedLattice = Mod boundedLattice_theory ❙
boundedLattice = Mod `?BoundedLattice/boundedLattice_theory ❙
......@@ -116,7 +116,7 @@ theory ComplementedLattice : base:?Logic =
prop_complemented : bool ❘ = ∀[a] ∃[c] comp a c ❙
axiom_complemented : ⊦ prop_complemented ❙
complementedLattice = Mod complementedLattice_theory ❙
complementedLattice = Mod `?ComplementedLattice/complementedLattice_theory ❙
theory BooleanAlgebra : base:?Logic =
......@@ -126,5 +126,5 @@ theory BooleanAlgebra : base:?Logic =
include ?ComplementedLattice/complementedLattice_theory ❙
include ?DistributiveLattice/distributiveLattice_theory ❙
booleanalgebra = Mod booleanAlgebra_theory ❙
booleanalgebra = Mod `?BooleanAlgebra/booleanAlgebra_theory ❙
......@@ -58,7 +58,7 @@ theory Module : base:?Logic =
// dimension : NAT ❙
// basis : U^dimension ❙
// is_basis : ⊦ ∀ [v : U] ∃ [s : scaltp^dimension] v ≐ (∑ ⟨' s..i ⋅ basis..i | i:dimension '⟩) ❙
// ❚
theory Vectorspace : base:?Logic =
......
......@@ -24,7 +24,7 @@ theory GroupAction : base:?Logic =
inner_notation : {g : U, x : X} X ❘= [g,x] (Φ g) x ❘# 1 < 2 > ❙
is_action : ⊦ ∀[g: U] ∀[h: U] ∀[x:X] g<h<x>> ≐ (g ∘ h)<x>❙
groupAction = Mod groupAction_theory❙
groupAction = Mod `GroupAction/groupAction_theory❙
outer_notation : {GX : groupAction, g : dom GX, x : GX.X} GX.X ❘= [GX,g,x] ((GX.phi) g) x ❘# 2 < 3 > ❙
include ../algebra?RationalPolynomials ❙
......@@ -42,7 +42,7 @@ theory PermutationGroup : base:?Logic =
include ?GroupAction/groupAction_theory ❙
is_injective_action : ⊦ is_injective Φ ❙
permutationGroup = Mod permutationGroup_theory ❙
permutationGroup = Mod `?PermutationGroup/permutationGroup_theory ❙
fromPerm: (List permutation) ⟶ permutationGroup ❙
generators : permutationGroup ⟶ List permutation ❙
......@@ -55,7 +55,7 @@ theory TransitiveGroupAction : base:?Logic =
include ?GroupAction/groupAction_theory ❙
is_transitive : ⊦ ∀[x:X] ∀[y:X] ∃[g:U] (Φ g) x ≐ y ❙
transitiveGroupAction = Mod transitiveGroupAction_theory ❙
transitiveGroupAction = Mod `?TransitiveGroupAction/transitiveGroupAction_theory ❙
tr_value : transitiveGroupAction ⟶ ℕ ❙
......
......@@ -18,7 +18,7 @@ theory Ringoid : base:?Logic =
axiom_distributive : ⊦ prop_distributive plus times ❙
ringoid = Mod ringoid_theory ❙
ringoid = Mod `?Ringoid/ringoid_theory ❙
/T MiKo: refactor this with Ringoid ❚
......@@ -40,7 +40,7 @@ theory Rig : base:?Logic =
unitset = ⟨ x: U | ⊦ x ≠ O ⟩ ❙
axiom_distributive : ⊦ prop_distributive rplus rtimes ❙
rig = Mod rig_theory ❙
rig = Mod `?Rig/rig_theory ❙
unitsetOf : rig ⟶ type ❘ = [r] r.unitset ❙
axiom_rigUnitsetSubtype : {r : rig} r.unitset <* r.universe ❙
......@@ -73,7 +73,7 @@ theory Ring : base:?Logic =
axiom_leftUnital : ⊦ ∀[x : U] I ⋅ x ≐ x ❙
axiom_rightUnital : ⊦ ∀[x : U] x ⋅ I ≐ x ❙
ring = Mod ring_theory ❙
ring = Mod `?Ring/ring_theory ❙
multiplicative_monoid : ring ⟶ monoid ❘ = [r] ['
......@@ -97,7 +97,7 @@ theory Field : base:?Logic =
axiom_commutative : ⊦ ∀[x : U]∀[y] (x ⋅ y) ≐ (y ⋅ x) ❙
field : kind ❘ = Mod field_theory ❘ role abbreviation ❙
field : kind ❘ = Mod `?Field/field_theory ❘ role abbreviation ❙
// multiplicative_group : field ⟶ abeliangroup ❘ = [r] ['
......
......@@ -2,7 +2,7 @@ namespace http://mathhub.info/MitM/smglom ❚
import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
theory FinSequences : base:?Logic =
include arith:?NaturalArithmetics ❙
......
......@@ -13,7 +13,7 @@ theory MetricSpace : base:?Logic =
include sets:?SetStructures/setstruct_theory ❙
d : U ⟶ U ⟶ ℝ ❙
signature = Mod signature_theory ❙
signature = Mod `?MetricSpace/signature_theory ❙
prop_nonNegative : {G : type, d : G ⟶ G ⟶ ℝ} prop ❘ = [G,d] ∀[x]∀[y] 0 ≤ d x y ❙
prop_identityOfIndiscernibles : {G : type, d : G ⟶ G ⟶ ℝ} prop ❘ = [G,d] ∀[x]∀[y] d x y ≐ 0 ⇒ x ≐ y ❙
......@@ -28,7 +28,7 @@ theory MetricSpace : base:?Logic =
d : U ⟶ U ⟶ ℝ^+ ❙
axiom_isPseudoMetric : ⊦ prop_pseudoMetric U d ❙
pseudoMetricSpace = Mod pseudoMetricSpace_theory ❙
pseudoMetricSpace = Mod `?MetricSpace/pseudoMetricSpace_theory ❙
prop_triangleInequality : {G : type, d : G ⟶ G ⟶ ℝ} prop ❘
= [G][d] ∀[x]∀[y]∀[z] (d x z) ≤ ((d y x) + (d y z)) ❙
......@@ -37,7 +37,7 @@ theory MetricSpace : base:?Logic =
include ?MetricSpace/pseudoMetricSpace_theory ❙
axiom_triangleInequality : ⊦ prop_triangleInequality U d ❙
metricSpace = Mod metricSpace_theory ❙
metricSpace = Mod `?MetricSpace/metricSpace_theory ❙
// metricSpace : type ⟶ type ❘ # metricSpace 1 ❙ // = [A] ⟨metricspace | ([G] ⊦ A ≐≐ G.universe)⟩❘
distanceFunction : type ⟶ type ❘ = ⟨A ⟶ A ⟶ ℝ | ([x] ⊦ ∃[G: metricSpace] x ≐ G.d)⟩ ❘ # distanceFunction 1 ❙
......@@ -52,7 +52,7 @@ theory MetricMonoid : base:?Logic =
include algebra?Monoid/monoid_theory ❙
include ?MetricSpace/metricSpace_theory ❙
metricMonoid = Mod metricMonoid_theory ❙
metricMonoid = Mod `?MetricMonoid/metricMonoid_theory ❙
theory Ball : base:?Logic =
......
......@@ -40,7 +40,7 @@ theory BanachSpace : base:?Logic =
include ?NormedSpace/normedspace_theory ❙
structure ms : calculus:?MetricSpace/metricSpace_theory abbrev ?NormedSpace/NormedSpaceAsMetricSpace ❙
normedmetric = Mod normedmetric_theory ❙
normedmetric = Mod `?BanachSpace/normedmetric_theory ❙
banach : {n : normedSpace} prop ❘ = [n] complete n ❙ // TODO also as models-of ❙
......
......@@ -16,8 +16,8 @@ theory Graphs : base:?Logic =
undirected_edges : ⊦ symmetric edges ❙
dgraph : kind ❘ = Mod dgraph_theory ❘ role abbreviation ❙
ugraph : kind ❘ = Mod ugraph_theory ❘ role abbreviation ❙
dgraph : kind ❘ = Mod `?Graphs/dgraph_theory ❘ role abbreviation ❙
ugraph : kind ❘ = Mod `?Graphs/ugraph_theory ❘ role abbreviation ❙
include ts:?RelationClosure ❙
......
......@@ -22,7 +22,7 @@ theory PrOSet : base:?Logic =
prop_directed : bool ❘ = ∀[a] ∀[b] ∃[c] a ≼ c ∧ b ≼ c ❙
prop_directedSubset : (U ⟶ bool) ⟶ bool ❘ = [F] ∀[a] ∀[b] F a ∧ F b ⇒ ∃[c] F c ∧ a ≼ c ∧ b ≼ c ❙
proset = Mod proset_theory ❘ role abbreviation ❙
proset = Mod `?PrOSet/proset_theory ❘ role abbreviation ❙
theory LeastMost : base:?Logic =
......@@ -61,7 +61,7 @@ theory DirectedSet : base:?Logic =
joinAssociative : ⊦ prop_associative join ❘ = sketch "by associativity of disjunction" ❙
joinCommutative : ⊦ prop_commutative join ❘ = sketch "by commutativity of disjunction" ❙
directedSet = Mod directedSet_theory ❘ role abbreviation ❙
directedSet = Mod `?DirectedSet/directedSet_theory ❘ role abbreviation ❙
theory Fixpoints : base:?Logic =
......@@ -79,7 +79,7 @@ theory POSet : base:?Logic =
lemma_partialOrder : ⊦ partialOrder ord ❘ = and_introduction lemma_preOrder axiom_antisymmetric❙
strict_lemma : ⊦ strictPartialOrder strictord ❘ = sketch "by construction" ❙
poset = Mod poset_theory ❘ role abbreviation ❙
poset = Mod `?POSet/poset_theory ❘ role abbreviation ❙
theory SupremumReal : base:?Logic =
......
namespace http://mathhub.info/MitM/smglom/typedsets ❚
import base http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/smglom/typedsets ❚
import ts http://mathhub.info/MitM/smglom/typedsets ❚
import sig http://gl.mathhub.info/MMT/LFX/Sigma ❚
import ar http://mathhub.info/MitM/smglom/arithmetics ❚
......
......@@ -122,7 +122,7 @@ theory SetStructures : base:?Logic =
theory setstruct_theory : base:?Logic =
universe : type ❘ # U❙
setstruct = Mod setstruct_theory ❘ role abbreviation❙
setstruct = Mod `?SetStructures/setstruct_theory ❘ role abbreviation❙
include ?TypedSets ❙
......
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