update to use the new syntax

mathlingua · Feb 4, 2024 · 66076e4 · 66076e4
1 parent 97760e1
commit 66076e4
Show file tree

Hide file tree

Showing 19 changed files with 70 additions and 70 deletions.
diff --git a/algebra/field.math b/algebra/field.math
@@ -19,7 +19,7 @@ when:
 . 'F is \field'
 . 'x [.in.]: F'
 means: 'y [.in.]: F'
-specifies:
+expresses:
 . 'x * y = 1'
 . 'y * x = 1'
 Documented:
@@ -37,7 +37,7 @@ extends: 'x is \ring.element:of{R}'
 Provides:
 . symbol: 'x.inv :=> \field.multiplicative.inverse:of{x}:in{F}'
   written: "{x+}?^{-1}"
-. '-x :=> (F as \[abelian.group]).inv(x)'
+. '-x :=> (F as \:abelian.group).inv(x)'
 . 'x + y :=> x [.F.+.]: y'
 . 'x * y :=> x [.F.*.]: y'
 . 'x - y :=> x + (-y)'

diff --git a/algebra/group.math b/algebra/group.math
@@ -5,7 +5,7 @@
 [\group]
 Describes: G := (X, *, e)
 extends: 'G is \monoid'
-satisfies:
+specifies:
 . [existence.of.inverses]
   forAll: x
   where: 'x [.in.]: G'
@@ -42,7 +42,7 @@ Id: "5291b552-c380-4ac3-ad58-8d86ea8de9af"
 [\finite.group]
 Describes: G := (X, *, e)
 extends: 'X is \set'
-satisfies: 'X is \finite.set'
+specifies: 'X is \finite.set'
 Documented:
 . called: "finite group"
 ------------------------------------------
@@ -53,7 +53,7 @@ Id: "404e418f-9ab4-4080-9dfd-ff8054f3f555"
 Describes: H := (Y, *_0, u)
 when: 'G is \group'
 extends: 'Y is \set'
-satisfies:
+specifies:
 . 'Y [.subset.]: X'
 . 'Y is \non.empty.set'
 . forAll: x, y
@@ -99,7 +99,7 @@ when:
 . 'G is \group'
 . 'x [.in.]: G'
 means: 'y [.in.]: G'
-specifies:
+expresses:
 . 'x * y = e'
 . 'y * x = e'
 Justified:
@@ -120,7 +120,7 @@ when:
 . 'x [.in.]: G'
 . 'n is \natural'
 means: 'y [.in.]: G'
-specifies:
+expresses:
 . piecewise:
   if: 'n = 0'
   then: 'y = e'
@@ -139,7 +139,7 @@ Id: "1aaf732a-1987-4ee2-860e-98adf261b5f6"
 [G1 := (X1, *_1, e1) \group.direct.product/ G2 := (X2, *_2, e2)]
 Defines: H := (Y, +, u)
 when: 'G1, G2 is \group'
-specifies:
+expresses:
 . 'Y := X1 \set.times/ X2'
 . 'u := (e1, e2)'
 Documented:
@@ -163,7 +163,7 @@ Id: "bba5ed08-adfd-4465-8192-d60f2998a271"
 [\abelian.group]
 Describes: G
 extends: 'G is \group'
-satisfies:
+specifies:
 . forAll: x, y
   where: 'x, y [.in.]: G'
   then: 'x * y = y * x'
@@ -222,7 +222,7 @@ Id: "6dcccfc0-be83-489a-9c2e-040e61bce8f7"
 Defines: k
 when: 'P is \\formulation{statement}'
 means: 'k is \natural'
-specifies:
+expresses:
 . 'P(k)'
 . not:
   . exists: j
@@ -242,7 +242,7 @@ when:
 . 'G is \group'
 . 'n is \natural'
 means: 'n is \natural'
-specifies:
+expresses:
 . 'n := \smallest.natural:suchThat[k]{x^k = e}'
 Documented:
 . called: "\textrm{order of } x? \textrm{ in group } G?"

