Commit 5d2b76db by Dennis Müller

### update

parent 6174d946
 ... ... @@ -26,7 +26,7 @@ theory Magma : base:?Logic = ❚ magma = Mod magma_theory ❘ role abbreviation ❙ baseset : magma ⟶ type ❘ = [m] (m.universe) ❘ # dom 1 ❙ operation : {G: magma} (dom G ⟶ dom G ⟶ dom G) ❘ # 2 ∘ 3 prec 20 ❘ = [G] [a,b] (G.op) a b ❙ operation : {G: magma} (G.universe ⟶ G.universe ⟶ G.universe) ❘ # 2 ∘ 3 prec 20 ❘ = [G] [a,b] (G.op) a b ❙ finite: magma ⟶ prop ❙ ❚ ... ... @@ -37,7 +37,7 @@ theory SemiGroup : base:?Logic = include ?Magma/magma_theory ❙ axiom_associative : ⊦ prop_associative op ❙ ❚ semigroup = Mod semigroup_theory ❘ role abbreviation ❙ semigroup = Mod semigroup_theory ❙ ❚ theory Unital : base:?Logic = ... ... @@ -49,7 +49,7 @@ theory Unital : base:?Logic = axiom_leftUnital : ⊦ prop_leftUnital op e ❙ axiom_rightUnital : ⊦ prop_rightUnital op e ❙ ❚ unital = Mod unital_theory ❘ role abbreviation ❙ unital = Mod unital_theory ❙ unitOf : {G: unital} dom G ❘ # %I1 e prec 5 ❘ = [G] (G.unit) ❙ ❚ ... ... @@ -67,7 +67,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 ❘ role abbreviation ❙ quasigroup = Mod quasigroup_theory ❙ ❚ theory CancellativeMagma : base:?Logic = ... ... @@ -79,7 +79,7 @@ theory CancellativeMagma : base:?Logic = axiom_rightCancellative : ⊦ prop_rightCancellative op ❙ ❚ cancellativemagma = Mod cancellativemagma_theory ❘ role abbreviation ❙ cancellativemagma = Mod cancellativemagma_theory ❙ /T MiKo: how to express the definitions? ❙ leftCancellative : magma ⟶ bool ❙ ... ... @@ -97,7 +97,7 @@ theory Loop : base:?Logic = inverse : U ⟶ U ❘ # 1 ⁻¹ prec 24 ❙ axiom_inverse : ⊦ prop_inverse op (inverse) e ❙ ❚ loop = Mod loop_theory ❘ role abbreviation ❙ loop = Mod loop_theory ❙ include ?Unital ❙ inverseElement : {U : unital} dom U ⟶ dom U ⟶ prop ❘ = [U][n,m] n ∘ m ≐ unitOf U ❙ ... ... @@ -114,7 +114,7 @@ theory Monoid : base:?Logic = include ?SemiGroup/semigroup_theory ❙ include ?Unital/unital_theory ❙ ❚ monoid = Mod monoid_theory ❘ role abbreviation ❙ monoid = Mod monoid_theory ❙ ❚ ... ... @@ -126,7 +126,7 @@ theory Group : base:?Logic = include ?Monoid/monoid_theory ❙ include ?Loop/loop_theory ❙ ❚ group = Mod group_theory ❘ role abbreviation ❙ group = Mod group_theory ❙ inverseOf : {G: group} dom G ⟶ dom G ❘ # 2 ⁻¹ prec 25 ❘ = [G] [a] (G.inverse) a ❙ ... ... @@ -134,10 +134,11 @@ theory Group : base:?Logic = include base:?NatLiterals ❙ include base:?IntLiterals ❙ include base:?InformalProofs ❙ include sets:?FiniteCardinality ❙ automorphisms : group ⟶ ℕ ❙ cyclic : group ⟶ prop ❙ order : group ⟶ ℕ ❘ = [g] cardinality (baseset g)❙ order : group ⟶ ℕ ❘ = [g] | fullset (baseset g) |❙ parity : group ⟶ ℤ ❙ solvable : group ⟶ prop ❙ psolvable : group ⟶ ℕ+ ⟶ prop ❙ ... ... @@ -161,9 +162,9 @@ theory GroupHomomorphism : base:?Logic = theory groupHomomorphism_theory : base:?Logic = from : group ❘# A❙ to : group ❘# B❙ map : dom A ⟶ dom B❙ axiom_morphism : ⊦ ∀[x: dom A] ∀[y: dom A] (B.op) (map x) (map y) ≐ map (x ∘ y)❙ morph : dom A ⟶ dom B❙ axiom_morphism : ⊦ ∀[x: dom A] ∀[y: dom A] (B.op) (morph x) (morph y) ≐ morph (x ∘ y)❙ ❚ groupHomomorphism = Mod `?GroupHomomorphism/groupHomomorphism_theory ❘ role abbreviation❙ groupHomomorphism = Mod `?GroupHomomorphism/groupHomomorphism_theory❙ ❚
 ... ... @@ -7,13 +7,13 @@ import sets http://mathhub.info/MitM/smglom/typedsets ❚ theory Module : base:?Logic = include ?Ring ❙ prop_dist1 : {A : type,B : type} (A ⟶ B ⟶ B) ⟶ (B ⟶ B ⟶ B) ⟶ bool ❘ = [A,B,times,plus] ∀[r]∀[x]∀[y] times r (plus x y) ≐ plus (times r x) (times r y) ❘ # prop_dist1 3 4❙ = [A,B,itimes,iplus] ∀[r]∀[x]∀[y] itimes r (iplus x y) ≐ iplus (itimes r x) (itimes r y) ❘ # prop_dist1 3 4❙ prop_dist2 : {A : type,B : type} (A ⟶ B ⟶ B) ⟶ (A ⟶ A ⟶ A) ⟶ (B ⟶ B ⟶ B) ⟶ bool ❘ = [A,B,times,plus1,plus2] ∀[r]∀[s]∀[x] times (plus1 r s) x ≐ plus2 (times r x) (times s x) ❘ # prop_dist2 3 4 5❙ = [A,B,itimes,plus1,plus2] ∀[r]∀[s]∀[x] itimes (plus1 r s) x ≐ plus2 (itimes r x) (itimes s x) ❘ # prop_dist2 3 4 5❙ prop_associative_scalars : {A : type,B : type} (A ⟶ B ⟶ B) ⟶ (A ⟶ A ⟶ A) ⟶ bool ❘ = [A,B,times,stimes] ∀[r]∀[s]∀[x] times r (times s x) ≐ times (stimes r s) x ❘ # prop_associative_scalars 3 4 ❙ = [A,B,itimes,stimes] ∀[r]∀[s]∀[x] itimes r (itimes s x) ≐ itimes (stimes r s) x ❘ # prop_associative_scalars 3 4 ❙ prop_unit_scalars : {A : type, B : type} (A ⟶ B ⟶ B) ⟶ A ⟶ bool ❘ = [A,B,times,u] ∀[x] times u x ≐ x ❘ # prop_unit_scalars 3 4❙ = [A,B,itimes,u] ∀[x] itimes u x ≐ x ❘ # prop_unit_scalars 3 4❙ theory module_theory : base:?Logic > scalars : ring ❘ = scaltp : type ❘ = scalars.universe ❙ ... ... @@ -22,26 +22,26 @@ theory Module : base:?Logic = scalarmult : scaltp ⟶ U ⟶ U ❘ # 1 ⋅ 2 ❙ axiom_dist1 : ⊦ prop_dist1 scalarmult op❙ axiom_dist2 : ⊦ prop_dist2 scalarmult (scalars.plus) op ❙ axiom_associative_scalars : ⊦ prop_associative_scalars scalarmult (scalars.times) ❙ axiom_unit_scalars : ⊦ prop_unit_scalars scalarmult (scalars.one) ❙ axiom_dist2 : ⊦ prop_dist2 scalarmult (scalars.rplus) op ❙ axiom_associative_scalars : ⊦ prop_associative_scalars scalarmult (scalars.rtimes) ❙ axiom_unit_scalars : ⊦ prop_unit_scalars scalarmult (scalars.rone) ❙ ❚ module = [R : ring] Mod `?Module/module_theory , R ❘ role abbreviation ❙ module = [R : ring] Mod `?Module/module_theory , R ❙ distributive_right : {R : ring} ⊦ prop_dist2 (R.times) (R.plus) (R.plus) ❘ # distributive_right 1 ❙ distributive_right : {R : ring} ⊦ prop_dist2 (R.rtimes) (R.rplus) (R.rplus) ❘ # distributive_right 1 ❙ asModule : {F : ring} module F ❘ = [f] [' universe := f.universe, op := f.plus, op := f.rplus, axiom_associative := f.addition/axiom_associative, unit := f.zero, unit := f.rzero, axiom_leftUnital := f.addition/axiom_leftUnital, axiom_rightUnital := f.addition/axiom_rightUnital, inverse := f.minus, inverse := f.rminus, axiom_inverse := f.addition/axiom_inverse, axiom_commutative := f.addition/axiom_commutative, scalarmult := f.times, scalarmult := f.rtimes, axiom_dist1 := f.axiom_distributive, axiom_dist2 := distributive_right f, axiom_associative_scalars := f.multiplication/axiom_associative, ... ... @@ -68,21 +68,21 @@ 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 ❘ role abbreviation ❙ vectorspace : field ⟶ kind ❘ = [F : field] Mod `?Vectorspace/vectorspace_theory , F ❙ include ?Module ❙ asVectorspace : {F : field} vectorspace F ❘ = [f] [' universe := f.universe, op := f.plus, op := f.rplus, axiom_associative := f.addition/axiom_associative, unit := f.zero, unit := f.rzero, axiom_leftUnital := f.addition/axiom_leftUnital, axiom_rightUnital := f.addition/axiom_rightUnital, inverse := f.minus, inverse := f.rminus, axiom_inverse := f.addition/axiom_inverse, axiom_commutative := f.addition/axiom_commutative, scalarmult := f.times, scalarmult := f.rtimes, axiom_dist1 := f.axiom_distributive, axiom_dist2 := distributive_right f, axiom_associative_scalars := f.multiplication/axiom_associative, ... ... @@ -117,11 +117,11 @@ theory Productspace : base:?Logic = product_axiom_dist1 : {F : field, V1 : vectorspace F, V2 : vectorspace F} ⊦ prop_dist1 (product_scalarmult F V1 V2) (V1 xop_ F V2) ❘ # product_axiom_dist1 1 2 3 ❙ product_axiom_dist2 : {F : field, V1 : vectorspace F, V2 : vectorspace F} ⊦ prop_dist2 (product_scalarmult F V1 V2) (F.plus) (V1 xop_ F V2) ❘ # product_axiom_dist2 1 2 3 ❙ ⊦ prop_dist2 (product_scalarmult F V1 V2) (F.rplus) (V1 xop_ F V2) ❘ # product_axiom_dist2 1 2 3 ❙ product_axiom_associativeScalars : {F : field, V1 : vectorspace F, V2 : vectorspace F} ⊦ prop_associative_scalars (product_scalarmult F V1 V2) (F.times) ❘ # product_axiom_associativeScalars 1 2 3 ❙ ⊦ prop_associative_scalars (product_scalarmult F V1 V2) (F.rtimes) ❘ # product_axiom_associativeScalars 1 2 3 ❙ product_axiom_unitScalars : {F : field, V1 : vectorspace F, V2 : vectorspace F} ⊦ prop_unit_scalars (product_scalarmult F V1 V2) (F.one) ❘ # product_axiom_unitScalars 1 2 3 ❙ ⊦ prop_unit_scalars (product_scalarmult F V1 V2) (F.rone) ❘ # product_axiom_unitScalars 1 2 3 ❙ productspace : {F : field} vectorspace F ⟶ vectorspace F ⟶ vectorspace F ❘ = [F] [v1] [v2] [' universe := v1 x_ F v2, ... ...
 ... ... @@ -20,6 +20,13 @@ theory Polynomials : base:?Logic = monomial : {r : ring} type ❘ # monomial 1❙ ❚ theory NumberSpaces : base:?Logic = include ?RationalField ❙ include ?Polynomials ❙ numberField : polynomialRing rationalField ⟶ ring ❙ ❚ theory RationalPolynomials : base:?Logic = include ?Polynomials ❙ include base:?Lists ❙ ... ...
 ... ... @@ -29,36 +29,36 @@ theory Rig : base:?Logic = include sets:?SetStructures/setstruct_theory ❙ structure addition : ?AbelianGroup/abeliangroup_theory = universe = `sets:?SetStructures/setstruct_theory?universe ❘ # Uadd ❙ op @ plus ❘ # 1 + 2 prec 5❙ unit @ zero ❘ # O ❙ inverse @ minus ❘ # - 1 ❙ op @ rplus ❘ # 1 + 2 prec 5❙ unit @ rzero ❘ # O ❙ inverse @ rminus ❘ # - 1 ❙ ❚ structure multiplication : ?SemiGroup/semigroup_theory = universe = `sets:?SetStructures/setstruct_theory?universe ❘ # Umult ❙ op @ times ❘ # 1 ⋅ 2 prec 6❙ op @ rtimes ❘ # 1 ⋅ 2 prec 6❙ ❚ unitset = ⟨ U | ([x] ⊦ x ≠ O) ⟩ ❙ axiom_distributive : ⊦ prop_distributive plus times ❙ unitset = ⟨ x: U | ⊦ x ≠ O ⟩ ❙ axiom_distributive : ⊦ prop_distributive rplus rtimes ❙ ❚ rig = Mod rig_theory ❘ role abbreviation ❙ rig = Mod rig_theory ❙ unitsetOf : rig ⟶ type ❘ = [r] r.unitset ❙ axiom_rigUnitsetSubtype : {r : rig} r.unitset <* r.universe ❙ additiveGroup : rig ⟶ abeliangroup ❘ = [r] [' universe := r.universe, op := r.plus , op := r.rplus , axiom_associative := r.addition/axiom_associative , unit := r.zero , unit := r.rzero , axiom_leftUnital := r.addition/axiom_leftUnital , axiom_rightUnital := r.addition/axiom_rightUnital , inverse := r.minus , inverse := r.rminus , axiom_inverse := r.addition/axiom_inverse , axiom_commutative := r.addition/axiom_commutative '] ❙ multiplicative_semigroup : rig ⟶ semigroup ❘ = [r] [' universe := r.universe, op := (r.times) , op := (r.rtimes) , axiom_associative := r.multiplication/axiom_associative '] ❙ // needs proof that ret type = unitset ❙ ❚ ... ... @@ -67,20 +67,20 @@ theory Ring : base:?Logic = // TODO needs refactoring once structures work ❙ theory ring_theory : base:?Logic = include ?Rig/rig_theory ❙ one : U ❘ # I ❙ rone : U ❘ # I ❙ axiom_oneNeqZero : ⊦ I ≠ O ❙ axiom_leftUnital : ⊦ ∀[x : U] I ⋅ x ≐ x ❙ axiom_rightUnital : ⊦ ∀[x : U] x ⋅ I ≐ x ❙ ❚ ring = Mod ring_theory ❘ role abbreviation ❙ ring = Mod ring_theory ❙ include ?Rig ❙ multiplicative_monoid : ring ⟶ monoid ❘ = [r] [' universe := r.universe, op := r.times, op := r.rtimes, axiom_associative := r.multiplication/axiom_associative, unit := r.one, unit := r.rone, axiom_leftUnital := r.axiom_leftUnital, axiom_rightUnital := r.axiom_rightUnital '] ❙ ... ...
 ... ... @@ -52,7 +52,7 @@ theory ComplexArithmetic : base:?Logic = complexAbsoluteSquared : ℂ ⟶ ℝ ❘ = [z] Re (z ⋅ cConj z) ❘ # | 1 |^ ❙ absolute : ℂ ⟶ ℝ ❘ = [z] sqrt (|z|^) ❘ # |1| ❙ nonzeroComplexNumbers : type ❘ # ℂnz ❘ = ⟨ ℂ | ([z] ⊦ Re z ≠ 0 ∧ Im z ≠ 0) ⟩❙ inverse : ℂnz ⟶ ℂ❘ # inv 1 prec 31 ❙ division: ℂ ⟶ ℂnz ⟶ ℂ ❘ = [u,z] u ⋅ (inv z) ❘ # 1 / 2 ❙ nonzeroComplexNumbers : type ❘ # ℂ* ❘ = ⟨ z : ℂ | ⊦ Re z ≠ 0 ∨ Im z ≠ 0 ⟩❙ inverse : ℂ* ⟶ ℂ❘ # inv 1 prec 31 ❙ division: ℂ ⟶ ℂ* ⟶ ℂ ❘ = [u,z] u ⋅ (inv z) ❘ # 1 / 2 ❙ ❚
 ... ... @@ -7,6 +7,7 @@ theory IntegerNumbers : base:?Logic = include base:?IntLiterals ❙ axiom_natsAreInt : nat_lit <* int_lit ❙ axiom_natsAreInt2 : NAT <* int_lit ❙ axiom_posAreInt : pos_lit <* int_lit ❙ negative : ℤ ⟶ ℤ ❘ = minus_int_lit❙ axiom_negZeroIsZero : ⊦ negative 0 ≐ 0 ❙ ... ... @@ -65,7 +66,7 @@ theory IntegerArithmetics : base:?Logic = // natissub : ℕ ≐≐ ⟨ ℤ | ([z] ⊦ ¬ z < 0) ⟩ ❙ posisneqzero : ℕ+ <* ⟨ ℤ | [x] ⊦ neq ℤ x 0 ⟩ ❙ posisneqzero : ℕ+ <* ⟨ x: ℤ | ⊦ x ≠ 0 ⟩ ❙ absolute : ℤ ⟶ ℕ ❙ // ❘ = [z] case z <0 ⟹ up (-z) . up z ❘ # | 1 | prec 10 ❙ // TODO: axioms for the other ones as well.❙ ... ...
 ... ... @@ -63,8 +63,8 @@ theory NaturalArithmetics : base:?Logic = // axiom_mod1: ⊦ ∀[n] ∀[m] n < m ⇒ (n mod m) ≐ n ❙ // axiom_mod2: ⊦ ∀[n] ∀[m] (m ≤ n) ⇒ ((n mod m) ≐ ((n - m) mod m)) ❙ primes : type ❘ = ⟨ ℕ+ | ([x] ⊦ x ≠ 1 ∧ ∀ [y : ℕ] (y | x) ⇒ (y ≐ 1 ∨ y ≐ x)) ⟩ ❙ fromOneTo : ℕ+ ⟶ type ❘ = [n] ⟨ ℕ+ | ([x] ⊦ 1 ≤ x ∧ x ≤ n) ⟩ ❙ primes : type ❘ = ⟨ x : ℕ+ | ⊦ x ≠ 1 ∧ ∀ [y : ℕ] (y | x) ⇒ (y ≐ 1 ∨ y ≐ x) ⟩ ❙ fromOneTo : ℕ+ ⟶ type ❘ = [n] ⟨ x: ℕ+ | ⊦ 1 ≤ x ∧ x ≤ n ⟩ ❙ /T Monoid Axioms ❙ axiom_associativePlus : {x: ℕ,y,z} ⊦ x + (y + z) ≐ (x + y) + z ❘ # associative_plus_nat 1 2 3❙ ... ...
 ... ... @@ -8,6 +8,7 @@ theory RationalNumbers : base:?Logic = rationalNumbers : type ❘ # ℚ ❙ axiom_intsAreRats : int_lit <* ℚ ❙ axiom_natsAreRats : nat_lit <* ℚ ❙ axiom_natsAreRats2 : NAT <* ℚ ❙ axiom_posAreRats : pos_lit <* ℚ ❙ fraction : ℤ ⟶ ℕ+ ⟶ ℚ ❘ # 1/2 ❙ ... ... @@ -35,10 +36,11 @@ theory RationalArithmetics : base:?Logic = axiom_ratTimesIsNatTimes : {x : ℤ, y : ℤ} ⊦ arithmetics?RationalArithmetics?multiplication x y ≐ arithmetics?IntegerArithmetics?multiplication x y ❙ /T Division ❙ non_zero_rationals = ⟨ x : ℚ | ⊦ x ≠ 0 ⟩ ❘ # ℚ*❙ inverse : {x:ℚ, p:⊦ x ≠ 0} ℚ ❘ # inv 1 %I2 prec 33 ❙ inverseTyped : ⟨ ℚ | ([x] ⊦ neq ℚ x 0) ⟩ ⟶ ⟨ ℚ | ([x] ⊦ neq ℚ x 0) ⟩ ❙ axiom_inv : {r : ℚ, p: ⊦ neq ℚ r 0} ⊦ r ⋅ (inv r) ≐ 1 ❘ // role Simplify ❘ # Axiom_inv_rat 1 2 ❙ axiom_inv2 : {r : ⟨ ℚ | ([x] ⊦ neq ℚ x 0) ⟩ } ⊦ r ⋅ (inverseTyped r) ≐ 1 ❘ # axiom_inv2 ❙ inverseTyped : ℚ* ⟶ ℚ* ❙ axiom_inv : {r : ℚ, p: ⊦ r ≠ 0} ⊦ r ⋅ (inv r) ≐ 1 ❘ // role Simplify ❘ # Axiom_inv_rat 1 2 ❙ axiom_inv2 : {r : ℚ* } ⊦ r ⋅ (inverseTyped r) ≐ 1 ❘ # axiom_inv2 ❙ div : {r:ℚ,s:ℚ, p:⊦ s ≠ 0} ℚ ❘ = [r,s,p] r ⋅ (inv s) ❘ # 1 / 2 %I3 prec 6 ❙ /T Exponentiation ❙ ... ...
 ... ... @@ -9,8 +9,8 @@ theory RealNumbers : base:?Logic = axiom_ratsAreReal : ℚ <* ℝ ❙ axiom_intsAreReal : ℤ <* ℝ ❙ axiom_natsAreReal : ℕ <* ℝ ❙ NAT_is_real : NAT <* ℝ ❙ axiom_posAreReal : ℕ+ <* ℝ ❙ NAT_is_real : NAT <* ℝ ❙ ❚ theory RealArithmetics : base:?Logic = ... ... @@ -34,10 +34,11 @@ theory RealArithmetics : base:?Logic = axiom_realTimesIsRatTimes : {x : ℚ, y : ℚ} ⊦ arithmetics?RealArithmetics?multiplication x y ≐ arithmetics?RationalArithmetics?multiplication x y ❙ /T Division ❙ no_zero_reals = ⟨ x : ℝ | ⊦ x ≠ 0 ⟩ ❘ # ℝ* ❙ inverse : {x:ℝ, p:⊦ x ≠ 0} ℝ ❘ # inv 1 %I2 prec 32 ❙ inverseTyped : ⟨ ℝ | ([x] ⊦ neq ℝ x 0) ⟩ ⟶ ⟨ ℝ | ([x] ⊦ neq ℝ x 0) ⟩ ❘ # inverseTyped 1 prec -1 ❙ axiom_inv : {x : ℝ, p : ⊦ neq ℝ x 0} ⊦ x ⋅ (inv x) ≐ 1 ❙ axiom_inv2 : {r : ⟨ ℝ | ([x] ⊦ neq ℝ x 0) ⟩ } ⊦ r ⋅ (inverseTyped r) ≐ 1 ❘ # axiom_inv2 ❙ inverseTyped : ℝ* ⟶ ℝ* ❘ # inverseTyped 1 prec -1 ❙ axiom_inv : {x : ℝ, p : ⊦ x ≠ 0} ⊦ x ⋅ (inv x) ≐ 1 ❙ axiom_inv2 : {r : ℝ* } ⊦ r ⋅ (inverseTyped r) ≐ 1 ❘ # axiom_inv2 ❙ div : {r:ℝ,s:ℝ, p:⊦ s ≠ 0} ℝ ❘ = [r,s,p] r ⋅ (inv s) ❘ # 1 / 2 %I3 prec 5 ❙ /T Exponentiation ❙ ... ... @@ -58,13 +59,12 @@ theory RealArithmetics : base:?Logic = axiom_realLeqIsRatLeq : {x : ℚ, y : ℚ} ⊦ arithmetics?RealArithmetics?leq x y ≐ arithmetics?RationalArithmetics?leq x y ❙ /T Subtypes ❙ NonzeroRealNumbers : type ❘ # ℝnz ❘ = ⟨ ℝ | ([x] ⊦ x ≠ 0) ⟩❙ NonNegativeRealNumbers : type ❘ # ℝ^+ ❘ = ⟨ ℝ | ([x] ⊦ x ≥ 0) ⟩❙ PositiveRealNumbers : type ❘ # ℝ+ ❘ = ⟨ ℝ | ([x] ⊦ x > 0) ⟩❙ NonNegativeRealNumbers : type ❘ # ℝ^+ ❘ = ⟨ x : ℝ | ⊦ x ≥ 0 ⟩❙ PositiveRealNumbers : type ❘ # ℝ+ ❘ = ⟨ x : ℝ | ⊦ x > 0 ⟩❙ /T Suprema ❙ // to allow for later usage of subspaces by way of a boolean function that tells whether it is part of the domain or not ❙ predAsSub : (ℝ ⟶ bool) ⟶ type ❘ = [P] ⟨ ℝ | ([z] ⊦ P z) ⟩ ❘ # pred 1 ❙ predAsSub : (ℝ ⟶ bool) ⟶ type ❘ = [P] ⟨ z : ℝ | ⊦ P z ⟩ ❘ # pred 1 ❙ sup : (ℝ ⟶ bool) ⟶ ℝ ❙ axiom_sup1 : {P : ℝ ⟶ bool, y : pred P} ⊦ y ≤ sup P ❙ axiom_sup2 : {P : ℝ ⟶ bool, y : ℝ, p : {z: pred P}⊦z ≤ y} ⊦ sup P ≤ y ❙ ... ... @@ -86,6 +86,8 @@ theory RealArithmetics : base:?Logic = theory ExtendedReals : base:?Logic = include ?RealArithmetics ❙ infty : ℝ ❘ # ∞ ❙ neginfty : ℝ ❘ = - ∞ ❘ # -∞ ❙ extended_reals : type ❘ # ℝ∞ ❙ reals_are_extended : ℝ <* ℝ∞ ❙ infty : ℝ∞ ❘ # ∞ prec 1 ❙ // TODO neginfty : ℝ∞ ❘ = - ∞ ❘ # -∞ ❙ ❚
 ... ... @@ -20,14 +20,17 @@ theory NormedSpace : base:?Logic = axiom_definiteness : ⊦ ∀[x : universe] 0.0 ≐ || x || ⇔ x ≐ unit ❙ // ⊦ ||x||≐0 ⇔ x ≐ e ❙ ❚ normedSpace : kind ❘ = Mod `?NormedSpace/normedspace_theory ❙ ❚ implicit view NormedSpaceAsMetricSpace : calculus:?MetricSpace/metricSpace_theory -> ?NormedSpace/normedspace_theory = universe = universe ❙ d = [x : universe, y : universe] || x - y ||❙ axiom_triangleInequality = sketch "follows from axiom_subadditivity" ❙ axiom_isPseudoMetric = sketch "follows from axiom_positivity, and from the symmetry in the metric as implied by multiplicativity" ❙ include calculus:?MetricSpace ❙ implicit view NormedSpaceAsMetricSpace : calculus:?MetricSpace/metricSpace_theory -> ?NormedSpace/normedspace_theory = universe = universe ❙ d = [x : universe, y : universe] || x - y ||❙ axiom_triangleInequality = sketch "follows from axiom_subadditivity" ❙ axiom_isPseudoMetric = sketch "follows from axiom_positivity, and from the symmetry in the metric as implied by multiplicativity" ❙ ❚ ❚ theory BanachSpace : base:?Logic = include ?NormedSpace ❙ ... ... @@ -35,7 +38,7 @@ theory BanachSpace : base:?Logic = theory normedmetric_theory = include ?NormedSpace/normedspace_theory ❙ structure ms : calculus:?MetricSpace/metricSpace_theory abbrev ?NormedSpaceAsMetricSpace ❙ structure ms : calculus:?MetricSpace/metricSpace_theory abbrev ?NormedSpace/NormedSpaceAsMetricSpace ❙ ❚ normedmetric = Mod normedmetric_theory ❙ ... ...
 ... ... @@ -11,10 +11,14 @@ theory ASet : base:?Logic = A : type ❙ ❚ view PowersetIsPOSet : ?POSet/poset_theory -> ?ASet = universe = set A ❙ ord = [S,T] subset A S T ❙ axiom_reflexive = lemma_subsetReflexive ❙ axiom_transitive = lemma_subsetTransitive ❙ axiom_antisymmetric = lemma_subsetAntisymmetric ❙ ❚ theory PowersetPOSet : base:?Logic = include ?POSet ❙ view PowersetIsPOSet : ?POSet/poset_theory -> ?ASet = universe = set A ❙ ord = [S,T] subset A S T ❙ axiom_reflexive = lemma_subsetReflexive ❙ axiom_transitive = lemma_subsetTransitive ❙ axiom_antisymmetric = lemma_subsetAntisymmetric ❙ ❚ ❚
 namespace http://mathhub.info/MitM/smglom/ZF ❚ import base http://mathhub.info/MitM/Foundation ❚ theory Sets : base:?Logic = Set : type ❙ element : Set ⟶ Set ⟶ prop ❘ # 1 ∈ 2 ❙ empty : Set ❘ # ∅ ❙ subset : Set ⟶ Set ⟶ prop ❘ = [s,t] ∀ [z] z ∈ s ⇒ z ∈ t ❘ # 1 ⊑ 2 ❙ disjoint : Set ⟶ Set ⟶ prop ❘ = [s,t] ¬∃[e] e ∈ s ∧ e ∈ t ❙ prop_extensionality = [s,t](∀[e] e ∈ s ⇔ e ∈ t) ⇒ s ≐ t ❙ prop_separation = [P : Set ⟶ prop][s]∃![t]∀[e]e ∈ t ⇔ (e ∈ s ∧ P e) ❙ prop_regularity = [s]s ≠ ∅ ⇒ ∃ [e] e ∈ s ∧ (disjoint s e) ❙ prop_pairing = [x,y] ∃[z] x ∈ z ∧ y ∈ z ❙ prop_pairing_unique = [x,y] ∃![z] x ∈ z ∧ y ∈ z ∧ ∀[w] w ∈ z ⇒ (w ≐ x ∨ w ≐ y) ❙ prop_union = [x] ∃![y]∀[z] z ∈ y ⇔ ∃[w] z ∈w ∧ w ∈ x ❙ prop_powerset = [x]∃![y] ∀[z] z ∈ y ⇔ z ⊑ x ❙ prop_replacement = [A][f : Set ⟶ Set] ∃![B]∀[z] (z ∈ B ⇔ ∃[a] a ∈ A ∧ z ≐ f a) ❙ ❚ theory TypeConversions : base:?Logic = include ?Sets ❙ asType : Set ⟶ type ❙ asSet : type ⟶ Set ❙ asTerm : {A,a} ⊦ a ∈ A ⟶ asType A ❘ # asTerm 2 ❙ asElem : {A : type} A ⟶ Set ❘ # asElem 2❙ axiom_asElemIsElem : {A,a : A} ⊦ (asElem a) ∈ (asSet A) ❘ # asElemIsElem 1 2❙ ❚ theory Extensionality : base:?Logic = include ?Sets ❙ axiom_extensionality : {s,t} ⊦ prop_extensionality s t ❙ ❚ theory Separation : base:?Logic = include ?Sets ❙ include base:?DescriptionOperator ❙ axiom_separation : {P,s} ⊦ prop_separation P s ❘ # separation_axiom 1 2❙ sep_constructor : {s : Set,P : Set ⟶ prop}Set ❘ = [s,P] that Set ([x] ∀[e]e ∈ x ⇔ (e ∈ s ∧ P e)) (axiom_separation P s)❘ # ≪ 1 | 2 ≫ prec -1 ❙ ❚ theory Regularity : base:?Logic = include ?Sets ❙ axiom_regularity : {s} ⊦ prop_regularity s ❙ ❚ theory Pairing : base:?Logic = include ?Sets ❙ include base:?InformalProofs ❙ axiom_pairing : {x,y} ⊦ prop_pairing x y ❙ lemma_pairing_unique : {x,y : Set} ⊦ prop_pairing_unique x y ❘ # axiom_pairing_unique 1 2 ❘ = [x,y] sketch "provable" ❙ ❚ theory KuratowskiPairs : base:?Logic = include ?Pairing ❙ include ?Separation ❙ include base:?InformalProofs ❙ uopair : Set ⟶ Set ⟶ Set ❘ = [x,y] that Set ([z] x ∈ z ∧ y ∈ z ∧ ∀[w] w ∈ z ⇒ (w ≐ x ∨ w ≐ y)) (lemma_pairing_unique x y) ❙ pair : Set ⟶ Set ⟶ Set ❘ = [x,y] uopair (uopair x y) x ❙ singleton : Set ⟶ Set ❘ = [s] uopair s s ❙ ❚ theory Union : base:?Logic = include ?Sets ❙ include base:?DescriptionOperator ❙ axiom_union : {x} ⊦ prop_union x ❘ # axiom_union 1❙ union : Set ⟶ Set ❘ = [s] that Set ([x] ∀[z] z ∈ x ⇔ ∃[w] z ∈w ∧ w ∈ s) (axiom_union s) ❘ # ⋃ 1 ❙ ❚ theory BinaryUnion : base:?Logic = include ?KuratowskiPairs ❙ include ?Union ❙ binaryunion : Set ⟶ Set ⟶ Set ❘ = [a,b] ⋃ (uopair a b) ❘ # 1 ∪ 2❙ ❚ theory Powerset : base:?Logic = include ?Sets ❙ include base:?DescriptionOperator ❙ axiom_powerset : {x} ⊦ prop_powerset x ❘ # axiom_powerset 1❙ powerset : Set ⟶ Set ❘ = [x] that Set ([y] ∀[z] z ∈ y ⇔ z ⊑ x) (axiom_powerset x) ❘ # ℘ 1 ❙ ❚ theory CartesianProduct : base:?Logic = include ?Powerset ❙ include ?Separation ❙ include ?BinaryUnion ❙ product : Set ⟶ Set ⟶ Set ❘ = [A,B] sep_constructor (℘ (℘ (A ∪ B))) ([p] ∃[a]∃[b] a ∈ A ∧ b ∈ B ∧ p ≐ pair a b) ❘ # 1 × 2 ❙ ❚ theory Relations : base:?Logic = include ?CartesianProduct ❙ include base:?Subtyping ❙ // include ?TypeConversions ❙ prop_relation = [s,A,B : Set] s ⊑ (A × B) ❘ # is_relation 1 2 3❙ relation : Set ⟶ Set ⟶ type ❘= [A,B] ⟨ Set | ([s] ⊦ prop_relation s A B) ⟩ ❙ // RelAsSet : {A,B : type} (A ⟶ B ⟶ prop) ⟶ relation (asSet A) (asSet B) ❘ = [A,B,R] coerce (asElem R) ❙ ❚ theory Functions : base:?Logic = include ?Relations ❙ prop_function = [f,A,B] prop_relation f A B ∧ ∀[x] x ∈ A ⇒ ∃[y] y ∈ B ∧ (pair x y) ∈ f ❙ // TODO ❙ function : Set ⟶ Set ⟶ type ❘= [A,B] ⟨ Set | ([s] ⊦ prop_relation s A B) ⟩ ❙ // FunAsSet : {A, B : type} (A ⟶ B ⟶ prop) ⟶ function (asSet A) (asSet B) ❘ = [A,B,f] coerce (asElem f) ❙ setfunapply : {A,B} function A B ⟶ {a : Set}⊦ a ∈ A ⟶ Set ❘ = [A,B,f,a,p] ι ([x] (pair a x) ∈ f) ❘ # 3 @ 4 %I5 ❙ theorem_setfun : {A,B,f : function A B, a} ⊦ (f @ a) ∈ B ❙ ❚ theory Replacement : base:?Logic = include ?Sets ❙ include base:?DescriptionOperator ❙ axiom_replacement : {a,f} ⊦ prop_replacement a f ❘ # axiom_replacement 1 2❙ replacement : Set ⟶ (Set ⟶ Set) ⟶ Set ❘ = [A,f] that Set ([B] ∀[z] (z ∈ B ⇔ ∃[a] a ∈ A ∧ z ≐ f a)) (axiom_replacement A f) ❘ # Im 2 of 1 ❙ ❚ theory Infinity : base:?Logic = include ?BinaryUnion ❙ prop_infinity = [N] ∅ ∈ N ∧ ∀[n] n ∈ N ⇒ (n ∪ (singleton n)) ∈ N ❙ omega : Set ❘ # ω ❘ = ι [x] prop_infinity x ∧ ∀[z] prop_infinity z ⇒ x ⊑ z❙ ❚ theory Naturals : base:?Logic = include ?Infinity ❙ include base:?NatLiterals ❙ asSet : ℕ ⟶ Set ❙ axiom_asSetIsNat : {n} ⊦ (asSet n) ∈ ω ❙ axiom_asSetZeroIsEmpty : ⊦ (asSet 0) ≐ ∅ ❙ axiom_asSetSucc : {n} ⊦ (asSet (nat_lit_succ n)) ≐ (asSet n) ∪ (singleton (asSet n)) ❙ ❚ theory ZF : base:?Logic = include ?Extensionality ❙ include ?Separation ❙ include ?Regularity ❙ include ?Pairing ❙ include ?Union ❙ include ?Powerset ❙ include ?Replacement ❙ include ?Infinity ❙ ❚ theory Choice : base:?Logic = include ?Functions ❙ prop_choiceFunction = [A,f : function A (⋃ A)] ∀[a] a ∈ A ⇒ (f @ a) ∈ a ❙ ❚
 ... ... @@ -17,17 +17,17 @@ theory OpenSetTopology : base:?Logic = axiom_intersection: ⊦ prop_finiteIntersection coll ❙ ❚ topology = [X : type] Mod `?OpenSetTopology/topology_theory , X ❘ role abbreviation❙ topology = [X : type] Mod `?OpenSetTopology/topology_theory , X❙ topologicalSpace : kind ❘ = {' universe : type , topology : topology universe '} ❘ role abbreviation❙ '}❙ topologyOf : {G: topologicalSpace} collection (dom G) ❘ = [G] (G.topology).coll ❘ # topologyOf 1 ❙ topologyOf : {G: topologicalSpace} collection (G.universe) ❘ = [G] (G.topology).coll ❘ # topologyOf 1 ❙ isOpen : {G : topologicalSpace} set (dom G) ⟶ prop ❘ = [G,S] S ∈ (topologyOf G) ❘ # open 2❙ isClosed : {G : topologicalSpace} set (dom G) ⟶ prop ❘= [G,S] ((doms G)\ S) ∈ (topologyOf G) ❘ # closed 2❙ isClopen : {G : topologicalSpace} set (dom G) ⟶ prop ❘ = [G,S] closed S ∧ open S ❙ isOpen : {G : topologicalSpace} set (G.universe) ⟶ prop ❘ = [G,S] S ∈ (topologyOf G) ❘ # open 2❙ isClosed : {G : topologicalSpace} set (G.universe) ⟶ prop ❘= [G,S] ((doms G)\ S) ∈ (topologyOf G) ❘ # closed 2❙ isClopen : {G : topologicalSpace} set (G.universe) ⟶ prop ❘ = [G,S] closed S ∧ open S ❙ ❚ ... ... @@ -84,7 +84,7 @@ theory ClosureInterior : base:?Logic = include ?OpenSetTopology ❙ closure : {G : topologicalSpace} set (G.universe) ⟶ set (G.universe) ❘ = [G,S] ⋃ ⟪ topologyOf G | ([T] closed T ∧ S ⊑ T) ⟫ ([T] T) ❘ # closure 2❙ interior : {G : topologicalSpace} set (dom G) ⟶ set (dom G)❘ interior : {G : topologicalSpace} set (G.universe) ⟶ set (G.universe)❘ = [G,S] ⋂ ⟪ topologyOf G | ([T] open T ∧ T ⊑ S) ⟫ ([T] T) ❘ # interior 2 ❙ boundary : {G : topologicalSpace} set (G.universe) ⟶ set (G.universe) ❘ = [G,S] closure S \ interior S ❘ # boundary 2❙ ... ... @@ -98,7 +98,7 @@ theory Neighborhood : base:?Logic = theory LimitPoint : base:?Logic = include ?Neighborhood ❙ limitPoint : {G : topologicalSpace} (dom G) ⟶ set (dom G) ⟶ prop ❘ limitPoint : {G : topologicalSpace} (G.universe) ⟶ set (G.universe) ⟶ prop ❘ = [G][a,S] S ⊑ doms G ∧ a ∈ S ∧ ∀[N : set (dom G)] neighborhood N a ⇒ ∃[b] b ∈ N ∧ ¬ a ≐ b ❙ ❚ ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!