Update Sun 08 Sep 2024 05:11:03 PM EDT

leanprover-community · Sep 8, 2024 · dfc3e7e · dfc3e7e
1 parent f264b0d
commit dfc3e7e
Show file tree

Hide file tree

Showing 25 changed files with 1,149 additions and 1,098 deletions.
diff --git a/.buildinfo b/.buildinfo
@@ -1,4 +1,4 @@
 # Sphinx build info version 1
 # This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
-config: 803b947a09f3db5a52c6c529e3761a53
+config: 9821478498fa33697c987b601aae688f
 tags: 645f666f9bcd5a90fca523b33c5a78b7
diff --git a/C01_Introduction.html b/C01_Introduction.html
@@ -1,7 +1,8 @@
 <!DOCTYPE html>
 <html class="writer-html5" lang="en" >
 <head>
-  <meta charset="utf-8" />
+  <meta charset="utf-8" /><meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />
+
   <meta name="viewport" content="width=device-width, initial-scale=1.0" />
   <title>1. Introduction &mdash; Mathematics in Lean 0.1 documentation</title>
       <link rel="stylesheet" href="_static/pygments.css" type="text/css" />
@@ -15,6 +16,7 @@
         <script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
         <script src="_static/jquery.js"></script>
         <script src="_static/underscore.js"></script>
+        <script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
         <script src="_static/doctools.js"></script>
     <script src="_static/js/theme.js"></script>
     <link rel="index" title="Index" href="genindex.html" />
@@ -83,10 +85,10 @@
           <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
            <div itemprop="articleBody">
 
-  <div class="section" id="introduction">
-<span id="id1"></span><h1><span class="section-number">1. </span>Introduction<a class="headerlink" href="#introduction" title="Permalink to this headline">&#61633;</a></h1>
-<div class="section" id="getting-started">
-<h2><span class="section-number">1.1. </span>Getting Started<a class="headerlink" href="#getting-started" title="Permalink to this headline">&#61633;</a></h2>
+  <section id="introduction">
+<span id="id1"></span><h1><span class="section-number">1. </span>Introduction<a class="headerlink" href="#introduction" title="Permalink to this heading">&#61633;</a></h1>
+<section id="getting-started">
+<h2><span class="section-number">1.1. </span>Getting Started<a class="headerlink" href="#getting-started" title="Permalink to this heading">&#61633;</a></h2>
 <p>The goal of this book is to teach you to formalize mathematics using the
 Lean 4 interactive proof assistant.
 It assumes that you know some mathematics, but it does not require much.
@@ -171,9 +173,9 @@ <h2><span class="section-number">1.1. </span>Getting Started<a class="headerlink
 the relevant skills, feel free to move on.
 You can always compare your solutions to the ones in the <code class="docutils literal notranslate"><span class="pre">solutions</span></code>
 folder associated with each section.</p>
-</div>
-<div class="section" id="overview">
-<h2><span class="section-number">1.2. </span>Overview<a class="headerlink" href="#overview" title="Permalink to this headline">&#61633;</a></h2>
+</section>
+<section id="overview">
+<h2><span class="section-number">1.2. </span>Overview<a class="headerlink" href="#overview" title="Permalink to this heading">&#61633;</a></h2>
 <p>Put simply, Lean is a tool for building complex expressions in a formal language
 known as <em>dependent type theory</em>.</p>
 <p id="index-0">Every expression has a <em>type</em>, and you can use the <cite>#check</cite> command to
@@ -334,22 +336,34 @@ <h2><span class="section-number">1.2. </span>Overview<a class="headerlink" href=
 Your life may never be the same.</p>
 <p><em>Acknowledgments.</em> We are grateful to Gabriel Ebner for setting up the
 infrastructure for running this tutorial in VS Code,
-and to Scott Morrison and Mario Carneiro for help porting it from Lean 4.
+and to Kim Morrison and Mario Carneiro for help porting it from Lean 4.
 We are also grateful for help and corrections from