diff --git a/algebra/magma.math b/algebra/magma.math
@@ -5,7 +5,7 @@
 [\magma]
 Describes: M := (X, *)
 extends: 'X is \set'
-satisfies: '"*" is \binary.operation:on{M}'
+specifies: '"*" is \binary.operation:on{M}'
 Provides:
 . symbol: 'x [.in.]: M :-> x is \magma.element:of{M}'
   written: "x? \in M?"

diff --git a/algebra/module.math b/algebra/module.math
@@ -6,7 +6,7 @@
 Describes: M := (R, G, *)
 when: 'R0 is \ring'
 extends: 'G is \group'
-satisfies:
+specifies:
 . 'R := R0'
 . '"*" is \function:on{R, G}:to{G}'
 . [scalar.multiplication]
@@ -51,7 +51,7 @@ Id: "b31db455-e075-4e67-823e-65d76087290a"
 Describes: M
 when: 'R is \ring.with.identity'
 extends: 'M is \left.module:over{R}'
-satisfies:
+specifies:
 . forAll: x
   where: 'x [.in.]: M'
   then: 'R.1 * x = x'
@@ -76,7 +76,7 @@ Id: "9e4db744-9571-4952-8f91-4ccb0873d788"
 Describes: M := (R, G, *)
 when: 'R0 is \ring'
 extends: 'G is \group'
-satisfies:
+specifies:
 . 'R := R0'
 . '"*" is \function:on{G, R}:to{G}'
 . [scalar.multiplication]
@@ -121,7 +121,7 @@ Id: "d8a4d363-63ff-4bc4-b0d1-60336739c587"
 Describes: M
 when: 'R is \ring.with.identity'
 extends: 'M is \right.module:over{R}'
-satisfies:
+specifies:
 . forAll: x
   where: 'x [.in.]: M'
   then: 'x * R.1  = x'

diff --git a/algebra/monoid.math b/algebra/monoid.math
@@ -5,7 +5,7 @@
 [\monoid]
 Describes: M := (X, *, e)
 extends: '(X, "*") is \semigroup'
-satisfies:
+specifies:
 . 'e [.in.]: M'
 . forAll: x
   where: 'x [.in.]: M'

diff --git a/algebra/operations.math b/algebra/operations.math
@@ -16,7 +16,7 @@ Id: "0b0939af-e4a8-4c4d-b8fc-beba6a9e516c"
 Describes: x * y
 when: 'X is \set'
 extends: '"*" is \binary.operation:on{X}'
-satisfies:
+specifies:
 . forAll: x, y, z
   where: 'x, y, z [.in.]: X'
   then: 'x * (y * z) = (x * y) * z'
@@ -30,7 +30,7 @@ Id: "4e45d31a-56d0-452c-8a94-38c09335cf2b"
 Describes: x * y
 when: 'X is \set'
 extends: '"*" is \binary.operation:on{X}'
-satisfies:
+specifies:
 . forAll: x, y
   where: 'x, y [.in.]: X'
   then: 'x * y = y * x'
@@ -45,7 +45,7 @@ Describes: x * y
 using: X
 when: 'Y [.subset.]: X'
 extends: '"*" is \binary.operation:on{X}'
-satisfies:
+specifies:
 . forAll: a, b
   where: 'a, b [.in.]: Y'
   then: 'a * b [.in.]: Y'

diff --git a/algebra/quasigroup.math b/algebra/quasigroup.math
@@ -5,7 +5,7 @@
 [\quasigroup]
 Describes: Q := (X, *)
 extends: 'Q is \magma'
-satisfies:
+specifies:
 . [latin.square.property]
   forAll: a, b
   where: 'a, b [.in.]: Q'

diff --git a/algebra/ring.math b/algebra/ring.math
@@ -8,7 +8,7 @@ Describes: R := (X, +, *, 0)
 extends:
 . '(X, "+", 0) is \abelian.group'
 . '(X, "*") is \semigroup'
