Fix exponents and bold definitions

blueprint/src/content.tex

@@ -99,13 +99,13 @@ \section{Content}
 \begin{lemma}\label{split_first_and_last}\lean{split_first_and_last_factor_of_product}\leanok
 Let $a$ and $b$ be elements of a semigroup $S$.
 
-For all $n > 1$, $(a*b)^n = a * (b+a)^(n-1) * b$.
+For all $n > 1$, $(a*b)^n = a * (b+a)^{n-1} * b$.
 \end{lemma}
 \begin{proof}
-Let $n=2$. Then $(a+b)^2 = a * (b*a)^(2-1) * b$.
+Let $n=2$. Then $(a+b)^2 = a * (b*a)^{2-1} * b$.
 
 Assume that the statement holds for $n$.
-Then we have that $(a*b)^(n+1) = a * b * (a*b)^n = a * b * a * (b*a)^(n-1) * b = a * (b*a)^n * b$.
+Then we have that $(a*b)^{n+1} = a * b * (a*b)^n = a * b * a * (b*a)^{n-1} * b = a * (b*a)^n * b$.
 \end{proof}
 
 \begin{lemma}\label{thm:comm_ineq}\lean{comm_factor_le, comm_swap_le, comm_dist_le}\leanok
@@ -120,47 +120,47 @@ \section{Content}
 Assume that the statement holds for $n$.
 Then we have that
 \begin{align}
-a^(n+1) + b^(n+1) &= a * a^n * b^n * b \\
+a^{n+1} + b^{n+1} &= a * a^n * b^n * b \\
 \text{by the induction hypothesis}\\
 &< a * (a * b)^n * b \\
 \text{since $a*b < b*a$}\\
 &< a * (b * a)^n * b \\
 \text{by the previous lemma}\\
-&= (a * b)^(n+1) \\
-&< (b * a)^(n+1) \\
+&= (a * b)^{n+1} \\
+&< (b * a)^{n+1} \\
 \text{by the previous lemma}\\
 &= b * (a * b)^n * a \\
 &< b * (b * a)^n * a \\
 \text{by the induction hypothesis}\\
 &< b * b^n * a^n * a \\
-&= b^(n+1) * a^(n+1)
+&= b^{n+1} * a^{n+1}
 \end{align}
 \end{proof}
 
 \begin{definition}\label{def:arch_wrt}\lean{is_archimedean_wrt}\leanok
 \uses{def:positive, def:negative}
 Let $a$ and $b$ be elements of an ordered semigroup $S$ that are not one.
 
-Then $a$ is said to be Archimedean with respect to $b$
+Then $a$ is said to be \textbf{Archimedean with respect to} $b$
 if there exists an $N\in \mathbb{N}^+$ such that for $n > N$,
 the inequality $b < a^n$ holds if $b$ is positive,
 and the inequality $b > a^n$ holds if $b$ is negative.
 \end{definition}
 
 \begin{definition}\label{def:arch}\lean{is_archimedean}\leanok
 \uses{def:one, def:arch_wrt}
-An ordered semigroup is Archimedean if any two of its elements
+An ordered semigroup is \textbf{Archimedean} if any two of its elements
 of the same sign are mutually Archimedean.
 \end{definition}
 
 \begin{definition}\label{def:anomalous_pair}\lean{anomalous_pair}\leanok
 Let $a$ and $b$ be elements of an ordered semigroup $S$.
 
-Then $a$ and $b$ are said to form an anomalous pair
+Then $a$ and $b$ are said to form an \textbf{anomalous pair}
 if for all $n\in \mathbb{N}^+$, one of the following holds
 \begin{align}
-a^n < b^n < a^(n+1) \\
-a^n > b^n > a^(n+1)
+a^n < b^n < a^{n+1} \\
+a^n > b^n > a^{n+1}
 \end{align}
 \end{definition}
 
@@ -183,7 +183,7 @@ \section{Content}
 \]
 which means that, since $a^n < b$,
 \[
-b^n < (a*b)^n < b^(n+1)
+b^n < (a*b)^n < b^{n+1}
 \]
 And so $b$ and $a*b$ form an anomalous pair.
 