-Takeshi Abe, Julian Berman, Alex Best, Thomas Browning,
-Bulwi Cha, Hanson Char, Bryan Gin-ge Chen, Steven Clontz, Mauricio Collaris, Johan Commelin, Mark Czubin,
-Alexandru Duca, Pierpaolo Frasa, Denis Gorbachev, Winston de Greef, Marc Huisinga,
-Mathieu Guay-Paquet, Julian K&#252;lshammer, Victor Liu, Jimmy Lu,
-Martin C. Martin,
-Giovanni Mascellani, John McDowell, Isaiah Mindich, Hunter Monroe, Pietro Monticone,
-Oliver Nash, Emanuelle Natale, Pim Otte,
-Bartosz Piotrowski, Nicolas Rolland, Keith Rush, Yannick Seurin, Guilherme Silva,
-Pedro S&#225;nchez Terraf, Matthew Toohey,
-Floris van Doorn, Eric Wieser, and others.
+Takeshi Abe,
+Julian Berman, Alex Best, Thomas Browning,
+Bulwi Cha, Hanson Char, Bryan Gin-ge Chen, Steven Clontz, Mauricio Collaris, Johan Commelin,
+Mark Czubin,
+Alexandru Duca,
+Pierpaolo Frasa,
+Denis Gorbachev, Winston de Greef, Mathieu Guay-Paquet,
+Marc Huisinga,
+Benjamin Jones,
+Julian K&#252;lshammer,
+Victor Liu, Jimmy Lu,
+Martin C. Martin, Giovanni Mascellani, John McDowell, Isaiah Mindich, Hunter Monroe,
+Pietro Monticone,
+Oliver Nash, Emanuelle Natale,
+Pim Otte,
+Bartosz Piotrowski,
+Nicolas Rolland, Keith Rush,
+Yannick Seurin, Guilherme Silva,
+Pedro S&#225;nchez Terraf, Matthew Toohey, Alistair Tucker,
+Floris van Doorn,
+Eric Wieser,
+and others.
 Our work has been partially supported by the Hoskinson Center for
 Formal Mathematics.</p>
-</div>
-</div>
+</section>
+</section>
 
 
            </div>

diff --git a/C02_Basics.html b/C02_Basics.html
@@ -1,7 +1,8 @@
 <!DOCTYPE html>
 <html class="writer-html5" lang="en" >
 <head>
-  <meta charset="utf-8" />
+  <meta charset="utf-8" /><meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />
+
   <meta name="viewport" content="width=device-width, initial-scale=1.0" />
   <title>2. Basics &mdash; Mathematics in Lean 0.1 documentation</title>
       <link rel="stylesheet" href="_static/pygments.css" type="text/css" />
@@ -15,6 +16,7 @@
         <script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
         <script src="_static/jquery.js"></script>
         <script src="_static/underscore.js"></script>
+        <script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
         <script src="_static/doctools.js"></script>
         <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
     <script src="_static/js/theme.js"></script>
@@ -87,14 +89,14 @@
           <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
            <div itemprop="articleBody">
 
-  <div class="section" id="basics">
-<span id="id1"></span><h1><span class="section-number">2. </span>Basics<a class="headerlink" href="#basics" title="Permalink to this headline">&#61633;</a></h1>
+  <section id="basics">
+<span id="id1"></span><h1><span class="section-number">2. </span>Basics<a class="headerlink" href="#basics" title="Permalink to this heading">&#61633;</a></h1>
 <p>This chapter is designed to introduce you to the nuts and
 bolts of mathematical reasoning in Lean: calculating,
 applying lemmas and theorems,
 and reasoning about generic structures.</p>
-<div class="section" id="calculating">
-<h2><span class="section-number">2.1. </span>Calculating<a class="headerlink" href="#calculating" title="Permalink to this headline">&#61633;</a></h2>
+<section id="calculating">
+<h2><span class="section-number">2.1. </span>Calculating<a class="headerlink" href="#calculating" title="Permalink to this heading">&#61633;</a></h2>
 <p>We generally learn to carry out mathematical calculations
 without thinking of them as proofs.
 But when we justify each step in a calculation,
@@ -383,9 +385,9 @@ <h2><span class="section-number">2.1. </span>Calculating<a class="headerlink" hr
   <span class="n">rw</span> <span class="o">[</span><span class="n">add_mul</span><span class="o">]</span>
 </pre></div>
 </div>
-</div>
-<div class="section" id="proving-identities-in-algebraic-structures">
-<span id="id2"></span><h2><span class="section-number">2.2. </span>Proving Identities in Algebraic Structures<a class="headerlink" href="#proving-identities-in-algebraic-structures" title="Permalink to this headline">&#61633;</a></h2>
+</section>
+<section id="proving-identities-in-algebraic-structures">
+<span id="id2"></span><h2><span class="section-number">2.2. </span>Proving Identities in Algebraic Structures<a class="headerlink" href="#proving-identities-in-algebraic-structures" title="Permalink to this heading">&#61633;</a></h2>
 <p id="index-7">Mathematically, a ring consists of a collection of objects,
 <span class="math notranslate nohighlight">\(R\)</span>, operations <span class="math notranslate nohighlight">\(+\)</span> <span class="math notranslate nohighlight">\(\times\)</span>, and constants <span class="math notranslate nohighlight">\(0\)</span>
 and <span class="math notranslate nohighlight">\(1\)</span>, and an operation <span class="math notranslate nohighlight">\(x \mapsto -x\)</span> such that:</p>