-satisfies:
+specifies:
 . [distributive.law]
   forAll: x, y, z
   where: 'x, y, z [.in.]: R'
@@ -61,7 +61,7 @@ Id: "7e9002e6-4aa3-4312-b113-798474c70e0f"
 [\commutative.ring]
 Describes: R
 extends: 'R is \ring'
-satisfies:
+specifies:
 . forAll: x, y
   where: 'x, y [.in.]: R'
   then: 'x * y = y * x'
@@ -83,7 +83,7 @@ Id: "57d40c75-7b95-4680-ac65-414efa306beb"
 [\trivial.ring]
 Defines: R := (X, +, *, 0)
 means: 'R is \ring'
-specifies:
+expresses:
 . define: x + y
   as: 'x + y := 0'
 . define: x * y
@@ -100,7 +100,7 @@ Id: "bcff7894-7ec2-44eb-ae00-6e445ef19c9a"
 [\nontrivial.ring]
 Describes: R
 extends: 'R is \ring'
-satisfies: 'R != \trivial.ring'
+specifies: 'R != \trivial.ring'
 Documented:
 . called: "non-trivial ring"
 ------------------------------------------
@@ -110,7 +110,7 @@ Id: "029fa21a-8527-4a08-9035-d5a29d8014f6"
 [\division.ring]
 Describes: R
 extends: 'R is \ring.with.identity'
-satisfies:
+specifies:
 . '0 != 1'
 . forAll: x
   where: 'x [.in.]: R'

diff --git a/algebra/semigroup.math b/algebra/semigroup.math
@@ -5,7 +5,7 @@
 [\semigroup]
 Describes: S := (X, *)
 extends: 'S is \magma'
-satisfies: '"*" is \associative.binary.operation:on{S}'
+specifies: '"*" is \associative.binary.operation:on{S}'
 Provides:
 . symbol: 'x [.in.]: S :-> x is \semigroup.element:of{S}'
   written: "x? \in S?"

diff --git a/analysis/metric_space.math b/analysis/metric_space.math
@@ -6,7 +6,7 @@
 Describes: d(x, y)
 when: 'X is \set'
 extends: 'd is \function:on{X, X}:to{\reals}'
-satisfies:
+specifies:
 . forAll: x
   where: 'x [.in.]: X'
   then: 'd(x, x) = 0'
@@ -32,7 +32,7 @@ Id: "be627b13-bda3-4e72-955e-4b960f2b123c"
 [\metric.space]
 Describes: M := (X, d)
 extends: 'X is \set'
-satisfies: 'd is \metric:on{X}'
+specifies: 'd is \metric:on{X}'
 Documented:
 . called: "metric space"
 ------------------------------------------

diff --git a/function.math b/function.math
@@ -10,7 +10,7 @@ is that it maps an input to a *unique* output.
 [\function:on{A...}:to{B}]
 Describes: f(x...)
 when: 'A..., B is \set'
-satisfies:
+specifies:
 . 'x... [.in.]: A...'
 . 'f(x) [.in.]: B'
 . forAll: a
@@ -42,7 +42,7 @@ Note: These types of functions are also said to be *one-to-one*.
 Describes: f(x)
 when: 'A, B is \set'
 extends: 'f is \function:on{A}:to{B}'
-satisfies:
+specifies:
 . forAll: x1, x2
   where: 'x1, x2 [.in.]: A'
   then:
@@ -77,7 +77,7 @@ element.  Surjective functions are also said to be *onto*.
 Describes: f(x)
 when: 'A, B is \set'
 extends: 'f is \function:on{A}:to{B}'
-satisfies:
+specifies:
 . forAll: b
   where: 'b [.in.]: B'
   then:
@@ -123,7 +123,7 @@ Defines: g(x)
 using: A, B
 when: 'f is \function:on{A}:to{B}'
 means: 'g is \function:on{B}:to{A}'