blueprint/web/dep_graph_document.html

@@ -104,9 +104,9 @@ <h1 id="doc_title">Dependencies</h1>
       </span>
       <span class="definition_thmlabel">10</span></div>
     <div class="thm_thmcontent"><p>Let \(a\) and \(b\) be elements of an ordered semigroup \(S\). </p>
-<p>Then \(a\) and \(b\) are said to form an anomalous pair if for all \(n\in \mathbb {N}^+\), one of the following holds </p>
+<p>Then \(a\) and \(b\) are said to form an <b class="bfseries">anomalous pair</b> if for all \(n\in \mathbb {N}^+\), one of the following holds </p>
 <div class="displaymath" id="a0000000010">
-  \begin{align}  a^n {\lt} b^n {\lt} a^(n+1) \\ a^n {\gt} b^n {\gt} a^(n+1) \end{align}
+  \begin{align}  a^n {\lt} b^n {\lt} a^{n+1} \\ a^n {\gt} b^n {\gt} a^{n+1} \end{align}
 </div>
 </div>
 
@@ -137,7 +137,7 @@ <h1 id="doc_title">Dependencies</h1>
       Definition
       </span>
       <span class="definition_thmlabel">9</span></div>
-    <div class="thm_thmcontent"><p> An ordered semigroup is Archimedean if any two of its elements of the same sign are mutually Archimedean. </p>
+    <div class="thm_thmcontent"><p> An ordered semigroup is <b class="bfseries">Archimedean</b> if any two of its elements of the same sign are mutually Archimedean. </p>
 </div>
 
     <a class="latex_link" href="index.html#def:arch">LaTeX</a>
@@ -168,7 +168,7 @@ <h1 id="doc_title">Dependencies</h1>
       </span>
       <span class="definition_thmlabel">8</span></div>
     <div class="thm_thmcontent"><p> Let \(a\) and \(b\) be elements of an ordered semigroup \(S\) that are not one. </p>
-<p>Then \(a\) is said to be Archimedean with respect to \(b\) if there exists an \(N\in \mathbb {N}^+\) such that for \(n {\gt} N\), the inequality \(b {\lt} a^n\) holds if \(b\) is positive, and the inequality \(b {\gt} a^n\) holds if \(b\) is negative. </p>
+<p>Then \(a\) is said to be <b class="bfseries">Archimedean with respect to</b> \(b\) if there exists an \(N\in \mathbb {N}^+\) such that for \(n {\gt} N\), the inequality \(b {\lt} a^n\) holds if \(b\) is positive, and the inequality \(b {\gt} a^n\) holds if \(b\) is negative. </p>
 </div>
 
     <a class="latex_link" href="index.html#def:arch_wrt">LaTeX</a>
@@ -258,7 +258,7 @@ <h1 id="doc_title">Dependencies</h1>
       Definition
       </span>
       <span class="definition_thmlabel">6</span></div>
-    <div class="thm_thmcontent"><p> An element \(a\) of an ordered semigroup \(S\) is <b class="bfseries">negative</b> if for all \(x\in S\), \(a*x \lt x\). </p>
+    <div class="thm_thmcontent"><p> An element \(a\) of an ordered semigroup \(S\) is <b class="bfseries">negative</b> if for all \(x\in S\), \(a*x {\lt} x\). </p>
 </div>
 
     <a class="latex_link" href="index.html#def:negative">LaTeX</a>
@@ -384,7 +384,7 @@ <h1 id="doc_title">Dependencies</h1>
       Definition
       </span>
       <span class="definition_thmlabel">5</span></div>
-    <div class="thm_thmcontent"><p> An element \(a\) of an ordered semigroup \(S\) is <b class="bfseries">positive</b> if for all \(x\in S\), \(a*x \gt x\). </p>
+    <div class="thm_thmcontent"><p> An element \(a\) of an ordered semigroup \(S\) is <b class="bfseries">positive</b> if for all \(x\in S\), \(a*x {\gt} x\). </p>
 </div>
 
     <a class="latex_link" href="index.html#def:positive">LaTeX</a>
