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

update

parent 671d2ec2
......@@ -4,6 +4,7 @@ import base http://mathhub.info/MitM/Foundation ❚
theory IdempotentMagma : base:?Logic =
include ?OperationProps ❙
include base:?InformalProofs ❙
include ?Magma ❙
theory idempotent_theory : base:?Logic =
include ?Magma/magma_theory ❙
......@@ -16,6 +17,7 @@ namespace http://mathhub.info/MitM/smglom/algebra/bands ❚
theory Band : base:?Logic =
include ../algebra?IdempotentMagma❙
include ../algebra?SemiGroup ❙
theory band_theory : base:?Logic =
include ../algebra?IdempotentMagma/idempotent_theory ❙
......@@ -43,7 +45,7 @@ theory LeftNormal : base:?Logic =
z ∘ x ∘ z ∘ y ≐ z ∘ x ∘ y ❙
implicit view Reg2LeftNormal : ?Regular/regular_theory -> ?LeftNormal/leftnormal_theory =
include ?Band/band_theory = ?Band/band_theory
include ?Band/band_theory ❙
axiom_regular = sketch "trivial" ❙
......@@ -57,7 +59,7 @@ theory RightNormal : base:?Logic =
y ∘ z ∘ x ∘ z ≐ y ∘ x ∘ z ❙
implicit view Reg2RightNormal : ?Regular/regular_theory -> ?RightNormal/rightnormal_theory =
include ?Band/band_theory = ?Band/band_theory
include ?Band/band_theory ❙
axiom_regular = sketch "trivial" ❙
......@@ -73,12 +75,12 @@ theory Normal : base:?Logic =
z ∘ x ∘ y ∘ z ≐ z ∘ y ∘ x ∘ z ❙
implicit view LeftNormal2Normal : ?LeftNormal/leftnormal_theory -> ?Normal/normal_theory =
include ?Band/band_theory = ?Band/band_theory
include ?Band/band_theory ❙
axiom_leftnormal = sketch "trivial" ❙
implicit view RightNormal2Normal : ?RightNormal/rightnormal_theory -> ?Normal/normal_theory =
include ?Band/band_theory = ?Band/band_theory
include ?Band/band_theory ❙
axiom_rightnormal = sketch "trivial" ❙
\ No newline at end of file
......@@ -20,6 +20,7 @@ theory OperationProps : base:?Logic =
theory Magma : base:?Logic =
include ?OperationProps ❙
include sets:?SetStructures ❙
theory magma_theory : base:?Logic =
include sets:?SetStructures/setstruct_theory ❙
op : U ⟶ U ⟶ U ❘ # 1 ∘ 2 prec 19 ❙
......
......@@ -54,27 +54,29 @@ theory Lattice : base:?Logic =
include ts:?POSet ❙
implicit view SemilatticeIsPOSet : ts:?POSet/poset_theory -> ?SemiLattice/semilattice_theory =
universe = universe ❙
ord = [a,b] a ≐ a ∘ b ❙
axiom_reflexive = sketch "trivial" ❙
axiom_transitive = sketch "trivial" ❙
axiom_antisymmetric = sketch "trivial" ❙
universe = universe ❙
ord = [a,b] a ≐ a ∘ b ❙
axiom_reflexive = sketch "trivial" ❙
axiom_transitive = sketch "trivial" ❙
axiom_antisymmetric = sketch "trivial" ❙
include ts:?SetStructures ❙
theory lattice_theory : base:?Logic =
include ts:?SetStructures/setstruct_theory ❙
implicit structure meetstruct : ?SemiLattice/semilattice_theory =
include ts:?SetStructures/setstruct_theory ❙
implicit structure meetstruct : ?SemiLattice/semilattice_theory =
universe = `ts:?SetStructures/setstruct_theory?universe ❙
op @ meet ❘ # 1 ⊓ 2 ❙
structure joinstruct : ?SemiLattice/semilattice_theory =
structure joinstruct : ?SemiLattice/semilattice_theory =
universe = `ts:?SetStructures/setstruct_theory?universe ❙
op @ join ❘ # 1 ⊔ 2 ❙
// order = `http://mathhub.info/MitM/smglom/typedsets?PrOSet/proset_theory?order ❙
prop_absorption1 : bool ❘ = prop_absorption meet join ❙
prop_absorption2 : bool ❘ = prop_absorption join meet ❙
axiom_absorption : ⊦ prop_absorption1 ∧ prop_absorption2 ❙
prop_absorption1 : bool ❘ = prop_absorption meet join ❙
prop_absorption2 : bool ❘ = prop_absorption join meet ❙
axiom_absorption : ⊦ prop_absorption1 ∧ prop_absorption2 ❙
lattice = Mod lattice_theory ❙
......@@ -108,7 +110,7 @@ theory BoundedLattice : base:?Logic =
theory ComplementedLattice : base:?Logic =
include ?BoundedLattice❙
theory complementedLattice_theory : base:?Logic =
theory complementedLattice_theory : base:?Logic =
include ?BoundedLattice/boundedLattice_theory ❙
complement : U ⟶ U ⟶ bool ❘ = [a,c] a ⊔ c ≐ ⊤ ∧ a ⊓ c ≐ ⊥ ❘ # comp 1 2❙
prop_complemented : bool ❘ = ∀[a] ∃[c] comp a c ❙
......@@ -119,6 +121,7 @@ theory ComplementedLattice : base:?Logic =
theory BooleanAlgebra : base:?Logic =
include ?ComplementedLattice❙
include ?DistributiveLattice ❙
theory booleanAlgebra_theory : base:?Logic =
include ?ComplementedLattice/complementedLattice_theory ❙
include ?DistributiveLattice/distributiveLattice_theory ❙
......
......@@ -92,7 +92,7 @@ theory Vectorspace : base:?Logic =
theory Productspace : base:?Logic =
include ?Vectorspace ❙
include base:?ProductType ❙
include base:?ProductTypes
product_universe : {F : field} vectorspace F ⟶ vectorspace F ⟶ type ❘ = [F,v1,v2] v1.universe × v2.universe ❘ # 2 x_ 1 3❙
product_op : {F : field, v1: vectorspace F, v2: vectorspace F} (v1 x_ F v2) ⟶ (v1 x_ F v2) ⟶ (v1 x_ F v2) ❘
......
......@@ -36,6 +36,7 @@ theory PermutationGroup : base:?Logic =
include algebra:?Group❙
include sets:?Bijective ❙
include ?Permutations ❙
include ?GroupAction ❙
theory permutationGroup_theory : base:?Logic =
include ?GroupAction/groupAction_theory ❙
......@@ -48,12 +49,12 @@ theory PermutationGroup : base:?Logic =
dihedralGroup : ℤ ⟶ permutationGroup ❙
theory TransitiveGroupAction : base:?Logic =
theory TransitiveGroupAction : base:?Logic =
include ?GroupAction❙
theory transitiveGroupAction_theory : base:?Logic =
include ?GroupAction/groupAction_theory ❙
is_transitive : ⊦ ∀[x:X] ∀[y:X] ∃[g:U] (Φ g) x ≐ y ❙
include ?GroupAction❙
transitiveGroupAction = Mod transitiveGroupAction_theory ❙
......
......@@ -32,7 +32,7 @@ theory RationalPolynomials : base:?Logic =
include ?Polynomials ❙
include base:?Lists ❙
include algebra?RationalField ❙
include base:?ProductType ❙
include base:?ProductTypes
poly_con : {r : ring} string ⟶ List ℚ ⟶ polynomial r ❘ // = [n,s] polynomial_of s ❙
......
......@@ -63,7 +63,8 @@ theory Rig : base:?Logic =
'] ❙ // needs proof that ret type = unitset ❙
theory Ring : base:?Logic =
theory Ring : base:?Logic =
include ?Rig ❙
// TODO needs refactoring once structures work ❙
theory ring_theory : base:?Logic =
include ?Rig/rig_theory ❙
......@@ -74,7 +75,6 @@ theory Ring : base:?Logic =
ring = Mod ring_theory ❙
include ?Rig ❙
multiplicative_monoid : ring ⟶ monoid ❘ = [r] ['
universe := r.universe,
......@@ -87,6 +87,8 @@ theory Ring : base:?Logic =
theory Field : base:?Logic =
include ?Ring ❙
theory field_theory : base:?Logic =
include ?Ring/ring_theory ❙
......@@ -96,8 +98,7 @@ theory Field : base:?Logic =
axiom_commutative : ⊦ ∀[x : U]∀[y] (x ⋅ y) ≐ (y ⋅ x) ❙
field : kind ❘ = Mod field_theory ❘ role abbreviation ❙
include ?Ring ❙
// multiplicative_group : field ⟶ abeliangroup ❘ = [r] ['
universe := r.unitset,
......
......@@ -5,7 +5,7 @@ import base http://mathhub.info/MitM/Foundation ❚
theory NaturalNumbers : base:?Logic =
include base:?NatLiterals ❙
succ : ℕ ⟶ ℕ ❘ # Succ 1 prec 5 ❘ = [n] nat_lit_succ n ❙
succ : ℕ ⟶ ℕ ❘ # Succ 1 prec 5 ❘ = [n] succ_nat_lit n ❙
axiom_succ1 : {x} ⊦ 0 ≠ Succ x ❙
axiom_succ2 : {x:ℕ,y:ℕ} ⊦ Succ x ≐ Succ y ⟶ ⊦ x ≐ y ❙
......
......@@ -7,6 +7,7 @@ import topo http://mathhub.info/MitM/smglom/topology ❚
theory MetricSpace : base:?Logic =
include arithmetics?RealArithmetics ❙
include sets:?SetStructures ❙
theory signature_theory : base:?Logic =
include sets:?SetStructures/setstruct_theory ❙
......
......@@ -97,7 +97,7 @@ theory Series : base:?Logic =
partialSum : {G : metricMonoid} G^ω ⟶ ℕ ⟶ (G.universe) ❘ # parSum 2 3 ❙
axiom_partialSumBase : {G : metricMonoid} ⊦ ∀[S : G^ω] parSum S 0 ≐ (G.unit) ❙
axiom_partialSumStep : {G : metricMonoid} ⊦ ∀[S : G^ω] ∀[n] parSum S (nat_lit_succ n) ≐ (G.op) (parSum S n) (S (nat_lit_succ n)) ❙
axiom_partialSumStep : {G : metricMonoid} ⊦ ∀[S : G^ω] ∀[n] parSum S (succ_nat_lit n) ≐ (G.op) (parSum S n) (S (succ_nat_lit n)) ❙
prop_convergent : {G : metricMonoid} G^ω ⟶ prop ❘ = [G][S] prop_convergent G ([n] parSum S n) ❙
series : {G : metricMonoid, S: G^ω} dom G ❘ = [G,S] lim (partialSum G S) ❘ # SUM 2 ❙
\ No newline at end of file
namespace http://mathhub.info/MitM/smglom/elliptic_curves ❚
import base http://mathhub.info/MitM/Foundation ❚
theory Weierstrass_model : ?Base =
include http://mathhub.info/MitM/smglom/typedsets?Injective ❙
include base:?Vectors ❙
weierstrass_model : type ❙
polynomial_equation : weierstrass_model ⟶ (polynomial rationalField) ❙
......
......@@ -5,7 +5,7 @@ import sig http://gl.mathhub.info/MMT/LFX/Sigma ❚
theory FiniteSets : base:?Logic =
include base:?ProductType ❙
include base:?ProductTypes
include ?AllSets ❙
......
......@@ -5,7 +5,7 @@ import base http://mathhub.info/MitM/Foundation ❚
theory Relations : base:?Logic =
include arith:?NaturalArithmetics ❙
include ?TypedSets ❙
include base:?ProductType ❙
include base:?ProductTypes
relation : type ⟶ type ⟶ type ❘ = [A,B] A ⟶ B ⟶ bool ❘ # relation 1 2 ❙
relOn : type ⟶ type ❘ = [A] A ⟶ A ⟶ bool ❘ # relOn 1 ❙
......
......@@ -167,7 +167,7 @@ theory SetCollection : base:?Logic =
theory TaggedSetCollection : base:?Logic =
include ?SetCollection ❙
include base:?ProductType ❙
include base:?ProductTypes
taggedCollection : type ⟶ type ❘= [G] set (G × set G) ❙
......
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