-specifies:
+expresses:
 . forAll: a
   where: 'a [.in.]: A'
   then: 'g(f(a)) = a'
@@ -150,7 +150,7 @@ when:
 . 'g is \function:on{A}:to{B}'
 . 'f is \function:on{B}:to{C}'
 means: 'h is \function:on{A}:to{C}'
-specifies: 'h(x) := f(g(x))'
+expresses: 'h(x) := f(g(x))'
 Documented:
 . written: "f+? \circ g+?"
 . called: "function composition"
@@ -169,7 +169,7 @@ structure.
 Defines: f(x)
 when: 'A is \set'
 means: 'f is \function:on{A}:to{A}'
-specifies: 'f(x) := x'
+expresses: 'f(x) := x'
 Documented:
 . written: "\textrm{id}_{A?}"
 . called: "identify function on $A?$"

diff --git a/integers.math b/integers.math
@@ -14,7 +14,7 @@ Id: "67ba0d5c-d30c-4c1f-85e0-60b9efba44d5"
 [\integer.set]
 Defines: X
 means: 'X is \set'
-specifies: 'X := \set:of[x]{x | x is \integer}'
+expresses: 'X := \set:of[x]{x | x is \integer}'
 Documented:
 . written: "\mathbb{Z}"
 ------------------------------------------
@@ -24,7 +24,7 @@ Id: "5f310f77-f89c-4094-8b39-aab057b03720"
 [\integers]
 Defines: Z := (X, +, *, 0, 1)
 means: 'X is \set'
-specifies: 'X := \integer.set'
+expresses: 'X := \integer.set'
 Provides: 'x [.in.]: Z :-> x [.in.]: X'
 Documented:
 . written: "\mathbb{Z}"

diff --git a/naturals/introduction.math b/naturals/introduction.math
@@ -4,7 +4,7 @@
 
 [\natural.succ(n)]
 Defines: f(n)
-specifies:
+expresses:
 . 'n is \natural'
 . 'f(n) is \natural'
 Documented:
@@ -16,7 +16,7 @@ Id: "5826e12b-34e7-441f-8002-336d002e0ac5"
 
 [\natural]
 Describes: n
-satisfies:
+specifies:
 . anyOf:
   . 'n = 0'
   . exists: m
@@ -66,7 +66,7 @@ Id: "6214d07e-66f8-471d-a528-3c243ccf7fc7"
 [\natural.set]
 Defines: N
 means: 'N is \set'
-specifies: 'N := \set:of[n]{n | n is \natural}'
+expresses: 'N := \set:of[n]{n | n is \natural}'
 Documented:
 . written: "\mathbb{N}"
 . called: "the set of natural numbers"
@@ -76,7 +76,7 @@ Id: "fd98138f-b329-4b31-ab42-d8e52a149bfc"
 
 [\naturals]
 Defines: N := (X, 0, succ(x))
-specifies:
+expresses:
 . 'X := \natural.set'
 . '0 := \natural.0'
 . 'succ(x) := \natural.succ(x)'

diff --git a/naturals/operations.math b/naturals/operations.math
@@ -21,7 +21,7 @@ Id: "e4967613-c907-48cb-a459-4c2813f6250f"
 
 [n \natural.+/ m]
 Defines: n + m
-specifies:
+expresses:
 . piecewise:
   if: 'n = 0'
   then: 'n + m := m'
@@ -96,7 +96,7 @@ Id: "91369cbd-3a99-4845-8e3a-6e4fadd47c3d"
 [n \natural.*/ m]
 Defines: n * m
 when: 'n, m is \natural'
-specifies:
+expresses:
 . piecewise:
   if: 'n = 0'
   then: 'n * m = 0'

diff --git a/naturals/positive_naturals.math b/naturals/positive_naturals.math
@@ -5,7 +5,7 @@
 [\positive.natural]
 Describes: n
 extends: 'n is \natural'
-satisfies: 'n != 0'
+specifies: 'n != 0'
 Documented:
 . called: "positive natural number"
 ------------------------------------------