@@ -703,9 +705,9 @@ <h2><span class="section-number">2.1. </span>Calculating<a class="headerlink" hr
 <cite>noncomm_ring</cite> and <cite>ring</cite>. This is partly for historical reasons,
 but also for the convenience of using a shorter name for the
 tactic that deals with commutative rings, since it is used more often.</p>
-</div>
-<div class="section" id="using-theorems-and-lemmas">
-<span id="id3"></span><h2><span class="section-number">2.3. </span>Using Theorems and Lemmas<a class="headerlink" href="#using-theorems-and-lemmas" title="Permalink to this headline">&#61633;</a></h2>
+</section>
+<section id="using-theorems-and-lemmas">
+<span id="id3"></span><h2><span class="section-number">2.3. </span>Using Theorems and Lemmas<a class="headerlink" href="#using-theorems-and-lemmas" title="Permalink to this heading">&#61633;</a></h2>
 <p id="index-16">Rewriting is great for proving equations,
 but what about other sorts of theorems?
 For example, how can we prove an inequality,
@@ -970,9 +972,9 @@ <h2><span class="section-number">2.1. </span>Calculating<a class="headerlink" hr
 </div>
 <p>If you managed to solve this, congratulations!
 You are well on your way to becoming a master formalizer.</p>
-</div>
-<div class="section" id="more-examples-using-apply-and-rw">
-<span id="more-on-order-and-divisibility"></span><h2><span class="section-number">2.4. </span>More examples using apply and rw<a class="headerlink" href="#more-examples-using-apply-and-rw" title="Permalink to this headline">&#61633;</a></h2>
+</section>
+<section id="more-examples-using-apply-and-rw">
+<span id="more-on-order-and-divisibility"></span><h2><span class="section-number">2.4. </span>More examples using apply and rw<a class="headerlink" href="#more-examples-using-apply-and-rw" title="Permalink to this heading">&#61633;</a></h2>
 <p id="index-21">The <code class="docutils literal notranslate"><span class="pre">min</span></code> function on the real numbers is uniquely characterized
 by the following three facts:</p>
 <div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span> <span class="o">(</span><span class="n">min_le_left</span> <span class="n">a</span> <span class="n">b</span> <span class="o">:</span> <span class="n">min</span> <span class="n">a</span> <span class="n">b</span> <span class="bp">&#8804;</span> <span class="n">a</span><span class="o">)</span>
@@ -1171,9 +1173,9 @@ <h2><span class="section-number">2.1. </span>Calculating<a class="headerlink" hr
 the one specifically for the natural numbers.
 You can use <code class="docutils literal notranslate"><span class="pre">_root_.dvd_antisymm</span></code> to specify the generic one;
 either one will work.</p>
-</div>
-<div class="section" id="proving-facts-about-algebraic-structures">
-<span id="id4"></span><h2><span class="section-number">2.5. </span>Proving Facts about Algebraic Structures<a class="headerlink" href="#proving-facts-about-algebraic-structures" title="Permalink to this headline">&#61633;</a></h2>
+</section>
+<section id="proving-facts-about-algebraic-structures">
+<span id="id4"></span><h2><span class="section-number">2.5. </span>Proving Facts about Algebraic Structures<a class="headerlink" href="#proving-facts-about-algebraic-structures" title="Permalink to this heading">&#61633;</a></h2>
 <p id="index-27">In <a class="reference internal" href="#proving-identities-in-algebraic-structures"><span class="std std-numref">Section 2.2</span></a>,
 we saw that many common identities governing the real numbers hold
 in more general classes of algebraic structures,
@@ -1404,8 +1406,8 @@ <h2><span class="section-number">2.1. </span>Calculating<a class="headerlink" hr
 </div>
 <p>We recommend making use of the theorem <code class="docutils literal notranslate"><span class="pre">nonneg_of_mul_nonneg_left</span></code>.
 As you may have guessed, this theorem is called <code class="docutils literal notranslate"><span class="pre">dist_nonneg</span></code> in Mathlib.</p>
-</div>
-</div>
+</section>
+</section>
 
 
            </div>