@@ -489,7 +489,7 @@ <h1 id="doc_title">Dependencies</h1>
       </span>
       <span class="lemma_thmlabel">1</span></div>
     <div class="thm_thmcontent"><p>Let \(a\) and \(b\) be elements of a semigroup \(S\). </p>
-<p>For all \(n {\gt} 1\), \((a*b)^n = a * (b+a)^(n-1) * b\). </p>
+<p>For all \(n {\gt} 1\), \((a*b)^n = a * (b+a)^{n-1} * b\). </p>
 </div>
 
     <a class="latex_link" href="index.html#split_first_and_last">LaTeX</a>
@@ -629,7 +629,7 @@ <h1 id="doc_title">Dependencies</h1>
     .width(width)
     .height(height)
     .fit(true)
-    .renderDot(`strict digraph "" {	graph [bgcolor=transparent];	node [label="\N",		penwidth=1.8	];	edge [arrowhead=vee];	"thm:neg_lt_pos"	[color=green,		fillcolor="#A3D6FF",		label=neg_lt_pos,		shape=ellipse,		style=filled];	"lem:right_forall"	[color=green,		label=right_forall,		shape=ellipse];	non_arch_anomalous	[color=green,		fillcolor="#A3D6FF",		label=non_arch_anomalous,		shape=ellipse,		style=filled];	"def:OrderedSemigroup"	[color=green,		fillcolor="#B0ECA3",		label=OrderedSemigroup,		shape=box,		style=filled];	"def:positive"	[color=green,		fillcolor="#B0ECA3",		label=positive,		shape=box,		style=filled];	"def:OrderedSemigroup" -> "def:positive"	[style=dashed];	"def:OrderedCancelSemigroup"	[color=green,		fillcolor="#B0ECA3",		label=OrderedCancelSemigroup,		shape=box,		style=filled];	"def:OrderedSemigroup" -> "def:OrderedCancelSemigroup"	[style=dashed];	"def:LinearOrderedSemigroup"	[color=green,		fillcolor="#B0ECA3",		label=LinearOrderedSemigroup,		shape=box,		style=filled];	"def:OrderedSemigroup" -> "def:LinearOrderedSemigroup"	[style=dashed];	"def:negative"	[color=green,		fillcolor="#B0ECA3",		label=negative,		shape=box,		style=filled];	"def:OrderedSemigroup" -> "def:negative"	[style=dashed];	"def:one"	[color=green,		fillcolor="#B0ECA3",		label=one,		shape=box,		style=filled];	"def:OrderedSemigroup" -> "def:one"	[style=dashed];	"def:positive" -> "thm:neg_lt_pos"	[style=dashed];	"def:positive" -> "lem:right_forall"	[style=dashed];	"def:arch_wrt"	[color=green,		fillcolor="#B0ECA3",		label=arch_wrt,		shape=box,		style=filled];	"def:positive" -> "def:arch_wrt"	[style=dashed];	"thm:pos_neg_or_one"	[color=green,		fillcolor="#A3D6FF",		label=pos_neg_or_one,		shape=ellipse,		style=filled];	"def:positive" -> "thm:pos_neg_or_one"	[style=dashed];	"def:LinearOrderedCancelSemigroup"	[color=green,		fillcolor="#B0ECA3",		label=LinearOrderedCancelSemigroup,		shape=box,		style=filled];	"def:OrderedCancelSemigroup" -> "def:LinearOrderedCancelSemigroup"	[style=dashed];	"def:negative" -> "thm:neg_lt_pos"	[style=dashed];	"def:negative" -> "lem:right_forall"	[style=dashed];	"def:negative" -> "def:arch_wrt"	[style=dashed];	"def:negative" -> "thm:pos_neg_or_one"	[style=dashed];	"def:one" -> "lem:right_forall"	[style=dashed];	"def:one" -> "thm:pos_neg_or_one"	[style=dashed];	"def:arch"	[color=green,		fillcolor="#B0ECA3",		label=arch,		shape=box,		style=filled];	"def:one" -> "def:arch"	[style=dashed];	"def:arch_wrt" -> "def:arch"	[style=dashed];	"def:LinearOrderedCancelSemigroup" -> "thm:pos_neg_or_one"	[style=dashed];	"def:arch" -> non_arch_anomalous	[style=dashed];	"def:anomalous_pair"	[color=green,		fillcolor="#B0ECA3",		label=anomalous_pair,		shape=box,		style=filled];	"def:anomalous_pair" -> non_arch_anomalous	[style=dashed];	split_first_and_last	[color=green,		fillcolor="#A3D6FF",		label=split_first_and_last,		shape=ellipse,		style=filled];	a0000000014	[color=blue,		fillcolor="#A3D6FF",		label=a0000000014,		shape=ellipse,		style=filled];	"thm:comm_ineq"	[color=green,		fillcolor="#A3D6FF",		label=comm_ineq,		shape=ellipse,		style=filled];}`)
+    .renderDot(`strict digraph "" {	graph [bgcolor=transparent];	node [label="\N",		penwidth=1.8	];	edge [arrowhead=vee];	split_first_and_last	[color=green,		fillcolor="#A3D6FF",		label=split_first_and_last,		shape=ellipse,		style=filled];	"lem:right_forall"	[color=green,		label=right_forall,		shape=ellipse];	non_arch_anomalous	[color=green,		fillcolor="#A3D6FF",		label=non_arch_anomalous,		shape=ellipse,		style=filled];	"thm:pos_neg_or_one"	[color=green,		fillcolor="#A3D6FF",		label=pos_neg_or_one,		shape=ellipse,		style=filled];	"thm:comm_ineq"	[color=green,		fillcolor="#A3D6FF",		label=comm_ineq,		shape=ellipse,		style=filled];	a0000000014	[color=blue,		fillcolor="#A3D6FF",		label=a0000000014,		shape=ellipse,		style=filled];	"def:OrderedSemigroup"	[color=green,		fillcolor="#B0ECA3",		label=OrderedSemigroup,		shape=box,		style=filled];	"def:OrderedCancelSemigroup"	[color=green,		fillcolor="#B0ECA3",		label=OrderedCancelSemigroup,		shape=box,		style=filled];	"def:OrderedSemigroup" -> "def:OrderedCancelSemigroup"	[style=dashed];	"def:LinearOrderedSemigroup"	[color=green,		fillcolor="#B0ECA3",		label=LinearOrderedSemigroup,		shape=box,		style=filled];	"def:OrderedSemigroup" -> "def:LinearOrderedSemigroup"	[style=dashed];	"def:positive"	[color=green,		fillcolor="#B0ECA3",		label=positive,		shape=box,		style=filled];	"def:OrderedSemigroup" -> "def:positive"	[style=dashed];	"def:negative"	[color=green,		fillcolor="#B0ECA3",		label=negative,		shape=box,		style=filled];	"def:OrderedSemigroup" -> "def:negative"	[style=dashed];	"def:one"	[color=green,		fillcolor="#B0ECA3",		label=one,		shape=box,		style=filled];	"def:OrderedSemigroup" -> "def:one"	[style=dashed];	"def:LinearOrderedCancelSemigroup"	[color=green,		fillcolor="#B0ECA3",		label=LinearOrderedCancelSemigroup,		shape=box,		style=filled];	"def:OrderedCancelSemigroup" -> "def:LinearOrderedCancelSemigroup"	[style=dashed];	"def:positive" -> "lem:right_forall"	[style=dashed];	"def:positive" -> "thm:pos_neg_or_one"	[style=dashed];	"def:arch_wrt"	[color=green,		fillcolor="#B0ECA3",		label=arch_wrt,		shape=box,		style=filled];	"def:positive" -> "def:arch_wrt"	[style=dashed];	"thm:neg_lt_pos"	[color=green,		fillcolor="#A3D6FF",		label=neg_lt_pos,		shape=ellipse,		style=filled];	"def:positive" -> "thm:neg_lt_pos"	[style=dashed];	"def:negative" -> "lem:right_forall"	[style=dashed];	"def:negative" -> "thm:pos_neg_or_one"	[style=dashed];	"def:negative" -> "def:arch_wrt"	[style=dashed];	"def:negative" -> "thm:neg_lt_pos"	[style=dashed];	"def:one" -> "lem:right_forall"	[style=dashed];	"def:one" -> "thm:pos_neg_or_one"	[style=dashed];	"def:arch"	[color=green,		fillcolor="#B0ECA3",		label=arch,		shape=box,		style=filled];	"def:one" -> "def:arch"	[style=dashed];	"def:LinearOrderedCancelSemigroup" -> "thm:pos_neg_or_one"	[style=dashed];	"def:arch_wrt" -> "def:arch"	[style=dashed];	"def:arch" -> non_arch_anomalous	[style=dashed];	"def:anomalous_pair"	[color=green,		fillcolor="#B0ECA3",		label=anomalous_pair,		shape=box,		style=filled];	"def:anomalous_pair" -> non_arch_anomalous	[style=dashed];}`)
     .on("end", interactive);
 
 latexLabelEscaper = function(label) {

blueprint/web/index.html

@@ -335,7 +335,7 @@ <h1>Lean declarations</h1>
         </div>
   </div>
   <div class="definition_thmcontent">
-  <p> An element \(a\) of an ordered semigroup \(S\) is <b class="bfseries">positive</b> if for all \(x\in S\), \(a*x \gt x\). </p>
+  <p> An element \(a\) of an ordered semigroup \(S\) is <b class="bfseries">positive</b> if for all \(x\in S\), \(a*x {\gt} x\). </p>
 
   </div>
 </div>
@@ -398,7 +398,7 @@ <h1>Lean declarations</h1>
         </div>
   </div>
   <div class="definition_thmcontent">
-  <p> An element \(a\) of an ordered semigroup \(S\) is <b class="bfseries">negative</b> if for all \(x\in S\), \(a*x \lt x\). </p>
+  <p> An element \(a\) of an ordered semigroup \(S\) is <b class="bfseries">negative</b> if for all \(x\in S\), \(a*x {\lt} x\). </p>
 
   </div>
 </div>
@@ -745,7 +745,7 @@ <h1>Lean declarations</h1>
   </div>
   <div class="lemma_thmcontent">
   <p>Let \(a\) and \(b\) be elements of a semigroup \(S\). </p>
-<p>For all \(n {\gt} 1\), \((a*b)^n = a * (b+a)^(n-1) * b\). </p>
+<p>For all \(n {\gt} 1\), \((a*b)^n = a * (b+a)^{n-1} * b\). </p>
 
   </div>
 </div>
@@ -757,8 +757,8 @@ <h1>Lean declarations</h1>
     <span class="expand-proof">▶</span>
   </div>
   <div class="proof_content">
-  <p>Let \(n=2\). Then \((a+b)^2 = a * (b*a)^(2-1) * b\). </p>
-<p>Assume that the statement holds for \(n\). Then we have that \((a*b)^(n+1) = a * b * (a*b)^n = a * b * a * (b*a)^(n-1) * b = a * (b*a)^n * b\). </p>
+  <p>Let \(n=2\). Then \((a+b)^2 = a * (b*a)^{2-1} * b\). </p>
+<p>Assume that the statement holds for \(n\). Then we have that \((a*b)^{n+1} = a * b * (a*b)^n = a * b * a * (b*a)^{n-1} * b = a * (b*a)^n * b\). </p>
 
   </div>
 </div>
@@ -825,7 +825,7 @@ <h1>Lean declarations</h1>
   <p>If \(n=1\), then we are done. </p>
 <p>Assume that the statement holds for \(n\). Then we have that </p>
 <div class="displaymath" id="a0000000009">
-  \begin{align}  a^(n+1) + b^(n+1) & = a * a^n * b^n * b \\ \text{by the induction hypothesis}\\ & {\lt} a * (a * b)^n * b \\ \text{since $a*b {\lt} b*a$}\\ & {\lt} a * (b * a)^n * b \\ \text{by the previous lemma}\\ & = (a * b)^(n+1) \\ & {\lt} (b * a)^(n+1) \\ \text{by the previous lemma}\\ & = b * (a * b)^n * a \\ & {\lt} b * (b * a)^n * a \\ \text{by the induction hypothesis}\\ & {\lt} b * b^n * a^n * a \\ & = b^(n+1) * a^(n+1) \end{align}
+  \begin{align}  a^{n+1} + b^{n+1} & = a * a^n * b^n * b \\ \text{by the induction hypothesis}\\ & {\lt} a * (a * b)^n * b \\ \text{since $a*b {\lt} b*a$}\\ & {\lt} a * (b * a)^n * b \\ \text{by the previous lemma}\\ & = (a * b)^{n+1} \\ & {\lt} (b * a)^{n+1} \\ \text{by the previous lemma}\\ & = b * (a * b)^n * a \\ & {\lt} b * (b * a)^n * a \\ \text{by the induction hypothesis}\\ & {\lt} b * b^n * a^n * a \\ & = b^{n+1} * a^{n+1} \end{align}
 </div>
 
   </div>
@@ -892,7 +892,7 @@ <h1>Lean declarations</h1>
   </div>
   <div class="definition_thmcontent">
   <p> Let \(a\) and \(b\) be elements of an ordered semigroup \(S\) that are not one. </p>
-<p>Then \(a\) is said to be Archimedean with respect to \(b\) if there exists an \(N\in \mathbb {N}^+\) such that for \(n {\gt} N\), the inequality \(b {\lt} a^n\) holds if \(b\) is positive, and the inequality \(b {\gt} a^n\) holds if \(b\) is negative. </p>
+<p>Then \(a\) is said to be <b class="bfseries">Archimedean with respect to</b> \(b\) if there exists an \(N\in \mathbb {N}^+\) such that for \(n {\gt} N\), the inequality \(b {\lt} a^n\) holds if \(b\) is positive, and the inequality \(b {\gt} a^n\) holds if \(b\) is negative. </p>
 
   </div>
 </div>
@@ -957,7 +957,7 @@ <h1>Lean declarations</h1>
         </div>
   </div>
   <div class="definition_thmcontent">
-  <p> An ordered semigroup is Archimedean if any two of its elements of the same sign are mutually Archimedean. </p>
+  <p> An ordered semigroup is <b class="bfseries">Archimedean</b> if any two of its elements of the same sign are mutually Archimedean. </p>
 
   </div>
 </div>
@@ -1001,9 +1001,9 @@ <h1>Lean declarations</h1>
   </div>
   <div class="definition_thmcontent">
   <p>Let \(a\) and \(b\) be elements of an ordered semigroup \(S\). </p>
-<p>Then \(a\) and \(b\) are said to form an anomalous pair if for all \(n\in \mathbb {N}^+\), one of the following holds </p>
+<p>Then \(a\) and \(b\) are said to form an <b class="bfseries">anomalous pair</b> if for all \(n\in \mathbb {N}^+\), one of the following holds </p>
 <div class="displaymath" id="a0000000010">
-  \begin{align}  a^n {\lt} b^n {\lt} a^(n+1) \\ a^n {\gt} b^n {\gt} a^(n+1) \end{align}
+  \begin{align}  a^n {\lt} b^n {\lt} a^{n+1} \\ a^n {\gt} b^n {\gt} a^{n+1} \end{align}
 </div>
 
   </div>
@@ -1090,7 +1090,7 @@ <h1>Lean declarations</h1>
 </div>
 <p> which means that, since \(a^n {\lt} b\), </p>
 <div class="displaymath" id="a0000000013">
-  \[  b^n {\lt} (a*b)^n {\lt} b^(n+1)  \]
+  \[  b^n {\lt} (a*b)^n {\lt} b^{n+1}  \]
 </div>
 <p> And so \(b\) and \(a*b\) form an anomalous pair. </p>
 <p>The other cases follow similarly. </p>