82156352 - mathematics_in

Authored by: Jeremy Avigad
Authored at: 2023-07-07 14:07:47 -0400
Committed by: Jeremy Avigad
Committed at: 2023-07-07 14:07:47 -0400
Object name: 82156352eb13d868aebeede7e77cada49fc8f990
Parent: 8877f562

Update Fri 07 Jul 2023 02:07:47 PM EDT

Changes

6 changed files (+40/-47)

MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean
- @@ -39,21 +39,16 @@ example : min a b = min b a := by
  example : max a b = max b a := by sorry - example : min (min a b) c = min a (min b c) := by sorry - theorem aux : min a b + c ≤ min (a + c) (b + c) := by sorry - example : min a b + c = min (a + c) (b + c) := by sorry - #check (abs_add : ∀ a b : ℝ, |a + b| ≤ |a| + |b|) example : |a| - |b| ≤ |a - b| := sorry - end section
- @@ -71,21 +66,18 @@ example : x ∣ x ^ 2 := by
  example (h : x ∣ w) : x ∣ y * (x * z) + x ^ 2 + w ^ 2 := by sorry - end section variable (m n : ℕ) - open Nat - #check (gcd_zero_right n : gcd n 0 = n) - #check (gcd_zero_left n : gcd 0 n = n) - #check (lcm_zero_right n : lcm n 0 = 0) - #check (lcm_zero_left n : lcm 0 n = 0) + #check (Nat.gcd_zero_right n : Nat.gcd n 0 = n) + #check (Nat.gcd_zero_left n : Nat.gcd 0 n = n) + #check (Nat.lcm_zero_right n : Nat.lcm n 0 = 0) + #check (Nat.lcm_zero_left n : Nat.lcm 0 n = 0) - example : gcd m n = gcd n m := by + example : Nat.gcd m n = Nat.gcd n m := by sorry - end
MIL/C02_Basics/solutions/Solutions_S04_More_on_Order_and_Divisibility.lean
- @@ -99,19 +99,18 @@ end
  section variable (m n : ℕ) - open Nat - #check (gcd_zero_right n : gcd n 0 = n) - #check (gcd_zero_left n : gcd 0 n = n) - #check (lcm_zero_right n : lcm n 0 = 0) - #check (lcm_zero_left n : lcm 0 n = 0) + #check (Nat.gcd_zero_right n : Nat.gcd n 0 = n) + #check (Nat.gcd_zero_left n : Nat.gcd 0 n = n) + #check (Nat.lcm_zero_right n : Nat.lcm n 0 = 0) + #check (Nat.lcm_zero_left n : Nat.lcm 0 n = 0) - example : gcd m n = gcd n m := by - apply _root_.dvd_antisymm + example : Nat.gcd m n = Nat.gcd n m := by + apply Nat.dvd_antisymm repeat' - apply dvd_gcd - apply gcd_dvd_right - apply gcd_dvd_left + apply Nat.dvd_gcd + apply Nat.gcd_dvd_right + apply Nat.gcd_dvd_left end
html/C01_Introduction.html
- @@ -122,7 +122,7 @@ To get started:
 <li>Install Lean 4 and VS Code following these <a class="reference external" href="https://leanprover-community.github.io/get_started.html#regular-install">instructions</a>. It isn’t enough just to install the Lean 4 extension for VSCode; make sure you complete the steps so that Lean 4 and elan are installed.</li> - <li>Make sure you have <cite>git <https://git-scm.com/>_</cite> installed. + <li>Make sure you have <a class="reference external" href="https://git-scm.com/">git</a> installed. In a terminal, navigate to the folder where you want to put a copy of the repository, and type <code class="docutils literal notranslate">git clone git@github.com:leanprover-community/mathematics_in_lean.git</code> to fetch it from github.</li>
- @@ -135,8 +135,8 @@ not any other folder.</li>
 You can find them in the folder <code class="docutils literal notranslate">MIL</code>, organized by chapter. We strongly recommend making a copy of that folder and experimenting and doing the exercises in that copy. - This leaves the originals intact, and also makes it easier to update the repository as it changes (see below). - You can call the copy <code class="docutils literal notranslate">my_files</code> or whatever you want, and use it to create + This leaves the originals intact, and it also makes it easier to update the repository as it changes (see below). + You can call the copy <code class="docutils literal notranslate">my_files</code> or whatever you want and use it to create your own Lean files as well.</li> </ol> At that point, you can open the textbook in a side panel in VS Code as follows:
html/C02_Basics.html
- @@ -1072,7 +1072,6 @@ whether or not you use these tricks,
 we encourage you to prove the following: <div class="highlight-lean notranslate"><div class="highlight"><pre>example : max a b = max b a := by sorry - example : min (min a b) c = min a (min b c) := by sorry </pre></div>
- @@ -1099,7 +1098,6 @@ but for now we will stick to examples that don’t require the case split.</
 Here is one such example: <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem aux : min a b + c ≤ min (a + c) (b + c) := by sorry - example : min a b + c = min (a + c) (b + c) := by sorry </pre></div>
- @@ -1118,6 +1116,7 @@ in the library’s name for the triangle inequality:
 Use it to prove the following variant: <div class="highlight-lean notranslate"><div class="highlight"><pre>example : |a| - |b| ≤ |a - b| := sorry + end </pre></div> </div> See if you can do this in three lines or less.
- @@ -1150,6 +1149,7 @@ See if you can guess the names of the theorems
 you need to prove the following: <div class="highlight-lean notranslate"><div class="highlight"><pre>example (h : x ∣ w) : x ∣ y * (x * z) + x ^ 2 + w ^ 2 := by sorry + end </pre></div> </div> With respect to divisibility, the greatest common divisor,
- @@ -1158,32 +1158,34 @@ are analogous to <code class="docutils literal notranslate">mi
 Since every number divides <code class="docutils literal notranslate">0</code>, <code class="docutils literal notranslate">0</code> is really the greatest element with respect to divisibility: <div class="highlight-lean notranslate"><div class="highlight"><pre>variable (m n : ℕ) - open Nat - #check (gcd_zero_right n : gcd n 0 = n) - #check (gcd_zero_left n : gcd 0 n = n) - #check (lcm_zero_right n : lcm n 0 = 0) - #check (lcm_zero_left n : lcm 0 n = 0) + #check (Nat.gcd_zero_right n : Nat.gcd n 0 = n) + #check (Nat.gcd_zero_left n : Nat.gcd 0 n = n) + #check (Nat.lcm_zero_right n : Nat.lcm n 0 = 0) + #check (Nat.lcm_zero_left n : Nat.lcm 0 n = 0) </pre></div> </div> - The functions <code class="docutils literal notranslate">gcd</code> and <code class="docutils literal notranslate">lcm</code> for natural numbers are in the - <code class="docutils literal notranslate">Nat</code> namespace, - which means that the full identifiers are <code class="docutils literal notranslate">Nat.gcd</code> and <code class="docutils literal notranslate">Nat.lcm</code>. - Similarly, the names of the theorems listed are prefixed by <code class="docutils literal notranslate">Nat</code>. - The command <code class="docutils literal notranslate">open Nat</code> opens the namespace, - allowing us to use the shorter names. See if you can guess the names of the theorems you will need to prove the following: - <div class="highlight-lean notranslate"><div class="highlight"><pre>example : gcd m n = gcd n m := by + <div class="highlight-lean notranslate"><div class="highlight"><pre>example : Nat.gcd m n = Nat.gcd n m := by sorry + end </pre></div> </div> - Hint: you can use <code class="docutils literal notranslate">dvd_antisymm</code>, but if you do, Lean will - complain that the expression is ambiguous between the generic - theorem and the version <code class="docutils literal notranslate">Nat.dvd_antisymm</code>, - the one specifically for the natural numbers. - You can use <code class="docutils literal notranslate">_root_.dvd_antisymm</code> to specify the generic one; - either one will work. + <dl class="simple"> + <dt>Hint: you can use <code class="docutils literal notranslate">dvd_antisymm</code>, but if you do, Lean will</dt><dd>Hint: you can use <code class="docutils literal notranslate">dvd_antisymm</code>, but if you do, Lean will + </dd> + <dt>complain that the expression is ambiguous between the generic</dt><dd>complain that the expression is ambiguous between the generic + </dd> + <dt>theorem and the version <code class="docutils literal notranslate">Nat.dvd_antisymm</code>,</dt><dd>theorem and the version <code class="docutils literal notranslate">Nat.dvd_antisymm</code>, + </dd> + <dt>the one specifically for the natural numbers.</dt><dd>the one specifically for the natural numbers. + </dd> + <dt>You can use <code class="docutils literal notranslate">_root_.dvd_antisymm</code> to specify the generic one;</dt><dd>You can use <code class="docutils literal notranslate">_root_.dvd_antisymm</code> to specify the generic one; + </dd> + <dt>either one will work.</dt><dd>either one will work. + </dd> + </dl> </section> <section id="proving-facts-about-algebraic-structures"> <h2>2.5. Proving Facts about Algebraic Structures<a class="headerlink" href="#proving-facts-about-algebraic-structures" title="Permalink to this heading"></a></h2>
html/searchindex.js
- @@ -1,1 +1,1 @@
 - Search.setIndex({"docnames": ["C01_Introduction", "C02_Basics", "C03_Logic", "C04_Sets_and_Functions", "C05_Elementary_Number_Theory", "C06_Structures", "C07_Hierarchies", "C08_Topology", "C09_Differential_Calculus", "C10_Integration_and_Measure_Theory", "genindex", "index"], "filenames": ["C01_Introduction.rst", "C02_Basics.rst", "C03_Logic.rst", "C04_Sets_and_Functions.rst", "C05_Elementary_Number_Theory.rst", "C06_Structures.rst", "C07_Hierarchies.rst", "C08_Topology.rst", "C09_Differential_Calculus.rst", "C10_Integration_and_Measure_Theory.rst", "genindex.rst", "index.rst"], "titles": ["1. Introduction", "2. Basics", "3. Logic", "4. Sets and Functions", "5. Elementary Number Theory", "6. Structures", "7. Hierarchies", "8. Topology", "9. Differential Calculus", "10. Integration and Measure Theory", "Index", "Mathematics in Lean"], "terms": {"The": [0, 1, 4, 5, 6, 7, 8, 9, 11], "goal": [0, 1, 2, 3, 4, 5, 7], "thi": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "book": [0, 2, 7], "teach": 0, "you": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "formal": [0, 1, 2, 3, 4, 5, 6, 7, 8], "mathemat": [0, 1, 2, 3, 4, 5, 6, 7], "us": [0, 2, 3, 4, 5, 6, 7, 8, 9, 11], "lean": [0, 1, 2, 3, 4, 5, 6, 7, 8], "4": [0, 1, 2, 4, 5, 7, 8], "interact": [0, 5, 6, 9], "proof": [0, 1, 2, 3, 4, 5, 6, 7, 8], "assist": [0, 2, 5], "It": [0, 1, 2, 3, 4, 5, 6, 7, 8], "assum": [0, 1, 2, 3, 4, 6, 7], "know": [0, 1, 2, 3, 4, 5, 6, 7, 8], "some": [0, 1, 2, 3, 4, 5, 6, 7, 8], "doe": [0, 1, 2, 3, 4, 5, 6, 7, 8], "requir": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "much": [0, 2, 4, 6, 7, 8], "although": [0, 3, 4, 5, 6, 7], "we": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "cover": [0, 1, 3, 6, 7, 8], "exampl": [0, 2, 3, 4, 5, 6, 7, 8, 9, 11], "rang": [0, 2, 3, 4, 7], "from": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "number": [0, 1, 2, 3, 5, 6, 7, 8, 11], "theori": [0, 1, 2, 3, 6, 7, 8, 11], "measur": [0, 5, 7, 8, 11], "analysi": [0, 5, 8], "focu": [0, 1, 7, 9], "elementari": [0, 3, 5, 7, 11], "aspect": [0, 5], "those": [0, 1, 2, 3, 5, 6, 7, 8], "field": [0, 1, 5, 6, 8], "hope": 0, "thei": [0, 1, 2, 3, 4, 5, 6, 7, 8], "ar": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "familiar": [0, 1, 4, 5, 7, 8], "can": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "pick": [0, 6], "them": [0, 1, 2, 3, 4, 5, 6, 7], "up": [0, 2, 3, 4, 5, 6, 7], "go": [0, 1, 2, 3, 4, 6, 7], "also": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "don": [0, 1, 2, 3, 4, 5, 6, 7, 9], "t": [0, 1, 2, 3, 4, 5, 6, 7, 9], "presuppos": 0, "ani": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "background": 0, "method": [0, 2, 3, 4, 5], "seen": [0, 1, 2, 4, 5, 6, 7], "kind": [0, 1, 6, 7], "comput": [0, 3, 4, 5, 8, 9], "program": [0, 1], "write": [0, 1, 2, 4, 5, 6, 7, 8, 9], "definit": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "theorem": [0, 2, 4, 5, 7, 8, 9, 11], "regiment": 0, "languag": [0, 1, 3], "like": [0, 1, 2, 3, 4, 5, 6, 7], "understand": [0, 2, 3, 4, 5, 6, 7], "In": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "return": [0, 2, 3, 4, 5, 7], "provid": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "feedback": 0, "inform": [0, 1, 2, 3, 5, 6, 7], "interpret": [0, 1, 4, 5, 7], "express": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "guarante": [0, 3, 5], "well": [0, 1, 2, 3, 4, 5, 6, 7], "form": [0, 1, 2, 3, 4, 5, 6, 7, 9], "ultim": 0, "certifi": 0, "correct": [0, 1], "our": [0, 1, 2, 3, 4, 5, 6, 7, 9], "learn": [0, 1, 2, 4, 5], "more": [0, 2, 3, 4, 5, 6, 7, 8, 11], "about": [0, 2, 3, 4, 5, 6, 7, 8, 11], "project": [0, 4, 5, 7], "page": [0, 1, 4], "commun": [0, 4], "web": [0, 1, 4], "tutori": 0, "base": [0, 2, 3, 4, 6, 7, 8], "s": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "larg": [0, 6, 7], "ever": [0, 7], "grow": [0, 6], "librari": [0, 1, 2, 3, 4, 5, 7, 8], "mathlib": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "strongli": 0, "recommend": [0, 1, 3], "join": [0, 1, 5], "zulip": [0, 4], "onlin": 0, "chat": 0, "group": [0, 1, 2, 3, 5, 6, 7, 8], "haven": [0, 2, 6, 7], "alreadi": [0, 1, 2, 3, 4, 5, 6, 7], "ll": [0, 2, 4, 6, 7], "find": [0, 1, 2, 4, 5, 6, 7], "live": [0, 5], "welcom": [0, 1], "enthusiast": 0, "happi": 0, "answer": [0, 5, 7], "question": [0, 4, 6, 7, 9], "offer": [0, 2, 5, 7], "moral": [0, 5], "support": [0, 1, 2, 3, 4, 5, 6, 7], "read": [0, 1, 4, 6, 7], "pdf": 0, "html": 0, "version": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "design": [0, 1, 2, 3, 5, 7], "run": 0, "insid": [0, 1, 2, 3], "vs": [0, 1, 2, 3, 5], "code": [0, 1, 2, 3, 5, 6], "editor": [0, 1], "To": [0, 1, 2, 3, 4, 5, 6, 7], "instal": [0, 6], "follow": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "instruct": [0, 1, 7], "isn": [0, 2, 3, 4, 6], "enough": [0, 1, 2, 3, 4, 6, 7], "just": [0, 1, 2, 3, 4, 5, 6, 7], "extens": [0, 1, 6, 7, 8], "vscode": 0, "make": [0, 1, 2, 3, 4, 5, 6, 7, 8], "sure": [0, 1, 2, 3, 5, 6], "complet": [0, 1, 2, 3, 4, 6, 8], "step": [0, 1, 2, 3, 4, 5, 6], "so": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "elan": 0, "have": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "git": 0, "http": [0, 6], "scm": 0, "com": 0, "_": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "termin": 0, "navig": 0, "folder": 0, "where": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "want": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "put": [0, 1, 2, 3, 4, 5, 6, 7], "copi": [0, 3, 4, 6, 7], "repositori": [0, 1], "type": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "clone": 0, "github": [0, 1], "leanprov": 0, "mathematics_in_lean": 0, "fetch": 0, "execut": 0, "lake": 0, "ex": [0, 2], "cach": 0, "compil": 0, "open": [0, 1, 2, 3, 4, 5, 8, 9], "choos": [0, 2, 3, 4, 5, 6, 7], "file": [0, 1, 4, 5, 6, 7], "menu": [0, 1], "Be": [0, 1, 3], "other": [0, 1, 2, 3, 4, 5, 6, 7], "each": [0, 1, 2, 3, 4, 5, 6, 7, 8], "section": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "ha": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "an": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "associ": [0, 1, 2, 4, 5, 6, 7, 9], "exercis": [0, 1, 2, 3, 5, 6, 7, 8], "mil": 0, "organ": 0, "chapter": [0, 1, 2, 3, 4, 5, 6, 7, 8], "experi": [0, 1, 7], "do": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "leav": [0, 1, 2, 3, 5, 6], "origin": [0, 1, 5], "intact": 0, "easier": [0, 1, 3, 4, 6, 7], "updat": 0, "chang": [0, 1, 2, 4, 5, 7, 9], "see": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "below": [0, 2, 3, 4, 5, 6, 7, 8, 9], "call": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "my_fil": 0, "whatev": [0, 2, 4], "creat": [0, 1, 6], "your": [0, 1, 2, 3, 5, 6, 7], "own": [0, 1, 4, 5, 6], "At": [0, 1, 2, 4, 5, 6], "point": [0, 1, 2, 3, 5, 6, 7, 8, 9], "textbook": 0, "side": [0, 1, 2, 3, 4, 5, 6, 7, 8], "panel": 0, "ctrl": [0, 1, 2, 4, 5], "shift": [0, 1, 6, 7], "p": [0, 1, 2, 3, 4, 5, 6, 7, 9], "document": [0, 1, 3, 4, 6], "view": [0, 5, 6, 7], "bar": [0, 1, 2], "appear": [0, 1, 2, 5, 6, 7], "press": 0, "select": [0, 7], "soon": [0, 2, 6, 7], "highlight": 0, "window": [0, 1, 2, 5], "click": [0, 1, 3, 4, 5, 6], "current": [0, 1, 2, 6], "altern": [0, 2, 3, 4, 5, 6, 7], "cloud": 0, "gitpod": 0, "how": [0, 1, 2, 3, 4, 5, 6, 7, 9], "still": [0, 1, 2, 3, 4, 5, 6, 7, 9], "work": [0, 1, 2, 3, 4, 5, 6, 7, 8], "describ": [0, 1, 2, 3, 4, 5, 6, 7], "abov": [0, 1, 2, 3, 4, 5, 6, 7, 9], "progress": [0, 1, 5], "pull": [0, 7], "content": [0, 1, 4, 7], "which": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "why": [0, 2, 4, 6, 7], "suggest": [0, 2, 4, 5, 7], "intend": [0, 1, 2, 5], "while": [0, 1, 2, 6, 7], "contain": [0, 2, 3, 4, 5, 6, 7, 8, 9], "explan": [0, 7], "hint": [0, 1, 2, 9], "text": [0, 3, 5, 7], "often": [0, 1, 2, 3, 4, 5, 6, 7], "includ": [0, 1, 2, 3, 4, 6, 7, 8], "one": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "eval": 0, "hello": 0, "world": 0, "should": [0, 1, 2, 3, 4, 5, 6, 7, 8], "abl": [0, 1, 2, 3, 4, 5, 6, 8], "correspond": [0, 1, 2, 3, 4, 5, 6, 7, 8], "If": [0, 1, 2, 3, 4, 5, 6, 7], "line": [0, 1, 2, 3, 4, 6], "show": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "hover": [0, 1, 2, 3, 4, 5], "cursor": [0, 1, 2], "over": [0, 1, 2, 3, 4, 5, 6, 7, 8], "command": [0, 1, 2, 3, 4, 5, 6], "respons": [0, 1], "pop": 0, "encourag": [0, 1, 2, 3, 4, 5], "edit": 0, "try": [0, 1, 2, 3, 4, 5, 6, 7], "moreov": [0, 1, 4, 5, 7], "lot": [0, 3, 5, 6, 7], "challeng": [0, 1, 2, 3, 5, 8], "rush": 0, "past": [0, 1], "through": [0, 1, 3, 4, 5, 6, 7], "central": [0, 4], "all": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "when": [0, 1, 2, 3, 4, 5, 6, 7, 8], "feel": [0, 1, 2, 6, 7], "comfort": [0, 2], "master": [0, 1, 4], "relev": [0, 1, 2, 4, 5, 6, 7], "skill": [0, 1, 2, 3, 4], "free": [0, 1, 7], "move": [0, 1, 2, 6, 7], "alwai": [0, 1, 2, 3, 5, 6], "compar": [0, 5, 6, 7], "solut": [0, 1, 4, 6], "ones": [0, 1, 2, 3, 5, 9], "simpli": [0, 1, 2, 3, 4, 5, 6, 7], "tool": [0, 1, 2, 5, 6], "build": [0, 2, 4, 6, 7, 11], "complex": [0, 1, 2, 4, 5, 8, 9], "known": [0, 1, 2, 3, 4, 5, 6, 7, 8], "depend": [0, 2, 3, 4, 5, 6, 7], "everi": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "check": [0, 1, 2, 3, 4, 5, 6, 7], "print": [0, 3, 4, 5, 9], "\u2115": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "These": [0, 1, 2, 3, 4, 5, 8, 9], "object": [0, 1, 2, 3, 4, 5, 11], "2": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "def": [0, 2, 3, 4, 5, 6, 7], "f": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "x": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "3": [0, 1, 2, 3, 4, 5, 6, 7], "prop": [0, 2, 3, 4, 5, 6, 7, 9], "statement": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "fermatlasttheorem": 0, "y": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "z": [0, 1, 2, 5, 6, 7, 8, 9], "n": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "0": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "itself": [0, 2, 3, 5, 6, 7, 8], "Such": [0, 1, 2, 6], "proposit": [0, 2, 3, 4, 5], "easi": [0, 4, 5, 6, 7], "rfl": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "hard": [0, 1, 3, 5, 6], "sorri": [0, 1, 2, 3, 4, 5, 6, 7, 8], "manag": [0, 1, 4, 5, 7], "construct": [0, 2, 3, 4, 5, 6, 7], "accept": [0, 1, 2, 7], "term": [0, 1, 2, 3, 4, 5, 7], "done": [0, 2, 3, 4, 6, 7], "someth": [0, 1, 2, 4, 6, 7], "veri": [0, 2, 4, 6, 7, 9], "impress": 0, "cheat": [0, 1], "now": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "game": [0, 6], "left": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "rule": [0, 2, 4, 5, 6, 7], "complementari": 0, "companion": [0, 1], "prove": [0, 2, 3, 4, 5, 6, 7, 8, 9, 11], "thorough": 0, "underli": [0, 1, 5, 6], "logic": [0, 1, 3, 4, 5, 11], "framework": 0, "core": [0, 4, 5], "syntax": [0, 1, 4, 6], "peopl": [0, 1], "who": [0, 7], "prefer": [0, 1, 3], "user": [0, 2, 6], "manual": [0, 3, 4], "befor": [0, 1, 2, 3, 4, 5, 6], "new": [0, 1, 2, 3, 4, 5, 6, 7], "dishwash": 0, "person": 0, "hit": [0, 1], "button": 0, "figur": [0, 1, 2, 5], "out": [0, 1, 2, 3, 4, 5, 6, 7], "activ": 0, "potscrubb": 0, "featur": [0, 2, 4], "later": [0, 1, 2, 4, 5, 6, 7], "sens": [0, 2, 3, 4, 5, 6, 7, 8], "here": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "refer": [0, 1, 2, 4, 5, 6, 7, 8], "back": [0, 1, 2, 3, 5, 6, 7], "necessari": [0, 2, 4, 5], "anoth": [0, 1, 2, 3, 4, 5, 6, 7], "thing": [0, 1, 2, 3, 4, 5, 6, 7], "distinguish": [0, 5, 6, 7, 8], "place": [0, 1, 2, 5, 7], "greater": [0, 1, 2, 3, 4, 7], "emphasi": [0, 6], "tactic": [0, 1, 2, 3, 4, 5, 6, 7, 8], "given": [0, 1, 2, 3, 4, 5, 6, 7], "two": [0, 1, 2, 3, 4, 5, 6, 7, 9], "wai": [0, 1, 2, 3, 4, 5, 6, 7, 9], "down": [0, 3, 4, 6, 7], "themselv": [0, 4, 5], "suitabl": [0, 1, 2, 5, 7], "descript": [0, 1, 2, 4, 7], "thereof": 0, "For": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "repres": [0, 1, 2, 3, 4, 5, 6, 8], "fact": [0, 2, 3, 4, 5, 6, 7, 8, 9, 11], "even": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "m": [0, 1, 2, 4, 6, 7, 8], "nat": [0, 1, 2, 3, 4, 5, 7], "fun": [0, 2, 3, 4, 5, 6, 7, 8, 9], "k": [0, 2, 4, 5, 7, 8], "hk": [0, 8], "hmn": 0, "rw": [0, 2, 3, 4, 5, 6, 7, 11], "mul_add": [0, 1, 4, 6], "l": [0, 1, 8, 9], "compress": [0, 1, 7], "singl": [0, 1, 2, 3, 4, 5, 6, 8], "instead": [0, 1, 2, 3, 4, 5, 6, 7], "style": [0, 1], "same": [0, 1, 2, 3, 4, 5, 6, 7], "comment": [0, 4], "henc": [0, 2, 3, 4, 5, 6, 7, 8], "ignor": [0, 7], "sai": [0, 1, 2, 3, 4, 5, 6, 7, 9], "natur": [0, 1, 2, 3, 4, 5, 6, 7, 8], "rintro": [0, 2, 3, 4, 5, 7], "need": [0, 1, 2, 3, 4, 5, 6, 7], "twice": [0, 1, 7], "let": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "substitut": [0, 2], "obviou": [0, 4, 5, 6], "ring": [0, 1, 2, 3, 4, 5, 6], "As": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "enter": [0, 1, 2, 3, 7], "displai": [0, 1, 2, 6], "state": [0, 1, 2, 3, 4, 6, 7, 8], "separ": [0, 1, 2, 4, 5], "tell": [0, 2, 3, 4, 5, 6], "what": [0, 1, 2, 3, 4, 5, 6, 7], "establish": [0, 1, 2, 3, 4, 5], "task": [0, 2, 4, 5, 6, 7], "remain": [0, 1, 2, 3, 5, 6, 7], "replai": 0, "sinc": [0, 1, 2, 3, 4, 5, 6, 7], "continu": [0, 1, 4, 5, 6, 9], "first": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "introduc": [0, 1, 2, 3, 4, 7, 9], "could": [0, 1, 2, 4, 5, 6, 7], "renam": 0, "decompos": [0, 3, 5], "hypothesi": [0, 1, 2, 3, 4], "assumpt": [0, 1, 2, 3, 4, 5, 7, 8, 9], "second": [0, 1, 2, 3, 4, 5, 6, 7, 9], "declar": [0, 1, 4, 5, 6], "next": [0, 1, 2, 3, 4, 5, 6, 7, 8], "rewrit": [0, 1, 2, 3, 4, 5, 6, 7], "replac": [0, 1, 2, 3, 4, 6], "solv": [0, 1, 2, 3, 4, 5, 6, 7], "result": [0, 1, 2, 3, 4, 5, 6, 7], "abil": 0, "small": [0, 4, 5, 7], "increment": [0, 1], "extrem": [0, 6, 7], "power": [0, 1, 2, 3, 4, 5, 6], "reason": [0, 1, 2, 4, 5, 6, 7], "quicker": 0, "than": [0, 1, 2, 3, 4, 5, 6, 7, 8], "There": [0, 1, 2, 3, 4, 6, 7, 8, 9], "sharp": 0, "distinct": [0, 2, 3, 4, 5, 7], "between": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "insert": [0, 2, 4, 5, 7, 8], "did": [0, 2, 6, 7], "phrase": [0, 1, 2, 4, 5], "mul_left_comm": [0, 4], "convers": [0, 2, 4, 7], "short": [0, 1, 2, 3, 4, 5], "middl": [0, 1, 2, 7], "That": [0, 4, 5, 6], "said": [0, 2, 4, 5], "reduc": [0, 2, 3, 4, 5], "liner": 0, "carri": [0, 1, 2, 3, 4, 5, 6, 7, 9], "But": [0, 1, 2, 3, 4, 5, 6, 7], "substanti": 0, "autom": [0, 1, 5], "justifi": [0, 1, 2, 7], "longer": [0, 4, 5], "calcul": [0, 2, 4, 5, 11], "bigger": [0, 3, 8], "inferenti": 0, "invok": [0, 1, 7], "simplifi": [0, 2, 3, 4, 5, 7, 9], "specif": [0, 1, 3, 4, 5, 6], "pariti": [0, 4], "automat": [0, 1, 2, 3, 4, 5, 6, 7, 8], "intro": [0, 1, 2, 3, 4, 5, 6, 7], "simp": [0, 2, 3, 4, 5, 6, 7, 8], "parity_simp": 0, "big": [0, 5, 7, 8], "differ": [0, 1, 2, 3, 4, 5, 6, 7, 8], "onli": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "its": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "built": [0, 2, 6], "wherea": [0, 1, 3, 5, 7], "top": [0, 6, 7, 8], "meant": [0, 2, 6], "rather": [0, 1, 2, 4, 5, 6, 7], "think": [0, 1, 2, 3, 4, 5, 6, 7, 8], "basic": [0, 2, 4, 5, 7, 9, 11], "entri": [0, 5], "brows": [0, 1, 4], "frustrat": [0, 6], "curv": 0, "steep": 0, "newcom": 0, "avail": [0, 1, 4, 5, 6], "round": [0, 1, 5], "clock": 0, "doubt": 0, "too": [0, 1, 3, 5, 6, 7], "contribut": [0, 3], "develop": [0, 1, 4, 9], "mission": 0, "dive": 0, "come": [0, 1, 2, 3, 4, 5, 6, 7], "forewarn": 0, "fundament": [0, 4, 5, 6, 9], "life": [0, 2], "mai": [0, 1, 2, 3, 5, 6, 7, 8], "never": [0, 6], "acknowledg": 0, "grate": [0, 5], "gabriel": 0, "ebner": 0, "set": [0, 1, 2, 4, 5, 6, 8, 9, 11], "infrastructur": 0, "scott": 0, "morrison": 0, "mario": 0, "carneiro": 0, "help": [0, 1, 2, 3, 4, 5, 6, 7], "port": 0, "julian": 0, "berman": 0, "alex": 0, "best": 0, "bulwi": 0, "cha": 0, "bryan": 0, "gin": 0, "ge": [0, 2, 5], "chen": 0, "johan": 0, "commelin": 0, "mathieu": 0, "guai": 0, "paquet": 0, "k\u00fclshammer": 0, "giovanni": 0, "mascellani": 0, "hunter": 0, "monro": 0, "pietro": 0, "monticon": 0, "oliv": 0, "nash": 0, "bartosz": 0, "piotrowski": 0, "guilherm": 0, "silva": 0, "been": [0, 1, 2, 4, 5, 6, 8], "partial": [0, 1, 2, 3, 5, 6], "hoskinson": 0, "center": [0, 7], "nut": 1, "bolt": 1, "gener": [1, 2, 3, 4, 5, 6, 7, 8, 9], "without": [1, 2, 4, 5, 6, 7, 8], "net": 1, "hand": [1, 2, 3, 4, 5, 6, 7], "equal": [1, 2, 3, 4, 5, 6, 7, 9], "right": [1, 2, 3, 4, 5, 6, 7, 8], "tantamount": [1, 3], "name": [1, 2, 3, 4, 5, 6, 7, 8], "b": [1, 2, 3, 4, 5, 6, 7, 8, 9], "c": [1, 2, 4, 5, 6, 7, 8, 9], "real": [1, 2, 3, 4, 5, 6, 7, 8, 9], "mul_assoc": [1, 2, 4, 5, 6], "mul_comm": [1, 2, 4, 5, 6], "elimin": 1, "explicitli": [1, 2, 3, 5, 6, 7, 8], "purpos": [1, 2, 3, 4, 5, 6, 7], "illustr": [1, 2, 3, 4, 5], "multipl": [1, 2, 3, 4, 5, 6, 8], "written": [1, 2, 3, 4, 5, 6, 7, 8], "howev": [1, 2, 5, 6, 7, 8], "good": [1, 2, 3, 4, 5, 6, 7], "mind": [1, 2, 5, 6], "notat": [1, 2, 3, 4, 5, 6, 7, 8, 9], "convent": [1, 5, 9], "parenthes": [1, 2, 3, 4], "import": [1, 2, 3, 4, 5, 6, 7, 9], "data": [1, 2, 4, 5, 6, 7], "\u211d": [1, 2, 3, 5, 6, 7, 8, 9], "begin": [1, 2, 3, 4, 5, 6], "sake": [1, 4], "breviti": [1, 5], "suppress": 1, "repeat": [1, 4, 5, 6], "happen": [1, 6, 7], "charact": [1, 3, 6], "r": [1, 2, 4, 5, 6, 7], "symbol": [1, 2, 5, 6], "doesn": [1, 2, 7], "until": [1, 2, 4, 5, 6, 7], "space": [1, 2, 3, 5, 6, 9, 11], "tab": [1, 3, 4], "kei": [1, 4, 5, 7], "curiou": [1, 6], "abbrevi": [1, 2, 3, 5], "get": [1, 2, 3, 4, 6, 7, 8, 11], "access": [1, 3, 5, 6, 7, 9], "keyboard": 1, "easili": [1, 4, 5, 6], "backslash": [1, 3], "lead": [1, 2, 4, 5, 6, 7], "lean4": 1, "input": [1, 3, 7], "leader": 1, "report": 1, "infoview": 1, "A": [1, 2, 3, 4, 5, 6, 7, 8], "typic": 1, "might": [1, 2, 3, 4, 5], "look": [1, 2, 3, 4, 6, 7], "1": [1, 2, 3, 4, 5, 6, 7, 8, 9], "h\u2081": [1, 2, 3, 4], "prime": [1, 2, 3, 5, 6, 11], "h\u2082": [1, 3, 4], "h\u2083": [1, 3], "denot": [1, 3, 4, 6, 7], "context": [1, 2, 4, 5, 6, 7, 8, 9], "plai": [1, 3, 4, 6, 7], "three": [1, 2, 4, 5, 7], "label": [1, 2], "everyth": [1, 2, 6, 7], "identifi": [1, 2, 4], "subscript": 1, "h": [1, 2, 3, 4, 5, 6, 7, 8, 9], "legal": 1, "would": [1, 2, 3, 4, 5, 6, 7, 8], "h1": [1, 3, 4, 5], "h2": [1, 3, 5], "h3": 1, "foo": [1, 3, 5], "baz": 1, "last": [1, 2, 3, 4, 5, 6, 7], "sometim": [1, 2, 3, 4, 5, 6, 7], "target": [1, 6, 7, 9], "combin": [1, 2, 5, 6, 7], "practic": [1, 2, 3, 6, 7], "mean": [1, 2, 3, 4, 5, 6, 7, 8, 9], "usual": [1, 2, 3, 4, 5, 7, 9], "clear": [1, 2, 4, 5, 6], "case": [1, 2, 3, 4, 5, 6, 7, 9], "With": [1, 3, 4, 6, 7], "arrow": [1, 2, 6, 7], "revers": [1, 2, 3, 5, 7], "note": [1, 2, 4, 5, 6, 7, 9], "noth": [1, 2, 3, 4, 5, 6], "argument": [1, 2, 3, 4, 5, 6, 7], "tri": [1, 2, 4, 6], "match": [1, 2, 5], "pattern": [1, 2, 3, 5, 6], "local": [1, 2, 6, 7, 8], "d": [1, 2, 4, 5, 8], "e": [1, 2, 3, 4, 5, 6, 7, 8, 9], "sub_self": [1, 2], "hyp": 1, "list": [1, 2, 3, 4, 5], "comma": 1, "squar": [1, 2, 4, 5, 6], "bracket": [1, 2, 5, 6], "after": [1, 2, 4, 6, 7, 8], "trick": [1, 2, 4, 6, 8], "variabl": [1, 2, 3, 4, 5, 6, 7, 8, 9], "onc": [1, 2, 3, 4, 5, 6, 7, 9], "outsid": [1, 4], "inspect": 1, "reveal": 1, "inde": [1, 5, 6, 7, 8], "delimit": 1, "scope": [1, 2, 3, 5], "end": [1, 2, 3, 4, 5, 6, 7, 8], "block": [1, 4], "final": [1, 2, 3, 5, 7, 9], "recal": [1, 2, 4, 5, 7, 9], "introduct": [1, 2, 7, 11], "determin": [1, 5, 7], "both": [1, 2, 3, 4, 5, 6, 7, 8], "expect": [1, 2, 3, 4, 5, 6, 7], "rais": [1, 4], "error": [1, 2, 3, 6], "explain": [1, 2, 3, 4, 5, 6, 7, 9], "output": 1, "meanwhil": [1, 4], "take": [1, 2, 3, 4, 5, 6, 7, 8, 9], "two_mul": 1, "add_mul": [1, 6], "distribut": [1, 4, 5, 6], "addit": [1, 2, 4, 5, 6, 7, 8, 9], "add_assoc": [1, 4, 5, 6], "precis": [1, 3, 7, 8], "possibl": [1, 2, 3, 4, 5, 7], "calc": [1, 2, 3, 5, 7], "keyword": [1, 2, 4, 5], "notic": [1, 2, 3, 4, 5, 7], "finicki": 1, "underscor": [1, 2, 3], "justif": [1, 2], "format": 1, "indic": [1, 2, 3, 5, 6], "indent": 1, "One": [1, 2, 3, 4, 5, 6, 7], "outlin": [1, 2, 4, 7], "modulo": [1, 4, 5], "individu": 1, "pure": [1, 7], "littl": [1, 2, 7, 8], "underneath": [1, 3], "pow_two": [1, 4], "mul_sub": 1, "add_sub": 1, "sub_sub": 1, "add_zero": [1, 5, 6], "perform": [1, 2, 3], "exact": [1, 2, 3, 4, 5, 7], "becaus": [1, 2, 3, 4, 5, 6, 7, 8], "exactli": [1, 2, 3, 5, 6, 7], "close": [1, 2, 3, 6, 8, 9], "bit": [1, 2, 4, 6, 7], "commut": [1, 2, 3, 4, 5, 6, 8], "long": [1, 2, 3, 5, 6, 8], "axiom": [1, 2, 3, 5, 6, 7, 9], "indirectli": 1, "similar": [1, 2, 3, 5, 6, 7], "common": [1, 2, 3, 4, 5, 7], "variat": [1, 3, 4, 5, 7, 8], "nth_rewrit": 1, "allow": [1, 2, 3, 4, 5, 6, 7, 8, 9], "particular": [1, 2, 5, 6, 7], "instanc": [1, 2, 3, 4, 5, 6, 7, 8], "enumer": [1, 2], "start": [1, 2, 3, 4, 6, 7, 8, 9, 11], "occurr": 1, "nth_rw": 1, "consist": [1, 3, 5, 6, 7, 8], "collect": [1, 2, 3, 5, 7, 9], "oper": [1, 2, 3, 4, 5, 6, 7, 8], "time": [1, 4, 5, 6, 7, 8, 9], "constant": [1, 2, 9], "mapsto": [1, 5], "abelian": [1, 5, 6], "negat": [1, 5, 11], "invers": [1, 3, 5, 6, 8, 9], "add_comm": [1, 4, 5, 6], "zero_add": [1, 4, 5, 6], "add_left_neg": [1, 5], "mul_on": [1, 5, 6], "one_mul": [1, 2, 5, 6], "being": [1, 3, 5, 7, 8], "suffic": [1, 2, 3, 7], "give": [1, 2, 3, 4, 6, 7, 9], "element": [1, 2, 3, 4, 5, 6, 7, 8, 9], "concret": [1, 2, 4, 5, 6, 7], "integ": [1, 2, 4, 6, 11], "abstract": [1, 2, 5, 6, 7], "character": [1, 3, 4, 7, 8], "axiomat": [1, 2, 3, 5], "train": [1, 6], "recogn": [1, 2, 4, 5, 6, 7], "appropri": [1, 2, 3, 5, 6], "\u2124": [1, 4, 5, 6], "ration": [1, 2, 4, 7], "\u211a": [1, 4, 7], "\u2102": [1, 5, 8], "extend": [1, 3, 4, 5, 6, 7, 9], "order": [1, 2, 3, 4, 5, 6, 7, 8], "Not": [1, 5, 7], "properti": [1, 2, 3, 4, 5, 6, 7, 8, 9], "hold": [1, 2, 3, 4, 5, 7, 9], "arbitrari": [1, 2, 3, 4, 5], "taken": [1, 2], "cours": [1, 2, 4, 6, 7, 8, 9], "linear": [1, 2, 5, 7], "matric": [1, 5], "fail": [1, 2, 3, 4, 5, 6, 7, 9], "commr": [1, 2, 5], "unchang": [1, 2], "linarith": [1, 2, 4, 5], "permiss": 1, "strike": [1, 2], "balanc": 1, "concis": [1, 5], "readabl": [1, 2, 3, 4, 7], "strengthen": [1, 2, 4], "deriv": [1, 2, 4, 8, 9], "most": [1, 2, 3, 4, 5, 6, 7, 9], "organiz": 1, "mechan": [1, 2, 5], "namespac": [1, 2, 3, 4, 5, 7], "full": [1, 3, 4, 5, 6, 7], "shorter": [1, 3, 4, 7], "avoid": [1, 3, 4, 5, 6, 8], "due": [1, 3, 6], "clash": 1, "myre": 1, "add_right_neg": 1, "effect": [1, 3, 6, 7], "temporarili": [1, 2], "reprov": 1, "care": [1, 2, 3, 5], "earlier": 1, "pai": [1, 2, 6, 7], "attent": [1, 2, 4, 6, 7], "curli": [1, 2], "implicit": [1, 2, 5, 6, 7, 8], "moment": [1, 2, 5], "worri": [1, 3, 4, 5], "neg_add_cancel_left": 1, "add_neg_cancel_right": 1, "add_left_cancel": 1, "add_right_cancel": 1, "plan": [1, 6, 7], "brace": 1, "imagin": 1, "situat": [1, 3, 6, 7], "draw": [1, 5, 6], "conclus": [1, 2, 4], "hypothes": [1, 2, 3, 4, 5], "redund": [1, 5, 7, 9], "few": [1, 2, 3, 4, 7], "extra": [1, 2, 3, 5, 6, 7], "oner": 1, "complic": [1, 2, 6], "tediou": [1, 2, 6], "mark": [1, 2, 6, 7], "suppos": [1, 2, 3, 4, 5, 7], "infer": [1, 2, 3, 5, 6], "mul_zero": [1, 5, 6], "serv": [1, 3, 4, 5, 9], "therefor": [1, 4, 5, 7], "promot": 1, "modular": 1, "subproof": 1, "wa": [1, 3], "except": [1, 5], "ad": [1, 2, 3, 4, 5, 6, 7], "variant": [1, 2, 7], "whose": [1, 2, 4, 5, 6, 7, 8], "necessarili": [1, 9], "miss": [1, 3, 4], "piec": [1, 4, 5, 6, 7], "either": [1, 2, 3, 5, 6, 7], "becom": [1, 4, 5, 6, 7], "technic": [1, 5, 6], "strictli": [1, 2, 8], "less": [1, 2, 3, 4, 5, 6, 7], "script": 1, "slightli": [1, 6, 7, 8], "clearer": [1, 3, 5], "human": 1, "reader": [1, 7], "maintain": 1, "evolv": 1, "rememb": [1, 2, 3, 4, 5, 6, 7], "zero_mul": [1, 4, 5, 6], "By": [1, 3, 5, 6], "neg_eq_of_add_eq_zero": 1, "eq_neg_of_add_eq_zero": 1, "neg_zero": 1, "neg_neg": 1, "had": [1, 6], "annot": [1, 3, 4, 5, 6], "third": [1, 2, 3, 5, 7], "specifi": [1, 2, 3, 4, 5, 7, 8, 9], "imposs": 1, "default": [1, 2, 3, 4, 5, 6, 8], "subtract": [1, 4, 5], "provabl": [1, 3, 6, 7], "sub_eq_add_neg": 1, "On": [1, 2, 3, 5, 6, 7, 9], "defin": [1, 2, 3, 4, 6, 7, 8, 9, 11], "reflex": [1, 2], "present": [1, 2, 4, 7], "forc": [1, 2, 3], "unfold": [1, 2, 3, 4, 5, 7], "deal": [1, 2, 3, 4, 5, 7], "equat": [1, 2, 3, 4, 5], "interchang": 1, "self_sub": 1, "effort": [1, 4], "one_add_one_eq_two": 1, "norm_num": [1, 2, 4, 5], "strength": 1, "weaker": [1, 2], "notion": [1, 2, 3, 4, 5, 7, 8, 9], "addgroup": [1, 5], "otherwis": [1, 2, 3, 4, 5], "addcommgroup": 1, "commgroup": 1, "g": [1, 2, 3, 5, 6, 7, 8, 9], "mul_left_inv": [1, 5], "\u00b9": [1, 3, 5, 6, 7], "cocki": 1, "helper": 1, "along": [1, 4, 7], "mul_right_inv": [1, 5], "mul_inv_rev": 1, "non": [1, 3, 6, 7, 8, 9], "abel": 1, "noncomm_r": 1, "seem": [1, 2, 4, 6, 7, 8], "odd": [1, 2, 3, 4], "partli": [1, 6], "histor": 1, "conveni": [1, 2, 3, 5, 6, 7], "great": [1, 5], "sort": [1, 3, 4], "inequ": [1, 2, 6, 7], "le": [1, 5, 6], "whenev": [1, 2, 4, 5], "consid": [1, 2, 3, 4, 5, 6, 7, 8, 9], "le_refl": [1, 2], "le_tran": [1, 2], "detail": [1, 2, 3, 4, 5, 6], "unless": [1, 2, 5], "realli": [1, 2, 3, 4, 6, 7], "insist": [1, 6], "discuss": [1, 2, 4, 5, 6, 7, 8], "implic": [1, 7, 11], "h\u2080": [1, 2, 3, 4, 7], "dot": [1, 7], "option": [1, 2, 4, 5, 6, 7], "within": [1, 2, 7], "visibl": 1, "must": [1, 5, 6, 7], "decreas": [1, 5], "fourth": [1, 2], "mode": [1, 2, 5], "entir": [1, 3, 5, 7, 8], "lt_of_le_of_lt": [1, 2], "lt_of_lt_of_l": 1, "lt_tran": [1, 2], "togeth": [1, 2, 3, 4, 5, 7], "handl": [1, 3, 4, 6], "arithmet": 1, "5": [1, 2, 5, 7, 8], "pass": [1, 5], "exp_le_exp": 1, "mpr": [1, 2, 5, 7], "exp": [1, 3], "applic": [1, 2, 4, 5, 9], "function": [1, 2, 4, 5, 6, 8, 9, 11], "compound": [1, 2, 7], "pars": [1, 3], "exp_lt_exp": 1, "log_le_log": 1, "log": [1, 3, 9], "log_lt_log": 1, "add_le_add": [1, 2], "add_le_add_left": 1, "add_le_add_right": 1, "add_lt_add_of_le_of_lt": 1, "add_lt_add_of_lt_of_l": 1, "add_lt_add_left": 1, "add_lt_add_right": 1, "add_nonneg": [1, 5], "add_po": 1, "add_pos_of_pos_of_nonneg": 1, "exp_po": [1, 3], "bi": [1, 5, 11], "lr": 1, "iff": [1, 3, 7, 8, 9], "connect": [1, 3, 5, 7], "equival": [1, 2, 3, 4, 5, 7, 8, 9], "mp": [1, 2, 3, 4, 7], "forward": [1, 2, 5, 7], "direct": [1, 2, 3, 6, 7, 8], "stand": [1, 2, 5, 7, 8], "modu": 1, "ponen": 1, "respect": [1, 2, 3, 4, 5, 7], "thu": [1, 3, 4, 5, 7], "again": [1, 2, 3, 4, 5, 6, 7], "numer": [1, 4, 5], "constitut": 1, "part": [1, 2, 3, 4, 5, 6, 7, 9], "strategi": [1, 2, 4], "api": 1, "reli": [1, 2, 3, 5, 7], "guess": [1, 2, 3, 4, 5], "cmd": [1, 2], "mac": [1, 2], "a_of_b_of_c": 1, "approxim": 1, "loud": 1, "probabl": [1, 5, 6, 7], "add_l": 1, "choic": [1, 2, 3, 5, 7], "exist": [1, 2, 3, 6, 7], "jump": [1, 4, 5, 7], "nearbi": [1, 4], "sq_nonneg": 1, "delet": [1, 2, 3, 4], "uncom": 1, "previou": [1, 2, 3, 5, 6, 7, 8, 9], "confirm": [1, 2, 3, 4], "finish": [1, 2, 3, 4], "job": 1, "pow_two_nonneg": [1, 2], "tend": [1, 7], "around": [1, 3, 6, 7, 9], "binari": [1, 2, 4, 5, 6], "increas": 1, "worth": [1, 2, 5], "definition": [1, 4, 5, 6, 7], "principl": [1, 2, 3, 4, 6, 8], "favor": [1, 2, 5], "timesav": 1, "clever": 1, "involv": [1, 2, 4, 5, 6, 7], "nice": [1, 2, 4, 6, 7], "idea": [1, 2, 3, 5, 6, 7], "abs_l": [1, 5], "congratul": [1, 2, 4], "min": [1, 2, 7, 9], "uniqu": [1, 2, 3, 4, 5, 7], "min_le_left": 1, "min_le_right": 1, "le_min": 1, "max": [1, 2, 6, 7, 9], "pair": [1, 2, 4, 5, 7], "act": 1, "curri": 1, "logician": 1, "haskel": 1, "bind": [1, 3], "tighter": [1, 3], "infix": [1, 6], "le_antisymm": [1, 2], "usag": 1, "inconsist": 1, "outer": 1, "level": [1, 2, 6], "nest": [1, 2], "bother": [1, 3], "repetit": [1, 6], "foreshadow": 1, "univers": [1, 3, 5, 7, 11], "quantifi": [1, 3, 4, 5, 7, 11], "desir": [1, 3, 6, 7], "implicitli": [1, 2], "mani": [1, 2, 3, 5, 6, 7, 8, 9, 11], "whether": [1, 2, 3, 4, 6, 7], "Of": [1, 2, 4, 6, 7, 8, 9], "interest": [1, 2, 3, 5, 6, 7], "vice": [1, 3], "versa": [1, 3], "word": [1, 2, 3, 4, 5, 7], "switch": [1, 6], "transit": [1, 2, 5, 7], "total": 1, "satisfi": [1, 3, 4, 5, 6, 7, 8], "disjunct": [1, 3, 11], "stick": [1, 2, 7, 8], "split": [1, 2, 3, 4], "aux": [1, 2, 4, 7], "valu": [1, 2, 3, 4, 5, 6, 7, 8, 9], "yield": [1, 2, 3, 4, 5, 7], "made": [1, 2, 3, 5, 7], "manifest": [1, 7], "triangl": [1, 2, 5], "abs_add": [1, 2], "sub_add_cancel": [1, 5], "relat": [1, 2, 3, 5, 6, 7, 8, 9], "divis": [1, 2, 4, 5, 6], "ordinari": [1, 2, 4, 5, 7], "unicod": [1, 3, 6], "obtain": [1, 2, 4, 5, 7, 8], "dvd": 1, "dvd_tran": 1, "dvd_mul_of_dvd_left": 1, "dvd_mul_left": 1, "expon": 1, "expand": [1, 2, 3, 4, 5], "w": [1, 6], "greatest": [1, 5, 7], "divisor": [1, 2, 4, 5], "gcd": [1, 2, 4], "least": [1, 5, 6, 7], "lcm": 1, "analog": [1, 2, 3, 4, 5, 7, 8], "divid": [1, 2, 4, 5], "gcd_zero_right": 1, "gcd_zero_left": 1, "lcm_zero_right": 1, "lcm_zero_left": 1, "similarli": [1, 2, 3, 4, 5], "prefix": [1, 4, 6], "dvd_antisymm": 1, "complain": 1, "ambigu": [1, 5], "_root_": [1, 4], "saw": [1, 5, 6, 7], "govern": [1, 5], "class": [1, 4, 5, 6, 7, 8, 9], "\u03b1": [1, 2, 3, 4, 5, 6, 7, 8, 9], "partialord": [1, 2], "adopt": 1, "letter": [1, 5, 8], "\u03b2": [1, 2, 3, 5, 6, 7, 9], "\u03b3": [1, 2, 5, 7], "greek": [1, 4], "especi": [1, 5, 6, 7], "strict": [1, 2], "somewhat": [1, 3, 7], "lt_irrefl": [1, 2], "lt_iff_le_and_n": 1, "lattic": [1, 5, 6, 7], "inf_le_left": [1, 7], "inf_le_right": 1, "le_inf": 1, "le_sup_left": 1, "le_sup_right": 1, "sup_l": 1, "lower": [1, 2, 4], "bound": [1, 2, 3, 4, 5, 7, 8, 9], "upper": [1, 2], "glb": 1, "lub": 1, "infimum": [1, 6, 7, 9], "supremum": [1, 4, 6], "inf": [1, 6, 7], "sup": [1, 4, 7], "further": [1, 7], "matter": [1, 2], "meet": [1, 2, 3, 5], "keep": [1, 5, 6], "dictionari": 1, "subset": [1, 2, 3, 5, 7, 8], "domain": [1, 2, 3, 4, 5, 7], "boolean": 1, "truth": [1, 4], "fals": [1, 2, 3, 4, 6], "true": [1, 2, 3, 6, 7], "posit": [1, 3, 4, 5, 7, 9], "subspac": [1, 6], "vector": [1, 3, 6, 8], "intersect": [1, 3, 5, 6, 7, 9], "sum": [1, 2, 4, 5, 6, 7], "inclus": [1, 3, 7], "topolog": [1, 5, 6, 8, 11], "union": [1, 3, 4, 5, 6, 8, 9], "inf_comm": 1, "inf_assoc": 1, "sup_comm": 1, "sup_assoc": 1, "absorpt": 1, "law": 1, "absorb1": 1, "absorb2": 1, "found": [1, 5, 8], "inf_sup_self": 1, "sup_inf_self": 1, "distriblattic": 1, "inf_sup_left": 1, "inf_sup_right": 1, "sup_inf_left": 1, "sup_inf_right": 1, "shown": [1, 5, 8, 9], "explicit": [1, 2, 5, 6, 7], "nondistribut": 1, "finit": [1, 3, 4, 5, 7, 8, 9], "impli": [1, 2, 3, 4, 5, 7], "larger": [1, 7], "carrier": [1, 5, 6], "compat": [1, 7], "strictorderedr": 1, "mul_po": [1, 4], "mul_nonneg": 1, "coupl": [1, 2, 6, 7], "metric": [1, 5, 8, 11], "equip": [1, 3, 5, 6, 7, 8, 9], "distanc": [1, 2, 7, 8], "dist": [1, 7], "map": [1, 2, 3, 5, 6, 7], "metricspac": [1, 7, 8], "dist_self": 1, "dist_comm": [1, 7], "dist_triangl": [1, 7], "nonneg": [1, 5], "nonneg_of_mul_nonneg_left": 1, "dist_nonneg": [1, 7], "dealt": 2, "simpl": [2, 4, 5, 6, 8], "absolut": 2, "\u03b5": [2, 7, 8], "though": [2, 3, 4, 5], "treat": [2, 3, 5, 6, 7, 8], "appli": [2, 3, 4, 5, 6, 7, 8, 9, 11], "my_lemma": 2, "\u03b4": [2, 7], "hb": [2, 7], "subsequ": [2, 4, 7], "lemma": [2, 4, 5, 6, 7, 8, 9, 11], "mention": [2, 3, 5, 6, 7], "my_lemma2": 2, "stage": [2, 5, 6], "my_lemma3": 2, "epo": 2, "ele1": 2, "xlt": 2, "ylt": 2, "essenti": [2, 3, 5, 7], "colon": 2, "off": [2, 3, 4], "my_lemma4": 2, "abs_mul": 2, "mul_le_mul": 2, "abs_nonneg": 2, "mul_lt_mul_right": 2, "extract": [2, 7], "hidden": 2, "expos": [2, 7], "predic": [2, 3, 4, 6, 7, 8], "fnub": 2, "fnlb": 2, "lambda": [2, 5], "hfa": 2, "hgb": 2, "dsimp": [2, 3, 4, 5], "simplif": [2, 3, 4], "contract": 2, "anyhow": 2, "control": 2, "transform": [2, 3], "rest": [2, 3, 5, 7], "routin": 2, "nnf": 2, "nng": 2, "hfb": 2, "nna": 2, "codomain": [2, 4, 7], "structur": [2, 4, 6, 7, 8, 9, 11], "monoid": [2, 3, 4, 6], "fnub_add": 2, "orderedcanceladdcommmonoid": 2, "high": 2, "monoton": [2, 6, 7], "nondecreas": [2, 4], "placehold": 2, "Or": [2, 3], "backward": [2, 7], "subgoal": 2, "mf": 2, "mg": 2, "aleb": 2, "flag": [2, 3], "squiggli": 2, "marker": 2, "nnc": 2, "bbb": [2, 5], "fneven": 2, "fnodd": 2, "ef": 2, "eg": 2, "og": 2, "shorten": 2, "rid": 2, "won": [2, 4, 6, 7], "cannot": [2, 3, 4, 5, 6, 7], "contrari": 2, "syntact": 2, "reduct": [2, 3], "erw": 2, "harder": 2, "spot": 2, "manipul": [2, 5, 7], "foundat": [2, 3, 4, 5], "mundan": 2, "assert": [2, 3, 6], "contrast": [2, 3, 5, 6, 7], "zermelo": 2, "fraenkel": 2, "sin": [2, 8], "co": 2, "zf": 2, "defect": [2, 6, 7], "theoret": [2, 3, 7], "motiv": 2, "detect": 2, "meaningless": 2, "independ": [2, 3, 5], "continuum": 2, "meta": [2, 6], "beyond": [2, 6, 8], "ask": [2, 4, 5, 6, 7], "xs": [2, 3], "refl": [2, 3, 5, 6], "tran": [2, 4, 5, 6], "setub": 2, "inject": [2, 3, 4, 6, 7], "x_1": [2, 3], "x_2": [2, 3], "x\u2081": [2, 3, 5, 7], "x\u2082": [2, 3, 5], "add": [2, 4, 5, 6, 7, 8], "nonzero": [2, 4, 5, 9], "sourc": [2, 7], "inspir": 2, "add_left_inj": 2, "composit": [2, 3, 5, 6, 7], "injg": 2, "injf": [2, 3], "canon": [2, 3, 4, 5], "exhibit": [2, 7], "anonym": [2, 3, 4, 5], "constructor": [2, 3, 4, 5, 6], "angl": 2, "certain": [2, 6, 7], "fnhasub": 2, "fnhaslb": 2, "ubf": 2, "ubg": 2, "ubfa": 2, "ubgb": 2, "unpack": [2, 3], "claus": [2, 6], "els": [2, 3, 4], "turn": [2, 3, 4, 5, 6, 7, 8], "fn_ub_add": 2, "directli": [2, 4, 5, 6, 7], "lbf": 2, "lbg": 2, "cousin": 2, "rcase": [2, 3, 4, 5, 7], "flexibl": [2, 7], "recurs": [2, 3, 5, 11], "harm": [2, 3], "swiss": 2, "armi": 2, "knive": 2, "wide": 2, "old": [2, 5, 6], "chestnut": 2, "product": [2, 4, 5, 6, 7, 9], "magic": [2, 5, 6], "verifi": 2, "sumofsquar": 2, "sumofsquares_mul": 2, "sosx": 2, "sosi": 2, "xeq": [2, 3], "yeq": 2, "insight": 2, "gaussian": [2, 11], "i": [2, 3, 4, 5, 7, 8, 9], "sqrt": [2, 3, 4, 5], "norm": [2, 5, 7, 11], "reflect": 2, "di": [2, 5], "xy": [2, 5], "cryptic": 2, "easiest": [2, 4], "perspicu": 2, "6": [2, 4, 5, 6, 7, 8], "divab": 2, "divbc": 2, "beq": 2, "ceq": 2, "And": [2, 4, 6, 7], "pretti": [2, 6, 7], "Then": [2, 3, 5, 6, 7, 9], "divac": 2, "alpha": [2, 3], "beta": [2, 3], "surject": [2, 3, 7], "yourself": [2, 5], "mul_div_cancel": [2, 4], "field_simp": [2, 5], "denomin": [2, 4, 5], "hx": [2, 3, 5, 6, 8], "surjg": 2, "surjf": [2, 3], "contradict": [2, 3, 4], "speak": [2, 5, 7], "irreflex": 2, "asymmetri": 2, "lt_asymm": 2, "sugar": 2, "eventu": [2, 3, 7], "fnuba": 2, "not_le_of_gt": 2, "not_lt_of_g": [2, 4, 5], "lt_of_not_g": 2, "le_of_not_gt": 2, "snippet": [2, 4, 5], "counterexampl": [2, 8], "monof": 2, "four": [2, 5], "valid": 2, "far": [2, 3, 6, 7], "q": [2, 4, 5, 6, 7], "straightforward": [2, 6], "difficult": [2, 6], "conclud": [2, 8], "nonexist": 2, "contradictori": 2, "classic": [2, 3, 4], "by_contra": [2, 4], "not_not": 2, "front": 2, "push": [2, 4, 7], "inward": 2, "facilit": [2, 7], "push_neg": [2, 3, 4], "restat": [2, 6], "contrapos": [2, 3, 4], "yet": [2, 3, 4, 5, 6, 7], "semicolon": [2, 4], "falso": 2, "anyth": [2, 5, 7], "elim": 2, "strang": [2, 4], "fairli": 2, "reach": [2, 6], "37": 2, "exfalso": 2, "absurd": [2, 4], "slick": 2, "drop": 2, "manner": [2, 5], "compon": [2, 3, 5, 7, 9], "techniqu": [2, 7], "variou": [2, 3, 5, 6, 9], "xltz": 2, "zlty": 2, "10": 2, "7": [2, 4], "behav": [2, 3, 6, 7], "roughli": [2, 3, 4], "friend": [2, 5], "were": [2, 4, 5, 7], "inscrut": [2, 3], "gadget": [2, 7], "auxiliari": [2, 7], "pow_eq_zero": [2, 4], "doubl": [2, 3], "symmetr": [2, 3], "abs_lt": 2, "dvd_gcd_iff": 2, "8": [2, 4, 7], "15": 2, "not_monotone_iff": 2, "antisymmetr": 2, "aris": 2, "preorder": [2, 6, 7], "pre": 2, "lt_iff_le_not_l": 2, "repeatedli": [2, 7], "instanti": [2, 5, 6, 7], "inl": [2, 3], "inr": [2, 3], "produc": [2, 8], "branch": [2, 3, 6], "le_or_gt": 2, "abs_of_nonneg": [2, 5], "abs_of_neg": 2, "immedi": [2, 3, 5, 6], "myab": 2, "le_abs_self": 2, "neg_le_abs_self": 2, "enjoi": [2, 3, 4, 7], "pun": 2, "lt_ab": 2, "genuin": 2, "vertic": [2, 5], "lt_trichotomi": 2, "xgt": 2, "dvd_mul_right": [2, 4], "eq_zero_or_eq_zero_of_mul_eq_zero": 2, "zero": [2, 3, 4, 5, 6, 7, 8, 9], "nontrivi": [2, 3, 4, 5, 7], "integr": [2, 8, 11], "isdomain": 2, "em": [2, 3], "exclud": [2, 4], "by_cas": [2, 3, 4], "dispos": 2, "s_0": [2, 3], "s_1": 2, "s_2": 2, "ldot": [2, 3, 4], "varepsilon": [2, 7], "s_n": [2, 3], "render": [2, 4], "convergesto": 2, "ext": [2, 3, 4, 5, 6], "enabl": [2, 3, 4, 5], "actual": [2, 3, 4, 6, 7], "u": [2, 3, 5, 7, 9], "v": [2, 3, 5, 7], "congr": 2, "reconcil": 2, "peel": 2, "ab": [2, 5], "convert": [2, 4], "quit": [2, 6, 7], "zero_lt_on": [2, 4], "fill": [2, 3, 4, 5], "convergesto_const": 2, "\u03b5po": [2, 7], "nge": 2, "abs_zero": 2, "save": 2, "troubl": [2, 3, 5], "pen": 2, "paper": [2, 3, 5, 7, 9], "ns": 2, "nt": 2, "maximum": [2, 4, 7], "implement": [2, 5, 6, 8], "convergesto_add": 2, "cs": 2, "ct": 2, "clean": [2, 7], "\u03b52po": 2, "hs": [2, 4, 7, 9], "ht": 2, "le_of_max_le_left": 2, "le_of_max_le_right": 2, "tricki": [2, 3, 4, 6], "convergesto_mul_const": 2, "acpo": 2, "abs_po": 2, "exists_abs_le_of_convergesto": 2, "strong": [2, 4], "n\u2080": 2, "bpo": [2, 7], "pos\u2080": 2, "div_po": 2, "n\u2081": 2, "convergesto_mul": 2, "sketch": [2, 3, 4, 7], "limit": [2, 6, 7], "bold": 2, "scratch": 2, "convergesto_uniqu": 2, "sa": 2, "sb": 2, "abn": 2, "na": 2, "hna": 2, "nb": 2, "hnb": 2, "absa": 2, "absb": 2, "observ": [2, 4, 7], "everywher": [2, 3, 6, 7, 9], "linearord": 2, "vastli": 2, "awai": [2, 5], "vocabulari": 3, "uniform": [3, 7, 8], "primit": 3, "conceptu": 3, "advantag": [3, 4, 5, 8], "overload": 3, "verbos": 3, "system": [3, 4, 5, 6], "wrong": 3, "ss": 3, "sub": [3, 7, 9, 11], "cap": 3, "un": 3, "cup": 3, "univ": [3, 7, 8, 9], "empti": [3, 4, 5, 7, 9], "member": [3, 7], "membership": [3, 4, 6], "mem": 3, "notin": 3, "ident": [3, 4, 5, 6, 7, 11], "databas": [3, 4, 6, 7], "unlik": [3, 4], "existenti": [3, 11], "subset_def": 3, "inter_def": 3, "mem_setof": 3, "xu": 3, "mem_inter_iff": 3, "xsu": 3, "phenomenon": 3, "quirk": 3, "process": 3, "pitfal": 3, "heavili": [3, 7], "fall": 3, "union_def": 3, "mem_union": [3, 4], "xtu": 3, "xt": 3, "unnecessari": 3, "correctli": 3, "special": [3, 4, 5, 6, 7, 9], "rewritten": 3, "diff_eq": 3, "mem_diff": 3, "xstu": 3, "xnt": 3, "xnu": 3, "extension": [3, 5], "unsurprisingli": 3, "and_comm": 3, "antisymm": 3, "hood": [3, 5], "builder": 3, "trivial": [3, 4, 7], "eq_two_or_odd": 3, "even_iff": 3, "confus": [3, 4, 6, 7], "fortun": 3, "agre": 3, "prime_iff": 3, "symm": [3, 4, 5, 6, 7, 8], "rwa": [3, 4, 5], "restrict": [3, 4, 7], "signific": 3, "ball": [3, 8], "bex": 3, "bex_def": 3, "prime_x": 3, "slight": 3, "ssubt": 3, "index": [3, 6, 7], "model": [3, 7], "sequenc": [3, 6, 7, 8, 11], "a_0": 3, "a_1": 3, "a_2": 3, "mem_iunion": 3, "xai": 3, "mem_iint": 3, "mem_iunion\u2082": 3, "mem_iinter\u2082": 3, "exists_prime_and_dvd": 3, "eq_univ": 3, "eq_univ_of_foral": 3, "exists_infinite_prim": 3, "\u2080": 3, "sunion": 3, "sinter": 3, "relationship": [3, 4], "sunion_eq_biunion": 3, "sinter_eq_biint": 3, "preimag": [3, 7], "imag": [3, 4, 6, 7], "tripl": 3, "tag": [3, 6], "mem_image_of_mem": 3, "galoi": [3, 5, 7], "image_subset_iff": 3, "represent": [3, 4, 5], "asid": 3, "raini": 3, "dai": 3, "behavior": [3, 6, 7], "nonempti": [3, 7], "condit": [3, 4, 6, 7, 8], "fxeq": 3, "ai": 3, "fx": 3, "eq": [3, 5], "injon": [3, 9], "theme": 3, "rel": [3, 5], "relativ": 3, "xpo": 3, "ypo": 3, "exp_log": 3, "ingredi": [3, 5, 7, 8], "assign": [3, 5, 6], "inhabit": [3, 5, 7], "appeal": [3, 6], "choose_spec": 3, "noncomput": [3, 5], "inverse_spec": 3, "dif_po": 3, "dif_neg": 3, "fulli": [3, 7], "alon": 3, "leftinvers": 3, "rightinvers": 3, "hack": 3, "half": 3, "dozen": 3, "condens": 3, "cantor": 3, "famou": 3, "j": [3, 5], "intuit": [3, 7], "cardin": 3, "biject": [3, 5], "nineteenth": 3, "centuri": 3, "infinit": [3, 7, 11], "dedekind": 3, "quickli": [3, 9], "behind": 3, "problem": [3, 4, 5, 6, 7], "shade": 3, "region": 3, "diagram": 3, "circ": [3, 5], "scale": 3, "inner": 3, "smaller": [3, 4, 7], "concentr": 3, "unshad": 3, "compos": [3, 5, 7], "disjoint": [3, 9], "sound": [3, 5, 6], "plausibl": 3, "delic": 3, "improv": [3, 4], "confid": 3, "better": [3, 4, 5, 6, 7], "invfun": [3, 5], "leftinverse_invfun": 3, "invfun_eq": 3, "sbaux": 3, "sbset": 3, "sb_aux": 3, "s_": 3, "sb_set": 3, "bigcup_": 3, "mathbb": [3, 4, 5], "sbfun": 3, "complement": [3, 7, 9], "outermost": 3, "setminu": 3, "inv_fun": 3, "inv_fun_eq": 3, "sb_right_inv": 3, "goe": [3, 4, 5, 6, 7], "neither": [3, 5, 6], "nor": [3, 5], "sb_inject": 3, "hf": [3, 7, 8, 9], "hg": [3, 7, 8, 9], "a_def": 3, "h_def": 3, "hxeq": 3, "xa": [3, 5], "wlog": 3, "x\u2081a": 3, "resolve_left": 3, "x\u2082a": 3, "not_imp_self": 3, "x\u2082na": 3, "if_po": 3, "if_neg": 3, "x\u2082eq": 3, "hn": [3, 4, 7, 8], "sb_fun": 3, "bring": [3, 4, 7], "tradeoff": 3, "encapsul": [3, 5, 8], "symmetri": [3, 6], "dwell": 3, "succ": [3, 4, 6], "sb_surject": 3, "gya": 3, "xmem": 3, "sweet": 3, "schroeder_bernstein": 3, "substant": 4, "ancient": 4, "fraction": 4, "lowest": 4, "2c": 4, "4c": 4, "factor": [4, 5], "coprim": 4, "smart": 4, "12": 4, "encount": [4, 6], "algebra": [4, 6, 7, 8, 9, 11], "prime_def_lt": 4, "eq_one_or_self_of_dvd": 4, "prime_p": 4, "17": 4, "commonli": [4, 5], "prime_two": 4, "prime_thre": 4, "broader": [4, 8], "irreduc": [4, 5], "coincid": [4, 5, 7], "rise": [4, 6], "dvd_mul": 4, "even_of_even_sqr": 4, "dvd_of_dvd_pow": 4, "proce": [4, 6], "profici": 4, "search": [4, 5, 6], "engin": 4, "hesit": 4, "mul_right_inj": 4, "heart": 4, "irration": 4, "dvd_gcd": 4, "coprime_mn": 4, "sqr_eq": 4, "meq": 4, "dvd_iff_exists_eq_mul_left": 4, "two_l": 4, "le_of_dvd": 4, "approach": [4, 5, 6, 7], "quick": [4, 8], "ne": [4, 5], "occur": 4, "suffici": [4, 7], "permut": 4, "prime_of_mem_factor": 4, "prod_factor": 4, "factors_uniqu": 4, "talk": [4, 7, 8], "factorization_mul": 4, "mnez": 4, "nnez": 4, "factorization_pow": 4, "black": [4, 6], "box": 4, "simpa": [4, 8], "nnz": 4, "nsqr_nez": 4, "eq1": 4, "eq2": 4, "add_mul_mod_self_left": 4, "mul_mod_right": 4, "count_factors_mul_of_po": 4, "successor": 4, "succ_ne_zero": 4, "npow_nz": 4, "dvd_sub": 4, "pow_eq": 4, "npowz": 4, "add_sub_cancel": 4, "understood": [4, 7], "quotient": [4, 5, 6, 7], "pictur": [4, 5], "mediat": 4, "headach": 4, "contend": 4, "issu": [4, 5, 6, 7], "th": 4, "topic": [4, 6], "enat": 4, "infin": [4, 7, 9], "appreci": 4, "role": [4, 5, 7], "datatyp": 4, "freeli": 4, "translat": [4, 6, 7], "mathematician": [4, 7], "inj": 4, "factori": 4, "fac": 4, "ih": 4, "fac_po": 4, "succ_po": 4, "dvd_fac": 4, "ipo": 4, "il": 4, "of_le_succ": 4, "dvd_mul_of_dvd_right": 4, "crude": 4, "remaind": [4, 5], "pow_two_le_fac": 4, "finset": [4, 5, 7], "bigoper": [4, 5], "prod": [4, 7, 9], "sum_range_zero": 4, "sum_range_succ": 4, "summat": 4, "prod_range_zero": 4, "prod_range_succ": 4, "deserv": 4, "danger": [4, 5], "ordinarili": [4, 5], "loop": 4, "indefinit": 4, "fix": [4, 6, 7], "placement": 4, "re": [4, 5], "handi": 4, "sum_id": 4, "div_eq_of_eq_mul_right": 4, "succ_eq_add_on": 4, "sum_sqr": 4, "mynat": 4, "thumb": 4, "decid": [4, 7], "preced": 4, "truncat": 4, "exponenti": 4, "cut": 4, "predecessor": 4, "pred": 4, "mul": [4, 5, 6, 7], "succ_add": 4, "succ_mul": 4, "explor": [4, 7], "standard": [4, 5, 6, 7], "formul": [4, 7], "quirki": 4, "among": 4, "annoi": [4, 6], "h0": 4, "succ_le_succ": 4, "zero_l": [4, 5], "interval_cas": 4, "interv": [4, 7, 9], "decis": 4, "procedur": [4, 6], "revert": [4, 5], "minfac": 4, "smallest": [4, 6, 7], "strong_induction_on": 4, "subsum": 4, "exists_prime_factor": 4, "np": 4, "mltn": 4, "mdvdn": 4, "mne1": 4, "mz": 4, "zero_dvd_iff": 4, "mgt2": 4, "pp": 4, "pdvd": 4, "factorial_po": 4, "dvd_factori": 4, "primes_infinit": 4, "refin": [4, 8], "ple": 4, "p_1": 4, "p_n": 4, "prod_": 4, "p_i": [4, 7], "computation": 4, "test": 4, "decidableeq": 4, "abandon": 4, "ourselv": [4, 6], "subset_iff": 4, "mem_int": 4, "mem_sdiff": 4, "tauto": 4, "dispens": 4, "tautolog": 4, "dvd_prod_of_mem": 4, "eq_of_dvd_of_prim": 4, "prime_q": 4, "preserv": [4, 6, 7], "induction_on": 4, "singleton": 4, "prod_empti": 4, "prod_insert": 4, "mem_of_dvd_prod_prim": 4, "mem_insert": 4, "wrote": 4, "filter": [4, 8, 9, 11], "mem_filt": 4, "aim": 4, "prod_po": 4, "_def": 4, "mem_": 4, "id": [4, 6, 7, 8], "bounded_of_ex_finset": 4, "qk": 4, "lt_succ_of_l": 4, "le_sup": 4, "ex_finset_of_bound": 4, "decidablepr": 4, "lt_succ_iff": 4, "congruent": 4, "p_k": 4, "loss": 4, "27": 4, "mod_4_eq_3_or_mod_4_eq_3": 4, "mul_mod": 4, "mod_lt": 4, "hm": [4, 8], "two_le_of_mod_4_eq_3": 4, "neq": 4, "div_dvd_of_dvd": 4, "div_lt_self": 4, "exists_prime_factor_mod_4_eq_3": 4, "dvd_rfl": 4, "mge2": 4, "home": [4, 5], "stretch": [4, 5], "remov": [4, 7], "eras": 4, "mem_eras": 4, "readi": [4, 6, 7, 8], "dvd_add_iff_left": 4, "primes_mod_4_eq_3_infinit": 4, "p4": 4, "pltn": 4, "p4eq": 4, "ps": 4, "pne3": 4, "seriou": [4, 6, 7], "feat": 4, "modern": 5, "subject": 5, "mysteri": [5, 6], "consult": 5, "ann": 5, "baanen": 5, "abus": 5, "paramet": [5, 6], "broadest": 5, "constraint": [5, 7], "bundl": [5, 6, 7, 8], "tupl": 5, "hy": [5, 6], "hz": [5, 6], "mypoint1": 5, "mypoint2": 5, "mypoint3": 5, "mk": [5, 6, 7], "former": 5, "latter": [5, 7], "quot": [5, 7], "protect": 5, "intern": 5, "add_x": 5, "addalt": 5, "etc": [5, 7], "y\u2081": 5, "z\u2081": 5, "y\u2082": 5, "z\u2082": 5, "addalt_x": 5, "addalt_comm": 5, "ya": 5, "za": 5, "xb": 5, "yb": 5, "zb": 5, "apart": [5, 6], "effici": [5, 7], "scalar": [5, 6, 8], "smul": [5, 6], "smul_distrib": 5, "road": 5, "link": [5, 6], "belong": [5, 6, 7], "simplex": 5, "convinc": 5, "equilater": 5, "interior": [5, 8], "standardtwosimplex": 5, "x_nonneg": 5, "y_nonneg": 5, "z_nonneg": 5, "sum_eq": 5, "swap": 5, "swapxi": 5, "interestingli": [5, 8], "midpoint": 5, "div_nonneg": 5, "weight": 5, "averag": 5, "weightedaverag": 5, "lambda_nonneg": 5, "lambda_l": 5, "fin": [5, 9], "standardsimplex": 5, "sum_eq_on": 5, "div_eq_mul_inv": 5, "sum_mul": 5, "sum_add_distrib": 5, "mul_sum": 5, "islinear": 5, "is_addit": 5, "preserves_mul": 5, "linf": 5, "subtyp": [5, 6, 7], "preal": 5, "val": 5, "sigma": [5, 9], "wherebi": [5, 7], "stdsimplex": 5, "\u03c3": 5, "fst": [5, 7], "snd": [5, 7], "custom": 5, "robust": [5, 6], "interfac": 5, "redefin": [5, 6], "accessor": 5, "weav": 5, "rich": [5, 6], "interconnect": 5, "hierarchi": [5, 11], "clarifi": 5, "antireflex": 5, "cdot": 5, "mathcal": [5, 8], "proxi": 5, "bipartit": 5, "graph": 5, "categori": [5, 7, 8], "morphism": [5, 8, 11], "basi": [5, 7], "discret": [5, 8], "inherit": [5, 6], "polynomi": 5, "coeffici": 5, "dual": [5, 7], "accommod": 5, "almost": [5, 6, 7, 9], "marriag": 5, "heaven": 5, "group\u2081": [5, 6], "inv": [5, 6], "struc": 5, "counterpart": 5, "chosen": 5, "assur": 5, "groupcat": 5, "group\u2081cat": 5, "str": 5, "capit": 5, "roman": 5, "equiv": 5, "tofun": [5, 6], "right_inv": 5, "left_inv": 5, "creativ": 5, "evid": 5, "coercion": [5, 6, 7, 8], "omit": 5, "perm": 5, "under": [5, 6, 7], "orient": 5, "permgroup": 5, "trans_assoc": 5, "trans_refl": 5, "refl_tran": 5, "self_trans_symm": 5, "grouptheori": 5, "g_1": 5, "g_2": 5, "g_3": 5, "tightli": 5, "isomorph": [5, 8], "Its": [5, 6], "neg": [5, 6, 7, 9], "reproduc": 5, "accompani": 5, "addgroup\u2081": 5, "scheme": 5, "addgrouppoint": 5, "arrang": 5, "mul_inv_cancel_right": 5, "achiev": [5, 6, 7], "silent": [5, 6], "regist": [5, 6], "grp": 5, "contextu": 5, "cue": 5, "synthes": [5, 6], "whole": 5, "_inst_1": 5, "candid": 5, "group\u2082": 5, "mysquar": 5, "my_squar": 5, "remark": [5, 6], "headi": 5, "store": 5, "hasmulgroup\u2082": 5, "hasonegroup\u2082": 5, "hasinvgroup\u2082": 5, "suppli": 5, "accord": 5, "capabl": 5, "chain": 5, "recent": 5, "prioriti": 5, "bad": [5, 6, 7], "artifici": 5, "addgroup\u2082": 5, "subtl": [5, 7], "configur": 5, "invis": [5, 6], "wise": 5, "euclidean": 5, "terminolog": 5, "mid": 5, "imaginari": 5, "gaussint": 5, "im": 5, "pointwis": [5, 7, 8], "root": [5, 6, 11], "ac": 5, "bci": 5, "adi": 5, "bd": 5, "bc": 5, "hasmul": 5, "zero_def": 5, "one_def": 5, "add_def": 5, "neg_def": 5, "mul_def": 5, "zero_r": 5, "zero_im": 5, "one_r": 5, "one_im": 5, "add_r": 5, "add_im": 5, "neg_r": 5, "neg_im": 5, "mul_r": 5, "mul_im": 5, "surprisingli": [5, 6], "concept": [5, 7, 8], "light": 5, "bulb": 5, "skeleton": [5, 7], "scari": 5, "instcommr": 5, "left_distrib": [5, 6], "right_distrib": [5, 6], "ext_iff": 5, "bq": 5, "archetyp": 5, "int": [5, 6], "ediv_add_emod": 5, "emod_nonneg": 5, "emod_lt": 5, "unit": [5, 6, 7], "algorithm": 5, "conjug": 5, "frac": 5, "nearest": 5, "size": 5, "vi": 5, "multipli": 5, "emb": 5, "forth": 5, "quadrat": 5, "gaussianint": 5, "stai": 5, "face": [5, 6, 7], "machineri": [5, 6, 7], "adapt": 5, "invest": 5, "pragmat": 5, "seek": 5, "heather": 5, "macbeth": 5, "eleg": 5, "div": 5, "mod": 5, "_add_mod": 5, "abs_mod": 5, "_le": 5, "emod_lt_of_po": 5, "zero_lt_two": 5, "fixm": 5, "_eq": 5, "sq_add_sq_eq_zero": 5, "linearorderedr": 5, "norm_nonneg": [5, 8], "norm_eq_zero": [5, 8], "norm_po": 5, "norm_mul": [5, 8], "conj": 5, "conj_r": 5, "conj_im": 5, "norm_conj": 5, "bespok": 5, "quad": 5, "record": [5, 6], "div_def": 5, "mod_def": 5, "messi": 5, "nicer": [5, 7], "norm_mod_lt": 5, "norm_y_po": 5, "sq_ab": 5, "gcongr": 5, "ediv_mul_l": 5, "le_of_mul_le_mul_right": 5, "ediv_lt_of_lt_mul": 5, "natab": 5, "coe_natabs_norm": 5, "natabs_of_nonneg": 5, "natabs_norm_mod_lt": 5, "ofnat_lt": 5, "coe_natab": 5, "not_norm_mul_left_lt_norm": 5, "natabs_mul": 5, "le_mul_of_one_le_right": 5, "ofnat_l": 5, "add_one_le_of_lt": 5, "euclideandomain": 5, "quotient_mul_add_remainder_eq": 5, "quotient_zero": 5, "r_wellfound": 5, "remainder_lt": 5, "mul_left_not_lt": 5, "payoff": 5, "principalidealr": 5, "irreducible_iff_prim": 5, "studi": [6, 7], "prematur": 6, "technolog": 6, "simpler": 6, "ring\u2081": 6, "gradual": [6, 7], "bottom": [6, 7], "endow": 6, "one\u2081": 6, "heavier": 6, "inferr": 6, "resolut": 6, "ie": [6, 7], "attribut": 6, "ensur": [6, 7], "self": 6, "one\u2082": 6, "usabl": 6, "silli": 6, "affect": 6, "importantli": 6, "habit": 6, "ascript": 6, "messag": 6, "typeclass": 6, "stuck": 6, "metavari": 6, "263": 6, "auto": 6, "sever": [6, 7, 9], "unknown": 6, "collis": 6, "builtin": 6, "\ud835\udfd9": 6, "inherit_doc": 6, "diamond": 6, "dia\u2081": 6, "dia": 6, "infixl": 6, "70": 6, "semigroup": 6, "dia_assoc": 6, "semigroup\u2081": 6, "todia\u2081": 6, "previous": 6, "semigroup\u2082": 6, "hurdl": 6, "neutral": 6, "diaoneclass\u2081": 6, "one_dia": 6, "dia_on": 6, "trace": 6, "info": 6, "ters": 6, "expend": 6, "attempt": 6, "succe": 6, "success": 6, "set_opt": 6, "synthinst": 6, "monoid\u2081": 6, "hide": [6, 7], "subtleti": 6, "fear": 6, "unrel": 6, "tosemigroup\u2081": 6, "todiaoneclass\u2081": 6, "monoid\u2082": 6, "toone\u2081": 6, "overlap": 6, "tear": 6, "signatur": 6, "restor": 6, "optim": [6, 9], "reusabl": 6, "inv\u2081": 6, "postfix": 6, "inv_dia": 6, "weak": 6, "preliminari": 6, "left_inv_eq_right_inv\u2081": 6, "hba": 6, "hac": 6, "export": 6, "inv_eq_of_dia": 6, "dia_inv": 6, "naiv": [6, 7], "duplic": 6, "to_addit": 6, "semi": 6, "left_inv_eq_right_inv": 6, "left_neg_eq_right_neg": 6, "whatsnew": 6, "addsemigroup\u2083": 6, "add_assoc\u2083": 6, "semigroup\u2083": 6, "mul_assoc\u2083": 6, "addmonoid\u2083": 6, "addzeroclass": 6, "monoid\u2083": 6, "muloneclass": 6, "tomuloneclass": 6, "addcommsemigroup\u2083": 6, "commsemigroup\u2083": 6, "addcommmonoid\u2083": 6, "commmonoid\u2083": 6, "addgroup\u2083": 6, "neg_add": 6, "group\u2083": 6, "inv_mul": 6, "inv_eq_of_mul": 6, "propag": 6, "attr": 6, "mul_inv": 6, "mul_left_cancel\u2083": 6, "mul_right_cancel\u2083": 6, "addcommgroup\u2083": 6, "commgroup\u2083": 6, "demonstr": [6, 7], "opposit": [6, 7], "gain": 6, "besid": 6, "parent": 6, "ring\u2083": 6, "mulzeroclass": 6, "toaddgroup\u2083": 6, "mayb": 6, "le\u2081": 6, "50": 6, "\u2081": 6, "preorder\u2081": 6, "partialorder\u2081": 6, "orderedcommmonoid\u2081": 6, "modul": 6, "pretend": 6, "smul\u2083": 6, "infixr": 6, "73": 6, "module\u2081": 6, "zero_smul": 6, "one_smul": 6, "mul_smul": 6, "add_smul": 6, "smul_add": 6, "surpris": 6, "toaddcommgroup\u2083": 6, "inst": 6, "module\u2083": 6, "hunt": 6, "unspecifi": 6, "embark": 6, "main": [6, 7, 8], "quest": 6, "huge": 6, "trap": 6, "refus": [6, 7], "tosmul\u2083": 6, "inst_1": 6, "safe": 6, "selfmodul": 6, "invert": 6, "nsmul\u2081": 6, "zsmul\u2081": 6, "ofnat": 6, "negsucc": 6, "intermedi": [6, 7], "abgrpmodul": 6, "failur": 6, "synth": 6, "indirect": 6, "path": 6, "thank": [6, 7], "offend": 6, "poor": 6, "forget": 6, "inria": 6, "hal": 6, "scienc": 6, "02463336": 6, "modifi": 6, "nsmul": 6, "addmonoid\u2084": 6, "nsmul_zero": 6, "nsmul_succ": 6, "mysmul": 6, "stori": 6, "incorpor": 6, "zsmul": 6, "lt\u2081": 6, "comparison": 6, "ismonoidhom\u2081": 6, "unpleas": [6, 7], "conjunct": [6, 11], "chose": 6, "ismonoidhom\u2082": 6, "map_on": 6, "map_mul": 6, "tempt": 6, "higher": 6, "unif": 6, "psycholog": 6, "rare": 6, "adject": 6, "bare": 6, "noun": 6, "argu": 6, "continuous_id": [6, 7], "primari": 6, "monoidhom\u2081": 6, "coefun": 6, "coerc": 6, "coe": 6, "addmonoidhom\u2081": 6, "addmonoid": 6, "map_zero": 6, "map_add": [6, 8], "ringhom\u2081": 6, "minor": [6, 8], "tomonoidhom\u2081": 6, "juggl": 6, "monoidhomclass\u2081": 6, "badinst": 6, "wouldn": 6, "priori": 6, "boil": 6, "hopelessli": 6, "checksynthord": 6, "random": 6, "deduc": [6, 7], "outparam": 6, "trigger": 6, "retri": 6, "monoidhomclass\u2082": 6, "promis": [6, 7], "map_inv_of_inv": 6, "sight": 6, "got": 6, "presenc": 6, "layer": [6, 7], "funlik": 6, "monoidhomclass": 6, "monoidhomclass\u2083": 6, "coe_inject": 6, "stop": 6, "ringhomclass\u2083": 6, "ringhom": 6, "algebrahom": 6, "ve": [6, 7], "primarili": [6, 7], "unbundl": 6, "orderpreshom": 6, "le_of_l": 6, "orderpresmonoidhom": 6, "orderpreshomclass": 6, "subgroup": 6, "subr": 6, "reus": 6, "led": 6, "descend": 6, "break": 6, "barrier": 6, "setlik": 6, "wrap": [6, 7], "submonoid\u2081": 6, "submonoid": 6, "mul_mem": 6, "one_mem": 6, "tackl": 6, "setco": 6, "submonoid\u2081monoid": 6, "destructur": 6, "binder": 6, "submonoidclass\u2081": 6, "subgroup\u2081": 6, "subgroupclass\u2081": 6, "subobject": 6, "s\u2081": 6, "s\u2082": 6, "shame": 6, "across": 6, "weird": [6, 7], "distract": 6, "emphas": 6, "anecdot": 6, "devic": 6, "hasquoti": 6, "bewar": 6, "regular": [6, 7], "ascii": 6, "setoid": 6, "commmonoid": 6, "iseqv": 6, "hw": 6, "quotientmonoid": 6, "map\u2082": 6, "calculu": [7, 9, 11], "quantiti": 7, "begun": 7, "paradox": 7, "exot": 7, "x\u2080": [7, 8], "convention": 7, "eight": 7, "varieti": 7, "wish": 7, "64": 7, "y\u2080": 7, "z\u2080": 7, "paragraph": 7, "512": 7, "bourbaki": 7, "spell": 7, "dualli": 7, "arbitrarili": 7, "neighborhood": 7, "attop": [7, 9], "\ud835\udcdd": [7, 8, 9], "\ud835\udce4": 7, "entourag": 7, "\u03bc": [7, 9], "a_": 7, "univ_set": 7, "sets_of_superset": 7, "inter_set": 7, "blur": 7, "princip": 7, "\ud835\udcdf": 7, "opportun": 7, "x_0": 7, "ioo": [7, 8], "tendsto\u2081": 7, "tendsto": [7, 9], "lim_": 7, "abstractli": 7, "salient": 7, "pushforward": 7, "f_": 7, "tendsto\u2082": 7, "via": 7, "leverag": 7, "map_mono": 7, "map_map": 7, "shot": 7, "256": 7, "pullback": 7, "comap": 7, "map_le_iff_le_comap": 7, "contravari": 7, "comap_comap": 7, "plane": 7, "\u02e2": 7, "nhds_prod_eq": 7, "aforement": 7, "le_inf_iff": 7, "shouldn": 7, "prohibit": 7, "global": 7, "precondit": 7, "closur": 7, "nebot": 7, "tour": [7, 8], "claim": 7, "recaptur": 7, "superfici": 7, "stronger": 7, "famili": [7, 8], "\u03b9": [7, 8, 9], "hasbasi": 7, "nhds_basis_ioo_po": 7, "has_basi": 7, "tendsto_iff": 7, "reformul": 7, "ici": 7, "attop_basi": 7, "knew": 7, "gave": 7, "n_p": 7, "n_q": 7, "tiresom": 7, "\u1da0": [7, 8, 9], "superscript": 7, "hp": 7, "hq": 7, "eventually_eq": 7, "tendsto_congr": 7, "review": 7, "eventually_of_foral": 7, "mono": 7, "item": 7, "filter_upward": 7, "hr": 7, "ae": [7, 9], "aka": 7, "occasion": 7, "frequent": 7, "sophist": 7, "mem_closure_of_tendsto": 7, "clusterpt": 7, "mem_closure_iff_clusterpt": 7, "le_principal_iff": 7, "nebot_of_l": 7, "hux": 7, "hum": 7, "dist_eq_zero": 7, "emetricspac": 7, "pseudometricspac": 7, "pseudoemetricspac": 7, "journei": 7, "recast": 7, "tendsto_attop": 7, "continuous_iff": 7, "devot": 7, "uncurri": 7, "slow": 7, "continuous_fst": 7, "comp": 7, "assembl": 7, "prod_mk": 7, "continuous_snd": 7, "continuous_dist": 7, "clunki": 7, "crucial": 7, "elabor": 7, "prod_map": 7, "sad": 7, "border": 7, "obfusc": 7, "continuous_pow": 7, "continuousat": [7, 9], "continuousat_iff": 7, "geometr": 7, "closedbal": 7, "sign": 7, "radiu": 7, "mem_ball_self": 7, "mem_closedball_self": 7, "isopen": 7, "isopen_iff": 7, "Their": [7, 8], "isclos": [7, 8], "s\u1d9c": [7, 9], "isopen_compl_iff": 7, "hu": [7, 8], "mem_of_tendsto": 7, "mem_closure_iff": 7, "mem_closure_iff_seq_limit": 7, "nhds_basis_bal": 7, "nhds_basis_closedbal": 7, "mem_iff": 7, "segment": [7, 9], "somewher": 7, "continuouson": [7, 8], "minimum": 7, "iscompact": 7, "icc": [7, 8], "iscompact_icc": 7, "\u03c6": 7, "strictmono": 7, "tendsto_subseq": 7, "exists_forall_l": 7, "exists_forall_g": 7, "compactspac": 7, "iscompact_univ": 7, "cauchi": 7, "uniformcontinu": 7, "uniformcontinuous_iff": 7, "clearli": 7, "isclosed_l": 7, "eq_empty_or_nonempti": 7, "attain": 7, "closer": 7, "cauchyseq": 7, "cauchyseq_iff": 7, "completespac": [7, 8, 9], "cauchyseq_tendsto_of_complet": 7, "criterion": 7, "tendsto_pow_attop_nhds_0_of_lt_1": 7, "dist_le_range_sum_dist": 7, "cauchyseq_of_le_geometric_two": 7, "\u03b5_po": [7, 8], "le_iff_exists_add": 7, "boss": 7, "bair": [7, 8], "exclam": 7, "induct": [7, 11], "rec_on": 7, "ho": 7, "hd": 7, "dens": 7, "densiti": 7, "\u03b4po": 7, "hpo": 7, "hball": 7, "mem_closure_iff_nhds_basi": 7, "recon": 7, "rpo": 7, "rb": 7, "incl": 7, "cdist": 7, "ylim": 7, "yball": 7, "categor": 7, "topologicalspac": [7, 8], "isopen_univ": 7, "isopen_empti": 7, "isopen_iunion": 7, "fintyp": 7, "isopen_iint": 7, "continuous_def": 7, "attach": 7, "filteri": 7, "sent": 7, "mem_nhds_iff": 7, "digress": 7, "pure_le_nhd": 7, "eventually_eventually_nhd": 7, "topological_spac": 7, "mk_of_nhd": 7, "nhds_mk_of_nhd": 7, "functori": 7, "induc": 7, "sensibl": 7, "uncount": 7, "relatedli": 7, "coinduc": 7, "t_x": 7, "t_y": 7, "coinduced_le_iff_le_induc": 7, "covari": 7, "coinduced_compos": 7, "induced_compos": 7, "topological_structur": 7, "focus": 7, "nhd": 7, "recov": 7, "continuous_iff_coinduced_l": 7, "g_": 7, "t_z": 7, "wasn": 7, "\u03c0": [7, 8], "t_": 7, "x_i": 7, "pi": 7, "price": 7, "patholog": 7, "t2_space": 7, "hausdorff": 7, "t2space": 7, "tendsto_nhds_uniqu": 7, "regularspac": 7, "closed_nhds_basi": 7, "nhds_basis_open": 7, "denseinduc": 7, "continuousat_extend": 7, "funni": 7, "_in": 7, "nhds_induc": 7, "is_open": 7, "fortiori": 7, "f_cont": 7, "tendsto_right_iff": 7, "firstcountabletopolog": 7, "cluster": 7, "at_top": 7, "hfx": 7, "push_pul": 7, "of_map": 7, "f_ne": 7, "f_le": 7, "map_eq": 7, "hne": 7, "hle": 7, "huo": 7, "hsu": 7, "elim_finite_subcov": 7, "9": 8, "introductori": 8, "hasderivat": [8, 9], "hasderivat_sin": 8, "differentiable_at": 8, "differentiableat": 8, "inconveni": 8, "deriv_zero_of_not_differentiableat": 8, "deriv_add": 8, "islocalmin": 8, "deriv_eq_zero": 8, "ev": 8, "roll": 8, "weirder": 8, "hab": 8, "hfc": 8, "hfi": 8, "exists_deriv_eq_zero": 8, "differentiableon": 8, "exists_deriv_eq_slop": 8, "normedaddcommgroup": [8, 9], "norm_add_l": 8, "infer_inst": [8, 9], "normed_spac": 8, "normed_add_group": 8, "stipul": 8, "normedspac": [8, 9], "norm_smul": 8, "banach": [8, 9], "dimension": [8, 9], "finitedimension": [8, 9], "\ud835\udd5c": [8, 9], "nontriviallynormedfield": [8, 9], "normedfield": 8, "exists_one_lt_norm": 8, "nondiscret": 8, "continuouslinearmap": 8, "cont": 8, "map_smul": 8, "le_op_norm": 8, "hmp": 8, "op_norm_le_bound": 8, "steinhau": 8, "bounded": 8, "uniformli": 8, "nonempty_interior_of_union_of_clos": 8, "continuous_linear_map": 8, "op_norm_le_of_shel": 8, "interior_subset": 8, "interior_inter_subset": 8, "is_closed_l": 8, "hc": 8, "h\u03b5": 8, "real_norm_l": 8, "\u03b5k_po": 8, "o": 8, "normedgroup": 8, "isbigowith": 8, "isbigowith_iff": 8, "isbigo_iff_isbigowith": 8, "islittleo_iff_forall_isbigowith": 8, "hasfderivat": 8, "fderiv": 8, "fr\u00e9chet": 8, "hff": 8, "iter": 8, "multilinear": 8, "with_top": 8, "infti": 8, "cont_diff": 8, "iteratedfderiv": 8, "withtop": 8, "contdiff": 8, "contdiff_iff_continuous_differenti": 8, "stricter": 8, "hasstrictfderivat": 8, "\ud835\udd42": 8, "isrorc": 8, "contdiffat": 8, "localinvers": 8, "eventually_left_invers": 8, "eventually_right_invers": 8, "to_localinvers": 8, "hasfderivwithinat": [8, 9], "hasfderivatfilt": 8, "measuretheori": 9, "intervalintegr": 9, "integral_id": 9, "integral_one_div": 9, "differenti": [9, 11], "integral_hasstrictderivat_right": 9, "stronglymeasurableatfilt": 9, "volum": 9, "integral_eq_sub_of_hasderivat": 9, "convolut": 9, "bochner": 9, "lebesgu": 9, "measurablespac": 9, "countabl": 9, "encod": 9, "measurableset": 9, "compl": 9, "iunion": 9, "iinter": 9, "measure_eq_iinf": 9, "measure_iunion_l": 9, "hmea": 9, "hdi": 9, "pairwis": 9, "m_iunion": 9, "\u1d50": 9, "integral_add": 9, "ennreal": 9, "toreal": 9, "send": 9, "to_real": 9, "set_integral_const": 9, "domin": 9, "converg": [9, 11], "aestronglymeasur": 9, "hbound": 9, "hlim": 9, "tendsto_integral_of_dominated_converg": 9, "fubini": 9, "sigmafinit": 9, "\u03bd": 9, "integral_prod": 9, "bilinear": 9, "formula": 9, "borelspac": 9, "isaddhaarmeasur": 9, "invari": 9, "mass": 9, "compact": 9, "h_inj": 9, "det": 9, "integral_image_eq_integral_abs_det_fderiv_smul": 9, "overview": 11, "schr\u00f6der": 11, "bernstein": 11, "irrat": 11}, "objects": {}, "objtypes": {}, "objnames": {}, "titleterms": {"introduct": 0, "get": 0, "start": 0, "overview": 0, "basic": [1, 6], "calcul": 1, "prove": 1, "ident": 1, "algebra": [1, 5], "structur": [1, 5], "us": 1, "theorem": [1, 3], "lemma": 1, "more": 1, "exampl": 1, "appli": 1, "rw": 1, "fact": 1, "about": 1, "logic": 2, "implic": 2, "univers": 2, "quantifi": 2, "The": [2, 3], "existenti": 2, "negat": 2, "conjunct": 2, "bi": 2, "disjunct": 2, "sequenc": 2, "converg": [2, 7], "set": [3, 7], "function": [3, 7], "schr\u00f6der": 3, "bernstein": 3, "elementari": [4, 8, 9], "number": 4, "theori": [4, 9], "irrat": 4, "root": 4, "induct": 4, "recurs": 4, "infinit": 4, "mani": 4, "prime": 4, "defin": 5, "build": 5, "gaussian": 5, "integ": 5, "hierarchi": 6, "morphism": 6, "sub": 6, "object": 6, "topolog": 7, "filter": 7, "metric": 7, "space": [7, 8], "continu": [7, 8], "ball": 7, "open": 7, "close": 7, "compact": 7, "uniformli": 7, "complet": 7, "fundament": 7, "separ": 7, "countabl": 7, "differenti": 8, "calculu": 8, "norm": 8, "linear": 8, "map": 8, "asymptot": 8, "comparison": 8, "integr": 9, "measur": 9, "index": 10, "mathemat": 11, "lean": 11}, "envversion": {"sphinx.domains.c": 2, "sphinx.domains.changeset": 1, "sphinx.domains.citation": 1, "sphinx.domains.cpp": 6, "sphinx.domains.index": 1, "sphinx.domains.javascript": 2, "sphinx.domains.math": 2, "sphinx.domains.python": 3, "sphinx.domains.rst": 2, "sphinx.domains.std": 2, "sphinx": 56}}) + Search.setIndex({"docnames": ["C01_Introduction", "C02_Basics", "C03_Logic", "C04_Sets_and_Functions", "C05_Elementary_Number_Theory", "C06_Structures", "C07_Hierarchies", "C08_Topology", "C09_Differential_Calculus", "C10_Integration_and_Measure_Theory", "genindex", "index"], "filenames": ["C01_Introduction.rst", "C02_Basics.rst", "C03_Logic.rst", "C04_Sets_and_Functions.rst", "C05_Elementary_Number_Theory.rst", "C06_Structures.rst", "C07_Hierarchies.rst", "C08_Topology.rst", "C09_Differential_Calculus.rst", "C10_Integration_and_Measure_Theory.rst", "genindex.rst", "index.rst"], "titles": ["1. Introduction", "2. Basics", "3. Logic", "4. Sets and Functions", "5. Elementary Number Theory", "6. Structures", "7. Hierarchies", "8. Topology", "9. Differential Calculus", "10. Integration and Measure Theory", "Index", "Mathematics in Lean"], "terms": {"The": [0, 1, 4, 5, 6, 7, 8, 9, 11], "goal": [0, 1, 2, 3, 4, 5, 7], "thi": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "book": [0, 2, 7], "teach": 0, "you": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "formal": [0, 1, 2, 3, 4, 5, 6, 7, 8], "mathemat": [0, 1, 2, 3, 4, 5, 6, 7], "us": [0, 2, 3, 4, 5, 6, 7, 8, 9, 11], "lean": [0, 1, 2, 3, 4, 5, 6, 7, 8], "4": [0, 1, 2, 4, 5, 7, 8], "interact": [0, 5, 6, 9], "proof": [0, 1, 2, 3, 4, 5, 6, 7, 8], "assist": [0, 2, 5], "It": [0, 1, 2, 3, 4, 5, 6, 7, 8], "assum": [0, 1, 2, 3, 4, 6, 7], "know": [0, 1, 2, 3, 4, 5, 6, 7, 8], "some": [0, 1, 2, 3, 4, 5, 6, 7, 8], "doe": [0, 1, 2, 3, 4, 5, 6, 7, 8], "requir": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "much": [0, 2, 4, 6, 7, 8], "although": [0, 3, 4, 5, 6, 7], "we": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "cover": [0, 1, 3, 6, 7, 8], "exampl": [0, 2, 3, 4, 5, 6, 7, 8, 9, 11], "rang": [0, 2, 3, 4, 7], "from": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "number": [0, 1, 2, 3, 5, 6, 7, 8, 11], "theori": [0, 1, 2, 3, 6, 7, 8, 11], "measur": [0, 5, 7, 8, 11], "analysi": [0, 5, 8], "focu": [0, 1, 7, 9], "elementari": [0, 3, 5, 7, 11], "aspect": [0, 5], "those": [0, 1, 2, 3, 5, 6, 7, 8], "field": [0, 1, 5, 6, 8], "hope": 0, "thei": [0, 1, 2, 3, 4, 5, 6, 7, 8], "ar": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "familiar": [0, 1, 4, 5, 7, 8], "can": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "pick": [0, 6], "them": [0, 1, 2, 3, 4, 5, 6, 7], "up": [0, 2, 3, 4, 5, 6, 7], "go": [0, 1, 2, 3, 4, 6, 7], "also": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "don": [0, 1, 2, 3, 4, 5, 6, 7, 9], "t": [0, 1, 2, 3, 4, 5, 6, 7, 9], "presuppos": 0, "ani": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "background": 0, "method": [0, 2, 3, 4, 5], "seen": [0, 1, 2, 4, 5, 6, 7], "kind": [0, 1, 6, 7], "comput": [0, 3, 4, 5, 8, 9], "program": [0, 1], "write": [0, 1, 2, 4, 5, 6, 7, 8, 9], "definit": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "theorem": [0, 2, 4, 5, 7, 8, 9, 11], "regiment": 0, "languag": [0, 1, 3], "like": [0, 1, 2, 3, 4, 5, 6, 7], "understand": [0, 2, 3, 4, 5, 6, 7], "In": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "return": [0, 2, 3, 4, 5, 7], "provid": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "feedback": 0, "inform": [0, 1, 2, 3, 5, 6, 7], "interpret": [0, 1, 4, 5, 7], "express": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "guarante": [0, 3, 5], "well": [0, 1, 2, 3, 4, 5, 6, 7], "form": [0, 1, 2, 3, 4, 5, 6, 7, 9], "ultim": 0, "certifi": 0, "correct": [0, 1], "our": [0, 1, 2, 3, 4, 5, 6, 7, 9], "learn": [0, 1, 2, 4, 5], "more": [0, 2, 3, 4, 5, 6, 7, 8, 11], "about": [0, 2, 3, 4, 5, 6, 7, 8, 11], "project": [0, 4, 5, 7], "page": [0, 1, 4], "commun": [0, 4], "web": [0, 1, 4], "tutori": 0, "base": [0, 2, 3, 4, 6, 7, 8], "s": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "larg": [0, 6, 7], "ever": [0, 7], "grow": [0, 6], "librari": [0, 1, 2, 3, 4, 5, 7, 8], "mathlib": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "strongli": 0, "recommend": [0, 1, 3], "join": [0, 1, 5], "zulip": [0, 4], "onlin": 0, "chat": 0, "group": [0, 1, 2, 3, 5, 6, 7, 8], "haven": [0, 2, 6, 7], "alreadi": [0, 1, 2, 3, 4, 5, 6, 7], "ll": [0, 2, 4, 6, 7], "find": [0, 1, 2, 4, 5, 6, 7], "live": [0, 5], "welcom": [0, 1], "enthusiast": 0, "happi": 0, "answer": [0, 5, 7], "question": [0, 4, 6, 7, 9], "offer": [0, 2, 5, 7], "moral": [0, 5], "support": [0, 1, 2, 3, 4, 5, 6, 7], "read": [0, 1, 4, 6, 7], "pdf": 0, "html": 0, "version": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "design": [0, 1, 2, 3, 5, 7], "run": 0, "insid": [0, 1, 2, 3], "vs": [0, 1, 2, 3, 5], "code": [0, 1, 2, 3, 5, 6], "editor": [0, 1], "To": [0, 1, 2, 3, 4, 5, 6, 7], "instal": [0, 6], "follow": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "instruct": [0, 1, 7], "isn": [0, 2, 3, 4, 6], "enough": [0, 1, 2, 3, 4, 6, 7], "just": [0, 1, 2, 3, 4, 5, 6, 7], "extens": [0, 1, 6, 7, 8], "vscode": 0, "make": [0, 1, 2, 3, 4, 5, 6, 7, 8], "sure": [0, 1, 2, 3, 5, 6], "complet": [0, 1, 2, 3, 4, 6, 8], "step": [0, 1, 2, 3, 4, 5, 6], "so": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "elan": 0, "have": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "git": 0, "termin": 0, "navig": 0, "folder": 0, "where": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "want": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "put": [0, 1, 2, 3, 4, 5, 6, 7], "copi": [0, 3, 4, 6, 7], "repositori": [0, 1], "type": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "clone": 0, "github": [0, 1], "com": 0, "leanprov": 0, "mathematics_in_lean": 0, "fetch": 0, "execut": 0, "lake": 0, "ex": [0, 2], "cach": 0, "compil": 0, "open": [0, 1, 2, 3, 4, 5, 8, 9], "choos": [0, 2, 3, 4, 5, 6, 7], "file": [0, 1, 4, 5, 6, 7], "menu": [0, 1], "Be": [0, 1, 3], "other": [0, 1, 2, 3, 4, 5, 6, 7], "each": [0, 1, 2, 3, 4, 5, 6, 7, 8], "section": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "ha": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "an": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "associ": [0, 1, 2, 4, 5, 6, 7, 9], "exercis": [0, 1, 2, 3, 5, 6, 7, 8], "mil": 0, "organ": 0, "chapter": [0, 1, 2, 3, 4, 5, 6, 7, 8], "experi": [0, 1, 7], "do": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "leav": [0, 1, 2, 3, 5, 6], "origin": [0, 1, 5], "intact": 0, "easier": [0, 1, 3, 4, 6, 7], "updat": 0, "chang": [0, 1, 2, 4, 5, 7, 9], "see": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "below": [0, 2, 3, 4, 5, 6, 7, 8, 9], "call": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "my_fil": 0, "whatev": [0, 2, 4], "creat": [0, 1, 6], "your": [0, 1, 2, 3, 5, 6, 7], "own": [0, 1, 4, 5, 6], "At": [0, 1, 2, 4, 5, 6], "point": [0, 1, 2, 3, 5, 6, 7, 8, 9], "textbook": 0, "side": [0, 1, 2, 3, 4, 5, 6, 7, 8], "panel": 0, "ctrl": [0, 1, 2, 4, 5], "shift": [0, 1, 6, 7], "p": [0, 1, 2, 3, 4, 5, 6, 7, 9], "document": [0, 1, 3, 4, 6], "view": [0, 5, 6, 7], "bar": [0, 1, 2], "appear": [0, 1, 2, 5, 6, 7], "press": 0, "select": [0, 7], "soon": [0, 2, 6, 7], "highlight": 0, "window": [0, 1, 2, 5], "click": [0, 1, 3, 4, 5, 6], "current": [0, 1, 2, 6], "altern": [0, 2, 3, 4, 5, 6, 7], "cloud": 0, "gitpod": 0, "how": [0, 1, 2, 3, 4, 5, 6, 7, 9], "still": [0, 1, 2, 3, 4, 5, 6, 7, 9], "work": [0, 1, 2, 3, 4, 5, 6, 7, 8], "describ": [0, 1, 2, 3, 4, 5, 6, 7], "abov": [0, 1, 2, 3, 4, 5, 6, 7, 9], "progress": [0, 1, 5], "pull": [0, 7], "content": [0, 1, 4, 7], "which": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "why": [0, 2, 4, 6, 7], "suggest": [0, 2, 4, 5, 7], "intend": [0, 1, 2, 5], "while": [0, 1, 2, 6, 7], "contain": [0, 2, 3, 4, 5, 6, 7, 8, 9], "explan": [0, 7], "hint": [0, 1, 2, 9], "text": [0, 3, 5, 7], "often": [0, 1, 2, 3, 4, 5, 6, 7], "includ": [0, 1, 2, 3, 4, 6, 7, 8], "one": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "eval": 0, "hello": 0, "world": 0, "should": [0, 1, 2, 3, 4, 5, 6, 7, 8], "abl": [0, 1, 2, 3, 4, 5, 6, 8], "correspond": [0, 1, 2, 3, 4, 5, 6, 7, 8], "If": [0, 1, 2, 3, 4, 5, 6, 7], "line": [0, 1, 2, 3, 4, 6], "show": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "hover": [0, 1, 2, 3, 4, 5], "cursor": [0, 1, 2], "over": [0, 1, 2, 3, 4, 5, 6, 7, 8], "command": [0, 1, 2, 3, 4, 5, 6], "respons": [0, 1], "pop": 0, "encourag": [0, 1, 2, 3, 4, 5], "edit": 0, "try": [0, 1, 2, 3, 4, 5, 6, 7], "moreov": [0, 1, 4, 5, 7], "lot": [0, 3, 5, 6, 7], "challeng": [0, 1, 2, 3, 5, 8], "rush": 0, "past": [0, 1], "through": [0, 1, 3, 4, 5, 6, 7], "central": [0, 4], "all": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "when": [0, 1, 2, 3, 4, 5, 6, 7, 8], "feel": [0, 1, 2, 6, 7], "comfort": [0, 2], "master": [0, 1, 4], "relev": [0, 1, 2, 4, 5, 6, 7], "skill": [0, 1, 2, 3, 4], "free": [0, 1, 7], "move": [0, 1, 2, 6, 7], "alwai": [0, 1, 2, 3, 5, 6], "compar": [0, 5, 6, 7], "solut": [0, 1, 4, 6], "ones": [0, 1, 2, 3, 5, 9], "simpli": [0, 1, 2, 3, 4, 5, 6, 7], "tool": [0, 1, 2, 5, 6], "build": [0, 2, 4, 6, 7, 11], "complex": [0, 1, 2, 4, 5, 8, 9], "known": [0, 1, 2, 3, 4, 5, 6, 7, 8], "depend": [0, 2, 3, 4, 5, 6, 7], "everi": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "check": [0, 1, 2, 3, 4, 5, 6, 7], "print": [0, 3, 4, 5, 9], "\u2115": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "These": [0, 1, 2, 3, 4, 5, 8, 9], "object": [0, 1, 2, 3, 4, 5, 11], "2": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "def": [0, 2, 3, 4, 5, 6, 7], "f": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "x": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "3": [0, 1, 2, 3, 4, 5, 6, 7], "prop": [0, 2, 3, 4, 5, 6, 7, 9], "statement": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "fermatlasttheorem": 0, "y": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "z": [0, 1, 2, 5, 6, 7, 8, 9], "n": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "0": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "itself": [0, 2, 3, 5, 6, 7, 8], "Such": [0, 1, 2, 6], "proposit": [0, 2, 3, 4, 5], "easi": [0, 4, 5, 6, 7], "rfl": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "hard": [0, 1, 3, 5, 6], "sorri": [0, 1, 2, 3, 4, 5, 6, 7, 8], "manag": [0, 1, 4, 5, 7], "construct": [0, 2, 3, 4, 5, 6, 7], "accept": [0, 1, 2, 7], "term": [0, 1, 2, 3, 4, 5, 7], "done": [0, 2, 3, 4, 6, 7], "someth": [0, 1, 2, 4, 6, 7], "veri": [0, 2, 4, 6, 7, 9], "impress": 0, "cheat": [0, 1], "now": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "game": [0, 6], "left": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "rule": [0, 2, 4, 5, 6, 7], "complementari": 0, "companion": [0, 1], "prove": [0, 2, 3, 4, 5, 6, 7, 8, 9, 11], "thorough": 0, "underli": [0, 1, 5, 6], "logic": [0, 1, 3, 4, 5, 11], "framework": 0, "core": [0, 4, 5], "syntax": [0, 1, 4, 6], "peopl": [0, 1], "who": [0, 7], "prefer": [0, 1, 3], "user": [0, 2, 6], "manual": [0, 3, 4], "befor": [0, 1, 2, 3, 4, 5, 6], "new": [0, 1, 2, 3, 4, 5, 6, 7], "dishwash": 0, "person": 0, "hit": [0, 1], "button": 0, "figur": [0, 1, 2, 5], "out": [0, 1, 2, 3, 4, 5, 6, 7], "activ": 0, "potscrubb": 0, "featur": [0, 2, 4], "later": [0, 1, 2, 4, 5, 6, 7], "sens": [0, 2, 3, 4, 5, 6, 7, 8], "here": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "refer": [0, 1, 2, 4, 5, 6, 7, 8], "back": [0, 1, 2, 3, 5, 6, 7], "necessari": [0, 2, 4, 5], "anoth": [0, 1, 2, 3, 4, 5, 6, 7], "thing": [0, 1, 2, 3, 4, 5, 6, 7], "distinguish": [0, 5, 6, 7, 8], "place": [0, 1, 2, 5, 7], "greater": [0, 1, 2, 3, 4, 7], "emphasi": [0, 6], "tactic": [0, 1, 2, 3, 4, 5, 6, 7, 8], "given": [0, 1, 2, 3, 4, 5, 6, 7], "two": [0, 1, 2, 3, 4, 5, 6, 7, 9], "wai": [0, 1, 2, 3, 4, 5, 6, 7, 9], "down": [0, 3, 4, 6, 7], "themselv": [0, 4, 5], "suitabl": [0, 1, 2, 5, 7], "descript": [0, 1, 2, 4, 7], "thereof": 0, "For": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "repres": [0, 1, 2, 3, 4, 5, 6, 8], "fact": [0, 2, 3, 4, 5, 6, 7, 8, 9, 11], "even": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "m": [0, 1, 2, 4, 6, 7, 8], "nat": [0, 1, 2, 3, 4, 5, 7], "fun": [0, 2, 3, 4, 5, 6, 7, 8, 9], "k": [0, 2, 4, 5, 7, 8], "hk": [0, 8], "hmn": 0, "rw": [0, 2, 3, 4, 5, 6, 7, 11], "mul_add": [0, 1, 4, 6], "l": [0, 1, 8, 9], "_": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "compress": [0, 1, 7], "singl": [0, 1, 2, 3, 4, 5, 6, 8], "instead": [0, 1, 2, 3, 4, 5, 6, 7], "style": [0, 1], "same": [0, 1, 2, 3, 4, 5, 6, 7], "comment": [0, 4], "henc": [0, 2, 3, 4, 5, 6, 7, 8], "ignor": [0, 7], "sai": [0, 1, 2, 3, 4, 5, 6, 7, 9], "natur": [0, 1, 2, 3, 4, 5, 6, 7, 8], "rintro": [0, 2, 3, 4, 5, 7], "need": [0, 1, 2, 3, 4, 5, 6, 7], "twice": [0, 1, 7], "let": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "substitut": [0, 2], "obviou": [0, 4, 5, 6], "ring": [0, 1, 2, 3, 4, 5, 6], "As": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "enter": [0, 1, 2, 3, 7], "displai": [0, 1, 2, 6], "state": [0, 1, 2, 3, 4, 6, 7, 8], "separ": [0, 1, 2, 4, 5], "tell": [0, 2, 3, 4, 5, 6], "what": [0, 1, 2, 3, 4, 5, 6, 7], "establish": [0, 1, 2, 3, 4, 5], "task": [0, 2, 4, 5, 6, 7], "remain": [0, 1, 2, 3, 5, 6, 7], "replai": 0, "sinc": [0, 1, 2, 3, 4, 5, 6, 7], "continu": [0, 1, 4, 5, 6, 9], "first": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "introduc": [0, 1, 2, 3, 4, 7, 9], "could": [0, 1, 2, 4, 5, 6, 7], "renam": 0, "decompos": [0, 3, 5], "hypothesi": [0, 1, 2, 3, 4], "assumpt": [0, 1, 2, 3, 4, 5, 7, 8, 9], "second": [0, 1, 2, 3, 4, 5, 6, 7, 9], "declar": [0, 1, 4, 5, 6], "next": [0, 1, 2, 3, 4, 5, 6, 7, 8], "rewrit": [0, 1, 2, 3, 4, 5, 6, 7], "replac": [0, 1, 2, 3, 4, 6], "solv": [0, 1, 2, 3, 4, 5, 6, 7], "result": [0, 1, 2, 3, 4, 5, 6, 7], "abil": 0, "small": [0, 4, 5, 7], "increment": [0, 1], "extrem": [0, 6, 7], "power": [0, 1, 2, 3, 4, 5, 6], "reason": [0, 1, 2, 4, 5, 6, 7], "quicker": 0, "than": [0, 1, 2, 3, 4, 5, 6, 7, 8], "There": [0, 1, 2, 3, 4, 6, 7, 8, 9], "sharp": 0, "distinct": [0, 2, 3, 4, 5, 7], "between": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "insert": [0, 2, 4, 5, 7, 8], "did": [0, 2, 6, 7], "phrase": [0, 1, 2, 4, 5], "mul_left_comm": [0, 4], "convers": [0, 2, 4, 7], "short": [0, 1, 2, 3, 4, 5], "middl": [0, 1, 2, 7], "That": [0, 4, 5, 6], "said": [0, 2, 4, 5], "reduc": [0, 2, 3, 4, 5], "liner": 0, "carri": [0, 1, 2, 3, 4, 5, 6, 7, 9], "But": [0, 1, 2, 3, 4, 5, 6, 7], "substanti": 0, "autom": [0, 1, 5], "justifi": [0, 1, 2, 7], "longer": [0, 4, 5], "calcul": [0, 2, 4, 5, 11], "bigger": [0, 3, 8], "inferenti": 0, "invok": [0, 1, 7], "simplifi": [0, 2, 3, 4, 5, 7, 9], "specif": [0, 1, 3, 4, 5, 6], "pariti": [0, 4], "automat": [0, 1, 2, 3, 4, 5, 6, 7, 8], "intro": [0, 1, 2, 3, 4, 5, 6, 7], "simp": [0, 2, 3, 4, 5, 6, 7, 8], "parity_simp": 0, "big": [0, 5, 7, 8], "differ": [0, 1, 2, 3, 4, 5, 6, 7, 8], "onli": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "its": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "built": [0, 2, 6], "wherea": [0, 1, 3, 5, 7], "top": [0, 6, 7, 8], "meant": [0, 2, 6], "rather": [0, 1, 2, 4, 5, 6, 7], "think": [0, 1, 2, 3, 4, 5, 6, 7, 8], "basic": [0, 2, 4, 5, 7, 9, 11], "entri": [0, 5], "brows": [0, 1, 4], "frustrat": [0, 6], "curv": 0, "steep": 0, "newcom": 0, "avail": [0, 1, 4, 5, 6], "round": [0, 1, 5], "clock": 0, "doubt": 0, "too": [0, 1, 3, 5, 6, 7], "contribut": [0, 3], "develop": [0, 1, 4, 9], "mission": 0, "dive": 0, "come": [0, 1, 2, 3, 4, 5, 6, 7], "forewarn": 0, "fundament": [0, 4, 5, 6, 9], "life": [0, 2], "mai": [0, 1, 2, 3, 5, 6, 7, 8], "never": [0, 6], "acknowledg": 0, "grate": [0, 5], "gabriel": 0, "ebner": 0, "set": [0, 1, 2, 4, 5, 6, 8, 9, 11], "infrastructur": 0, "scott": 0, "morrison": 0, "mario": 0, "carneiro": 0, "help": [0, 1, 2, 3, 4, 5, 6, 7], "port": 0, "julian": 0, "berman": 0, "alex": 0, "best": 0, "bulwi": 0, "cha": 0, "bryan": 0, "gin": 0, "ge": [0, 2, 5], "chen": 0, "johan": 0, "commelin": 0, "mathieu": 0, "guai": 0, "paquet": 0, "k\u00fclshammer": 0, "giovanni": 0, "mascellani": 0, "hunter": 0, "monro": 0, "pietro": 0, "monticon": 0, "oliv": 0, "nash": 0, "bartosz": 0, "piotrowski": 0, "guilherm": 0, "silva": 0, "been": [0, 1, 2, 4, 5, 6, 8], "partial": [0, 1, 2, 3, 5, 6], "hoskinson": 0, "center": [0, 7], "nut": 1, "bolt": 1, "gener": [1, 2, 3, 4, 5, 6, 7, 8, 9], "without": [1, 2, 4, 5, 6, 7, 8], "net": 1, "hand": [1, 2, 3, 4, 5, 6, 7], "equal": [1, 2, 3, 4, 5, 6, 7, 9], "right": [1, 2, 3, 4, 5, 6, 7, 8], "tantamount": [1, 3], "name": [1, 2, 3, 4, 5, 6, 7, 8], "b": [1, 2, 3, 4, 5, 6, 7, 8, 9], "c": [1, 2, 4, 5, 6, 7, 8, 9], "real": [1, 2, 3, 4, 5, 6, 7, 8, 9], "mul_assoc": [1, 2, 4, 5, 6], "mul_comm": [1, 2, 4, 5, 6], "elimin": 1, "explicitli": [1, 2, 3, 5, 6, 7, 8], "purpos": [1, 2, 3, 4, 5, 6, 7], "illustr": [1, 2, 3, 4, 5], "multipl": [1, 2, 3, 4, 5, 6, 8], "written": [1, 2, 3, 4, 5, 6, 7, 8], "howev": [1, 2, 5, 6, 7, 8], "good": [1, 2, 3, 4, 5, 6, 7], "mind": [1, 2, 5, 6], "notat": [1, 2, 3, 4, 5, 6, 7, 8, 9], "convent": [1, 5, 9], "parenthes": [1, 2, 3, 4], "import": [1, 2, 3, 4, 5, 6, 7, 9], "data": [1, 2, 4, 5, 6, 7], "\u211d": [1, 2, 3, 5, 6, 7, 8, 9], "begin": [1, 2, 3, 4, 5, 6], "sake": [1, 4], "breviti": [1, 5], "suppress": 1, "repeat": [1, 4, 5, 6], "happen": [1, 6, 7], "charact": [1, 3, 6], "r": [1, 2, 4, 5, 6, 7], "symbol": [1, 2, 5, 6], "doesn": [1, 2, 7], "until": [1, 2, 4, 5, 6, 7], "space": [1, 2, 3, 5, 6, 9, 11], "tab": [1, 3, 4], "kei": [1, 4, 5, 7], "curiou": [1, 6], "abbrevi": [1, 2, 3, 5], "get": [1, 2, 3, 4, 6, 7, 8, 11], "access": [1, 3, 5, 6, 7, 9], "keyboard": 1, "easili": [1, 4, 5, 6], "backslash": [1, 3], "lead": [1, 2, 4, 5, 6, 7], "lean4": 1, "input": [1, 3, 7], "leader": 1, "report": 1, "infoview": 1, "A": [1, 2, 3, 4, 5, 6, 7, 8], "typic": 1, "might": [1, 2, 3, 4, 5], "look": [1, 2, 3, 4, 6, 7], "1": [1, 2, 3, 4, 5, 6, 7, 8, 9], "h\u2081": [1, 2, 3, 4], "prime": [1, 2, 3, 5, 6, 11], "h\u2082": [1, 3, 4], "h\u2083": [1, 3], "denot": [1, 3, 4, 6, 7], "context": [1, 2, 4, 5, 6, 7, 8, 9], "plai": [1, 3, 4, 6, 7], "three": [1, 2, 4, 5, 7], "label": [1, 2], "everyth": [1, 2, 6, 7], "identifi": [1, 2, 4], "subscript": 1, "h": [1, 2, 3, 4, 5, 6, 7, 8, 9], "legal": 1, "would": [1, 2, 3, 4, 5, 6, 7, 8], "h1": [1, 3, 4, 5], "h2": [1, 3, 5], "h3": 1, "foo": [1, 3, 5], "baz": 1, "last": [1, 2, 3, 4, 5, 6, 7], "sometim": [1, 2, 3, 4, 5, 6, 7], "target": [1, 6, 7, 9], "combin": [1, 2, 5, 6, 7], "practic": [1, 2, 3, 6, 7], "mean": [1, 2, 3, 4, 5, 6, 7, 8, 9], "usual": [1, 2, 3, 4, 5, 7, 9], "clear": [1, 2, 4, 5, 6], "case": [1, 2, 3, 4, 5, 6, 7, 9], "With": [1, 3, 4, 6, 7], "arrow": [1, 2, 6, 7], "revers": [1, 2, 3, 5, 7], "note": [1, 2, 4, 5, 6, 7, 9], "noth": [1, 2, 3, 4, 5, 6], "argument": [1, 2, 3, 4, 5, 6, 7], "tri": [1, 2, 4, 6], "match": [1, 2, 5], "pattern": [1, 2, 3, 5, 6], "local": [1, 2, 6, 7, 8], "d": [1, 2, 4, 5, 8], "e": [1, 2, 3, 4, 5, 6, 7, 8, 9], "sub_self": [1, 2], "hyp": 1, "list": [1, 2, 3, 4, 5], "comma": 1, "squar": [1, 2, 4, 5, 6], "bracket": [1, 2, 5, 6], "after": [1, 2, 4, 6, 7, 8], "trick": [1, 2, 4, 6, 8], "variabl": [1, 2, 3, 4, 5, 6, 7, 8, 9], "onc": [1, 2, 3, 4, 5, 6, 7, 9], "outsid": [1, 4], "inspect": 1, "reveal": 1, "inde": [1, 5, 6, 7, 8], "delimit": 1, "scope": [1, 2, 3, 5], "end": [1, 2, 3, 4, 5, 6, 7, 8], "block": [1, 4], "final": [1, 2, 3, 5, 7, 9], "recal": [1, 2, 4, 5, 7, 9], "introduct": [1, 2, 7, 11], "determin": [1, 5, 7], "both": [1, 2, 3, 4, 5, 6, 7, 8], "expect": [1, 2, 3, 4, 5, 6, 7], "rais": [1, 4], "error": [1, 2, 3, 6], "explain": [1, 2, 3, 4, 5, 6, 7, 9], "output": 1, "meanwhil": [1, 4], "take": [1, 2, 3, 4, 5, 6, 7, 8, 9], "two_mul": 1, "add_mul": [1, 6], "distribut": [1, 4, 5, 6], "addit": [1, 2, 4, 5, 6, 7, 8, 9], "add_assoc": [1, 4, 5, 6], "precis": [1, 3, 7, 8], "possibl": [1, 2, 3, 4, 5, 7], "calc": [1, 2, 3, 5, 7], "keyword": [1, 2, 4, 5], "notic": [1, 2, 3, 4, 5, 7], "finicki": 1, "underscor": [1, 2, 3], "justif": [1, 2], "format": 1, "indic": [1, 2, 3, 5, 6], "indent": 1, "One": [1, 2, 3, 4, 5, 6, 7], "outlin": [1, 2, 4, 7], "modulo": [1, 4, 5], "individu": 1, "pure": [1, 7], "littl": [1, 2, 7, 8], "underneath": [1, 3], "pow_two": [1, 4], "mul_sub": 1, "add_sub": 1, "sub_sub": 1, "add_zero": [1, 5, 6], "perform": [1, 2, 3], "exact": [1, 2, 3, 4, 5, 7], "becaus": [1, 2, 3, 4, 5, 6, 7, 8], "exactli": [1, 2, 3, 5, 6, 7], "close": [1, 2, 3, 6, 8, 9], "bit": [1, 2, 4, 6, 7], "commut": [1, 2, 3, 4, 5, 6, 8], "long": [1, 2, 3, 5, 6, 8], "axiom": [1, 2, 3, 5, 6, 7, 9], "indirectli": 1, "similar": [1, 2, 3, 5, 6, 7], "common": [1, 2, 3, 4, 5, 7], "variat": [1, 3, 4, 5, 7, 8], "nth_rewrit": 1, "allow": [1, 2, 3, 4, 5, 6, 7, 8, 9], "particular": [1, 2, 5, 6, 7], "instanc": [1, 2, 3, 4, 5, 6, 7, 8], "enumer": [1, 2], "start": [1, 2, 3, 4, 6, 7, 8, 9, 11], "occurr": 1, "nth_rw": 1, "consist": [1, 3, 5, 6, 7, 8], "collect": [1, 2, 3, 5, 7, 9], "oper": [1, 2, 3, 4, 5, 6, 7, 8], "time": [1, 4, 5, 6, 7, 8, 9], "constant": [1, 2, 9], "mapsto": [1, 5], "abelian": [1, 5, 6], "negat": [1, 5, 11], "invers": [1, 3, 5, 6, 8, 9], "add_comm": [1, 4, 5, 6], "zero_add": [1, 4, 5, 6], "add_left_neg": [1, 5], "mul_on": [1, 5, 6], "one_mul": [1, 2, 5, 6], "being": [1, 3, 5, 7, 8], "suffic": [1, 2, 3, 7], "give": [1, 2, 3, 4, 6, 7, 9], "element": [1, 2, 3, 4, 5, 6, 7, 8, 9], "concret": [1, 2, 4, 5, 6, 7], "integ": [1, 2, 4, 6, 11], "abstract": [1, 2, 5, 6, 7], "character": [1, 3, 4, 7, 8], "axiomat": [1, 2, 3, 5], "train": [1, 6], "recogn": [1, 2, 4, 5, 6, 7], "appropri": [1, 2, 3, 5, 6], "\u2124": [1, 4, 5, 6], "ration": [1, 2, 4, 7], "\u211a": [1, 4, 7], "\u2102": [1, 5, 8], "extend": [1, 3, 4, 5, 6, 7, 9], "order": [1, 2, 3, 4, 5, 6, 7, 8], "Not": [1, 5, 7], "properti": [1, 2, 3, 4, 5, 6, 7, 8, 9], "hold": [1, 2, 3, 4, 5, 7, 9], "arbitrari": [1, 2, 3, 4, 5], "taken": [1, 2], "cours": [1, 2, 4, 6, 7, 8, 9], "linear": [1, 2, 5, 7], "matric": [1, 5], "fail": [1, 2, 3, 4, 5, 6, 7, 9], "commr": [1, 2, 5], "unchang": [1, 2], "linarith": [1, 2, 4, 5], "permiss": 1, "strike": [1, 2], "balanc": 1, "concis": [1, 5], "readabl": [1, 2, 3, 4, 7], "strengthen": [1, 2, 4], "deriv": [1, 2, 4, 8, 9], "most": [1, 2, 3, 4, 5, 6, 7, 9], "organiz": 1, "mechan": [1, 2, 5], "namespac": [1, 2, 3, 4, 5, 7], "full": [1, 3, 4, 5, 6, 7], "shorter": [1, 3, 4, 7], "avoid": [1, 3, 4, 5, 6, 8], "due": [1, 3, 6], "clash": 1, "myre": 1, "add_right_neg": 1, "effect": [1, 3, 6, 7], "temporarili": [1, 2], "reprov": 1, "care": [1, 2, 3, 5], "earlier": 1, "pai": [1, 2, 6, 7], "attent": [1, 2, 4, 6, 7], "curli": [1, 2], "implicit": [1, 2, 5, 6, 7, 8], "moment": [1, 2, 5], "worri": [1, 3, 4, 5], "neg_add_cancel_left": 1, "add_neg_cancel_right": 1, "add_left_cancel": 1, "add_right_cancel": 1, "plan": [1, 6, 7], "brace": 1, "imagin": 1, "situat": [1, 3, 6, 7], "draw": [1, 5, 6], "conclus": [1, 2, 4], "hypothes": [1, 2, 3, 4, 5], "redund": [1, 5, 7, 9], "few": [1, 2, 3, 4, 7], "extra": [1, 2, 3, 5, 6, 7], "oner": 1, "complic": [1, 2, 6], "tediou": [1, 2, 6], "mark": [1, 2, 6, 7], "suppos": [1, 2, 3, 4, 5, 7], "infer": [1, 2, 3, 5, 6], "mul_zero": [1, 5, 6], "serv": [1, 3, 4, 5, 9], "therefor": [1, 4, 5, 7], "promot": 1, "modular": 1, "subproof": 1, "wa": [1, 3], "except": [1, 5], "ad": [1, 2, 3, 4, 5, 6, 7], "variant": [1, 2, 7], "whose": [1, 2, 4, 5, 6, 7, 8], "necessarili": [1, 9], "miss": [1, 3, 4], "piec": [1, 4, 5, 6, 7], "either": [1, 2, 3, 5, 6, 7], "becom": [1, 4, 5, 6, 7], "technic": [1, 5, 6], "strictli": [1, 2, 8], "less": [1, 2, 3, 4, 5, 6, 7], "script": 1, "slightli": [1, 6, 7, 8], "clearer": [1, 3, 5], "human": 1, "reader": [1, 7], "maintain": 1, "evolv": 1, "rememb": [1, 2, 3, 4, 5, 6, 7], "zero_mul": [1, 4, 5, 6], "By": [1, 3, 5, 6], "neg_eq_of_add_eq_zero": 1, "eq_neg_of_add_eq_zero": 1, "neg_zero": 1, "neg_neg": 1, "had": [1, 6], "annot": [1, 3, 4, 5, 6], "third": [1, 2, 3, 5, 7], "specifi": [1, 2, 3, 4, 5, 7, 8, 9], "imposs": 1, "default": [1, 2, 3, 4, 5, 6, 8], "subtract": [1, 4, 5], "provabl": [1, 3, 6, 7], "sub_eq_add_neg": 1, "On": [1, 2, 3, 5, 6, 7, 9], "defin": [1, 2, 3, 4, 6, 7, 8, 9, 11], "reflex": [1, 2], "present": [1, 2, 4, 7], "forc": [1, 2, 3], "unfold": [1, 2, 3, 4, 5, 7], "deal": [1, 2, 3, 4, 5, 7], "equat": [1, 2, 3, 4, 5], "interchang": 1, "self_sub": 1, "effort": [1, 4], "one_add_one_eq_two": 1, "norm_num": [1, 2, 4, 5], "strength": 1, "weaker": [1, 2], "notion": [1, 2, 3, 4, 5, 7, 8, 9], "addgroup": [1, 5], "otherwis": [1, 2, 3, 4, 5], "addcommgroup": 1, "commgroup": 1, "g": [1, 2, 3, 5, 6, 7, 8, 9], "mul_left_inv": [1, 5], "\u00b9": [1, 3, 5, 6, 7], "cocki": 1, "helper": 1, "along": [1, 4, 7], "mul_right_inv": [1, 5], "mul_inv_rev": 1, "non": [1, 3, 6, 7, 8, 9], "abel": 1, "noncomm_r": 1, "seem": [1, 2, 4, 6, 7, 8], "odd": [1, 2, 3, 4], "partli": [1, 6], "histor": 1, "conveni": [1, 2, 3, 5, 6, 7], "great": [1, 5], "sort": [1, 3, 4], "inequ": [1, 2, 6, 7], "le": [1, 5, 6], "whenev": [1, 2, 4, 5], "consid": [1, 2, 3, 4, 5, 6, 7, 8, 9], "le_refl": [1, 2], "le_tran": [1, 2], "detail": [1, 2, 3, 4, 5, 6], "unless": [1, 2, 5], "realli": [1, 2, 3, 4, 6, 7], "insist": [1, 6], "discuss": [1, 2, 4, 5, 6, 7, 8], "implic": [1, 7, 11], "h\u2080": [1, 2, 3, 4, 7], "dot": [1, 7], "option": [1, 2, 4, 5, 6, 7], "within": [1, 2, 7], "visibl": 1, "must": [1, 5, 6, 7], "decreas": [1, 5], "fourth": [1, 2], "mode": [1, 2, 5], "entir": [1, 3, 5, 7, 8], "lt_of_le_of_lt": [1, 2], "lt_of_lt_of_l": 1, "lt_tran": [1, 2], "togeth": [1, 2, 3, 4, 5, 7], "handl": [1, 3, 4, 6], "arithmet": 1, "5": [1, 2, 5, 7, 8], "pass": [1, 5], "exp_le_exp": 1, "mpr": [1, 2, 5, 7], "exp": [1, 3], "applic": [1, 2, 4, 5, 9], "function": [1, 2, 4, 5, 6, 8, 9, 11], "compound": [1, 2, 7], "pars": [1, 3], "exp_lt_exp": 1, "log_le_log": 1, "log": [1, 3, 9], "log_lt_log": 1, "add_le_add": [1, 2], "add_le_add_left": 1, "add_le_add_right": 1, "add_lt_add_of_le_of_lt": 1, "add_lt_add_of_lt_of_l": 1, "add_lt_add_left": 1, "add_lt_add_right": 1, "add_nonneg": [1, 5], "add_po": 1, "add_pos_of_pos_of_nonneg": 1, "exp_po": [1, 3], "bi": [1, 5, 11], "lr": 1, "iff": [1, 3, 7, 8, 9], "connect": [1, 3, 5, 7], "equival": [1, 2, 3, 4, 5, 7, 8, 9], "mp": [1, 2, 3, 4, 7], "forward": [1, 2, 5, 7], "direct": [1, 2, 3, 6, 7, 8], "stand": [1, 2, 5, 7, 8], "modu": 1, "ponen": 1, "respect": [1, 2, 3, 4, 5, 7], "thu": [1, 3, 4, 5, 7], "again": [1, 2, 3, 4, 5, 6, 7], "numer": [1, 4, 5], "constitut": 1, "part": [1, 2, 3, 4, 5, 6, 7, 9], "strategi": [1, 2, 4], "api": 1, "reli": [1, 2, 3, 5, 7], "guess": [1, 2, 3, 4, 5], "cmd": [1, 2], "mac": [1, 2], "a_of_b_of_c": 1, "approxim": 1, "loud": 1, "probabl": [1, 5, 6, 7], "add_l": 1, "choic": [1, 2, 3, 5, 7], "exist": [1, 2, 3, 6, 7], "jump": [1, 4, 5, 7], "nearbi": [1, 4], "sq_nonneg": 1, "delet": [1, 2, 3, 4], "uncom": 1, "previou": [1, 2, 3, 5, 6, 7, 8, 9], "confirm": [1, 2, 3, 4], "finish": [1, 2, 3, 4], "job": 1, "pow_two_nonneg": [1, 2], "tend": [1, 7], "around": [1, 3, 6, 7, 9], "binari": [1, 2, 4, 5, 6], "increas": 1, "worth": [1, 2, 5], "definition": [1, 4, 5, 6, 7], "principl": [1, 2, 3, 4, 6, 8], "favor": [1, 2, 5], "timesav": 1, "clever": 1, "involv": [1, 2, 4, 5, 6, 7], "nice": [1, 2, 4, 6, 7], "idea": [1, 2, 3, 5, 6, 7], "abs_l": [1, 5], "congratul": [1, 2, 4], "min": [1, 2, 7, 9], "uniqu": [1, 2, 3, 4, 5, 7], "min_le_left": 1, "min_le_right": 1, "le_min": 1, "max": [1, 2, 6, 7, 9], "pair": [1, 2, 4, 5, 7], "act": 1, "curri": 1, "logician": 1, "haskel": 1, "bind": [1, 3], "tighter": [1, 3], "infix": [1, 6], "le_antisymm": [1, 2], "usag": 1, "inconsist": 1, "outer": 1, "level": [1, 2, 6], "nest": [1, 2], "bother": [1, 3], "repetit": [1, 6], "foreshadow": 1, "univers": [1, 3, 5, 7, 11], "quantifi": [1, 3, 4, 5, 7, 11], "desir": [1, 3, 6, 7], "implicitli": [1, 2], "mani": [1, 2, 3, 5, 6, 7, 8, 9, 11], "whether": [1, 2, 3, 4, 6, 7], "Of": [1, 2, 4, 6, 7, 8, 9], "interest": [1, 2, 3, 5, 6, 7], "vice": [1, 3], "versa": [1, 3], "word": [1, 2, 3, 4, 5, 7], "switch": [1, 6], "transit": [1, 2, 5, 7], "total": 1, "satisfi": [1, 3, 4, 5, 6, 7, 8], "disjunct": [1, 3, 11], "stick": [1, 2, 7, 8], "split": [1, 2, 3, 4], "aux": [1, 2, 4, 7], "valu": [1, 2, 3, 4, 5, 6, 7, 8, 9], "yield": [1, 2, 3, 4, 5, 7], "made": [1, 2, 3, 5, 7], "manifest": [1, 7], "triangl": [1, 2, 5], "abs_add": [1, 2], "sub_add_cancel": [1, 5], "relat": [1, 2, 3, 5, 6, 7, 8, 9], "divis": [1, 2, 4, 5, 6], "ordinari": [1, 2, 4, 5, 7], "unicod": [1, 3, 6], "obtain": [1, 2, 4, 5, 7, 8], "dvd": 1, "dvd_tran": 1, "dvd_mul_of_dvd_left": 1, "dvd_mul_left": 1, "expon": 1, "expand": [1, 2, 3, 4, 5], "w": [1, 6], "greatest": [1, 5, 7], "divisor": [1, 2, 4, 5], "gcd": [1, 2, 4], "least": [1, 5, 6, 7], "lcm": 1, "analog": [1, 2, 3, 4, 5, 7, 8], "divid": [1, 2, 4, 5], "gcd_zero_right": 1, "gcd_zero_left": 1, "lcm_zero_right": 1, "lcm_zero_left": 1, "dvd_antisymm": 1, "complain": 1, "ambigu": [1, 5], "_root_": [1, 4], "saw": [1, 5, 6, 7], "govern": [1, 5], "class": [1, 4, 5, 6, 7, 8, 9], "\u03b1": [1, 2, 3, 4, 5, 6, 7, 8, 9], "partialord": [1, 2], "adopt": 1, "letter": [1, 5, 8], "\u03b2": [1, 2, 3, 5, 6, 7, 9], "\u03b3": [1, 2, 5, 7], "greek": [1, 4], "especi": [1, 5, 6, 7], "strict": [1, 2], "somewhat": [1, 3, 7], "lt_irrefl": [1, 2], "lt_iff_le_and_n": 1, "lattic": [1, 5, 6, 7], "inf_le_left": [1, 7], "inf_le_right": 1, "le_inf": 1, "le_sup_left": 1, "le_sup_right": 1, "sup_l": 1, "lower": [1, 2, 4], "bound": [1, 2, 3, 4, 5, 7, 8, 9], "upper": [1, 2], "glb": 1, "lub": 1, "infimum": [1, 6, 7, 9], "supremum": [1, 4, 6], "inf": [1, 6, 7], "sup": [1, 4, 7], "further": [1, 7], "matter": [1, 2], "meet": [1, 2, 3, 5], "keep": [1, 5, 6], "dictionari": 1, "subset": [1, 2, 3, 5, 7, 8], "domain": [1, 2, 3, 4, 5, 7], "boolean": 1, "truth": [1, 4], "fals": [1, 2, 3, 4, 6], "true": [1, 2, 3, 6, 7], "posit": [1, 3, 4, 5, 7, 9], "subspac": [1, 6], "vector": [1, 3, 6, 8], "intersect": [1, 3, 5, 6, 7, 9], "sum": [1, 2, 4, 5, 6, 7], "inclus": [1, 3, 7], "topolog": [1, 5, 6, 8, 11], "union": [1, 3, 4, 5, 6, 8, 9], "inf_comm": 1, "inf_assoc": 1, "sup_comm": 1, "sup_assoc": 1, "absorpt": 1, "law": 1, "absorb1": 1, "absorb2": 1, "found": [1, 5, 8], "inf_sup_self": 1, "sup_inf_self": 1, "distriblattic": 1, "inf_sup_left": 1, "inf_sup_right": 1, "sup_inf_left": 1, "sup_inf_right": 1, "shown": [1, 5, 8, 9], "explicit": [1, 2, 5, 6, 7], "nondistribut": 1, "finit": [1, 3, 4, 5, 7, 8, 9], "impli": [1, 2, 3, 4, 5, 7], "larger": [1, 7], "carrier": [1, 5, 6], "compat": [1, 7], "strictorderedr": 1, "mul_po": [1, 4], "mul_nonneg": 1, "coupl": [1, 2, 6, 7], "metric": [1, 5, 8, 11], "equip": [1, 3, 5, 6, 7, 8, 9], "distanc": [1, 2, 7, 8], "dist": [1, 7], "map": [1, 2, 3, 5, 6, 7], "metricspac": [1, 7, 8], "dist_self": 1, "dist_comm": [1, 7], "dist_triangl": [1, 7], "nonneg": [1, 5], "nonneg_of_mul_nonneg_left": 1, "dist_nonneg": [1, 7], "dealt": 2, "simpl": [2, 4, 5, 6, 8], "absolut": 2, "\u03b5": [2, 7, 8], "though": [2, 3, 4, 5], "treat": [2, 3, 5, 6, 7, 8], "appli": [2, 3, 4, 5, 6, 7, 8, 9, 11], "my_lemma": 2, "\u03b4": [2, 7], "hb": [2, 7], "subsequ": [2, 4, 7], "lemma": [2, 4, 5, 6, 7, 8, 9, 11], "mention": [2, 3, 5, 6, 7], "my_lemma2": 2, "stage": [2, 5, 6], "my_lemma3": 2, "epo": 2, "ele1": 2, "xlt": 2, "ylt": 2, "essenti": [2, 3, 5, 7], "colon": 2, "off": [2, 3, 4], "my_lemma4": 2, "abs_mul": 2, "mul_le_mul": 2, "abs_nonneg": 2, "mul_lt_mul_right": 2, "extract": [2, 7], "hidden": 2, "expos": [2, 7], "predic": [2, 3, 4, 6, 7, 8], "fnub": 2, "fnlb": 2, "lambda": [2, 5], "hfa": 2, "hgb": 2, "dsimp": [2, 3, 4, 5], "simplif": [2, 3, 4], "contract": 2, "anyhow": 2, "control": 2, "transform": [2, 3], "rest": [2, 3, 5, 7], "routin": 2, "nnf": 2, "nng": 2, "hfb": 2, "nna": 2, "codomain": [2, 4, 7], "structur": [2, 4, 6, 7, 8, 9, 11], "monoid": [2, 3, 4, 6], "fnub_add": 2, "orderedcanceladdcommmonoid": 2, "high": 2, "monoton": [2, 6, 7], "nondecreas": [2, 4], "placehold": 2, "Or": [2, 3], "backward": [2, 7], "subgoal": 2, "mf": 2, "mg": 2, "aleb": 2, "flag": [2, 3], "squiggli": 2, "marker": 2, "nnc": 2, "bbb": [2, 5], "fneven": 2, "fnodd": 2, "ef": 2, "eg": 2, "og": 2, "shorten": 2, "rid": 2, "won": [2, 4, 6, 7], "cannot": [2, 3, 4, 5, 6, 7], "contrari": 2, "syntact": 2, "reduct": [2, 3], "erw": 2, "harder": 2, "spot": 2, "manipul": [2, 5, 7], "foundat": [2, 3, 4, 5], "mundan": 2, "assert": [2, 3, 6], "contrast": [2, 3, 5, 6, 7], "zermelo": 2, "fraenkel": 2, "sin": [2, 8], "co": 2, "zf": 2, "defect": [2, 6, 7], "theoret": [2, 3, 7], "motiv": 2, "detect": 2, "meaningless": 2, "independ": [2, 3, 5], "continuum": 2, "meta": [2, 6], "beyond": [2, 6, 8], "ask": [2, 4, 5, 6, 7], "xs": [2, 3], "refl": [2, 3, 5, 6], "tran": [2, 4, 5, 6], "setub": 2, "inject": [2, 3, 4, 6, 7], "x_1": [2, 3], "x_2": [2, 3], "x\u2081": [2, 3, 5, 7], "x\u2082": [2, 3, 5], "add": [2, 4, 5, 6, 7, 8], "nonzero": [2, 4, 5, 9], "sourc": [2, 7], "inspir": 2, "add_left_inj": 2, "composit": [2, 3, 5, 6, 7], "injg": 2, "injf": [2, 3], "canon": [2, 3, 4, 5], "exhibit": [2, 7], "anonym": [2, 3, 4, 5], "constructor": [2, 3, 4, 5, 6], "angl": 2, "certain": [2, 6, 7], "fnhasub": 2, "fnhaslb": 2, "ubf": 2, "ubg": 2, "ubfa": 2, "ubgb": 2, "unpack": [2, 3], "claus": [2, 6], "els": [2, 3, 4], "turn": [2, 3, 4, 5, 6, 7, 8], "fn_ub_add": 2, "directli": [2, 4, 5, 6, 7], "lbf": 2, "lbg": 2, "cousin": 2, "rcase": [2, 3, 4, 5, 7], "flexibl": [2, 7], "recurs": [2, 3, 5, 11], "harm": [2, 3], "swiss": 2, "armi": 2, "knive": 2, "wide": 2, "old": [2, 5, 6], "chestnut": 2, "product": [2, 4, 5, 6, 7, 9], "magic": [2, 5, 6], "verifi": 2, "sumofsquar": 2, "sumofsquares_mul": 2, "sosx": 2, "sosi": 2, "xeq": [2, 3], "yeq": 2, "insight": 2, "gaussian": [2, 11], "i": [2, 3, 4, 5, 7, 8, 9], "sqrt": [2, 3, 4, 5], "norm": [2, 5, 7, 11], "reflect": 2, "di": [2, 5], "xy": [2, 5], "cryptic": 2, "easiest": [2, 4], "perspicu": 2, "6": [2, 4, 5, 6, 7, 8], "divab": 2, "divbc": 2, "beq": 2, "ceq": 2, "And": [2, 4, 6, 7], "pretti": [2, 6, 7], "Then": [2, 3, 5, 6, 7, 9], "divac": 2, "alpha": [2, 3], "beta": [2, 3], "surject": [2, 3, 7], "yourself": [2, 5], "mul_div_cancel": [2, 4], "field_simp": [2, 5], "denomin": [2, 4, 5], "hx": [2, 3, 5, 6, 8], "surjg": 2, "surjf": [2, 3], "contradict": [2, 3, 4], "speak": [2, 5, 7], "irreflex": 2, "asymmetri": 2, "lt_asymm": 2, "sugar": 2, "eventu": [2, 3, 7], "fnuba": 2, "not_le_of_gt": 2, "not_lt_of_g": [2, 4, 5], "lt_of_not_g": 2, "le_of_not_gt": 2, "snippet": [2, 4, 5], "counterexampl": [2, 8], "monof": 2, "four": [2, 5], "valid": 2, "far": [2, 3, 6, 7], "q": [2, 4, 5, 6, 7], "straightforward": [2, 6], "difficult": [2, 6], "conclud": [2, 8], "nonexist": 2, "contradictori": 2, "classic": [2, 3, 4], "by_contra": [2, 4], "not_not": 2, "front": 2, "push": [2, 4, 7], "inward": 2, "facilit": [2, 7], "push_neg": [2, 3, 4], "restat": [2, 6], "contrapos": [2, 3, 4], "similarli": [2, 3, 4, 5], "yet": [2, 3, 4, 5, 6, 7], "semicolon": [2, 4], "falso": 2, "anyth": [2, 5, 7], "elim": 2, "strang": [2, 4], "fairli": 2, "reach": [2, 6], "37": 2, "exfalso": 2, "absurd": [2, 4], "slick": 2, "drop": 2, "manner": [2, 5], "compon": [2, 3, 5, 7, 9], "techniqu": [2, 7], "variou": [2, 3, 5, 6, 9], "xltz": 2, "zlty": 2, "10": 2, "7": [2, 4], "behav": [2, 3, 6, 7], "roughli": [2, 3, 4], "friend": [2, 5], "were": [2, 4, 5, 7], "inscrut": [2, 3], "gadget": [2, 7], "auxiliari": [2, 7], "pow_eq_zero": [2, 4], "doubl": [2, 3], "symmetr": [2, 3], "abs_lt": 2, "dvd_gcd_iff": 2, "8": [2, 4, 7], "15": 2, "not_monotone_iff": 2, "antisymmetr": 2, "aris": 2, "preorder": [2, 6, 7], "pre": 2, "lt_iff_le_not_l": 2, "repeatedli": [2, 7], "instanti": [2, 5, 6, 7], "inl": [2, 3], "inr": [2, 3], "produc": [2, 8], "branch": [2, 3, 6], "le_or_gt": 2, "abs_of_nonneg": [2, 5], "abs_of_neg": 2, "immedi": [2, 3, 5, 6], "myab": 2, "le_abs_self": 2, "neg_le_abs_self": 2, "enjoi": [2, 3, 4, 7], "pun": 2, "lt_ab": 2, "genuin": 2, "vertic": [2, 5], "lt_trichotomi": 2, "xgt": 2, "dvd_mul_right": [2, 4], "eq_zero_or_eq_zero_of_mul_eq_zero": 2, "zero": [2, 3, 4, 5, 6, 7, 8, 9], "nontrivi": [2, 3, 4, 5, 7], "integr": [2, 8, 11], "isdomain": 2, "em": [2, 3], "exclud": [2, 4], "by_cas": [2, 3, 4], "dispos": 2, "s_0": [2, 3], "s_1": 2, "s_2": 2, "ldot": [2, 3, 4], "varepsilon": [2, 7], "s_n": [2, 3], "render": [2, 4], "convergesto": 2, "ext": [2, 3, 4, 5, 6], "enabl": [2, 3, 4, 5], "actual": [2, 3, 4, 6, 7], "u": [2, 3, 5, 7, 9], "v": [2, 3, 5, 7], "congr": 2, "reconcil": 2, "peel": 2, "ab": [2, 5], "convert": [2, 4], "quit": [2, 6, 7], "zero_lt_on": [2, 4], "fill": [2, 3, 4, 5], "convergesto_const": 2, "\u03b5po": [2, 7], "nge": 2, "abs_zero": 2, "save": 2, "troubl": [2, 3, 5], "pen": 2, "paper": [2, 3, 5, 7, 9], "ns": 2, "nt": 2, "maximum": [2, 4, 7], "implement": [2, 5, 6, 8], "convergesto_add": 2, "cs": 2, "ct": 2, "clean": [2, 7], "\u03b52po": 2, "hs": [2, 4, 7, 9], "ht": 2, "le_of_max_le_left": 2, "le_of_max_le_right": 2, "tricki": [2, 3, 4, 6], "convergesto_mul_const": 2, "acpo": 2, "abs_po": 2, "exists_abs_le_of_convergesto": 2, "strong": [2, 4], "n\u2080": 2, "bpo": [2, 7], "pos\u2080": 2, "div_po": 2, "n\u2081": 2, "convergesto_mul": 2, "sketch": [2, 3, 4, 7], "limit": [2, 6, 7], "bold": 2, "scratch": 2, "convergesto_uniqu": 2, "sa": 2, "sb": 2, "abn": 2, "na": 2, "hna": 2, "nb": 2, "hnb": 2, "absa": 2, "absb": 2, "observ": [2, 4, 7], "everywher": [2, 3, 6, 7, 9], "linearord": 2, "vastli": 2, "awai": [2, 5], "vocabulari": 3, "uniform": [3, 7, 8], "primit": 3, "conceptu": 3, "advantag": [3, 4, 5, 8], "overload": 3, "verbos": 3, "system": [3, 4, 5, 6], "wrong": 3, "ss": 3, "sub": [3, 7, 9, 11], "cap": 3, "un": 3, "cup": 3, "univ": [3, 7, 8, 9], "empti": [3, 4, 5, 7, 9], "member": [3, 7], "membership": [3, 4, 6], "mem": 3, "notin": 3, "ident": [3, 4, 5, 6, 7, 11], "databas": [3, 4, 6, 7], "unlik": [3, 4], "existenti": [3, 11], "subset_def": 3, "inter_def": 3, "mem_setof": 3, "xu": 3, "mem_inter_iff": 3, "xsu": 3, "phenomenon": 3, "quirk": 3, "process": 3, "pitfal": 3, "heavili": [3, 7], "fall": 3, "union_def": 3, "mem_union": [3, 4], "xtu": 3, "xt": 3, "unnecessari": 3, "correctli": 3, "special": [3, 4, 5, 6, 7, 9], "rewritten": 3, "diff_eq": 3, "mem_diff": 3, "xstu": 3, "xnt": 3, "xnu": 3, "extension": [3, 5], "unsurprisingli": 3, "and_comm": 3, "antisymm": 3, "hood": [3, 5], "builder": 3, "trivial": [3, 4, 7], "eq_two_or_odd": 3, "even_iff": 3, "confus": [3, 4, 6, 7], "fortun": 3, "agre": 3, "prime_iff": 3, "symm": [3, 4, 5, 6, 7, 8], "rwa": [3, 4, 5], "restrict": [3, 4, 7], "signific": 3, "ball": [3, 8], "bex": 3, "bex_def": 3, "prime_x": 3, "slight": 3, "ssubt": 3, "index": [3, 6, 7], "model": [3, 7], "sequenc": [3, 6, 7, 8, 11], "a_0": 3, "a_1": 3, "a_2": 3, "mem_iunion": 3, "xai": 3, "mem_iint": 3, "mem_iunion\u2082": 3, "mem_iinter\u2082": 3, "exists_prime_and_dvd": 3, "eq_univ": 3, "eq_univ_of_foral": 3, "exists_infinite_prim": 3, "\u2080": 3, "sunion": 3, "sinter": 3, "relationship": [3, 4], "sunion_eq_biunion": 3, "sinter_eq_biint": 3, "preimag": [3, 7], "imag": [3, 4, 6, 7], "tripl": 3, "tag": [3, 6], "mem_image_of_mem": 3, "galoi": [3, 5, 7], "image_subset_iff": 3, "represent": [3, 4, 5], "asid": 3, "raini": 3, "dai": 3, "behavior": [3, 6, 7], "nonempti": [3, 7], "condit": [3, 4, 6, 7, 8], "fxeq": 3, "ai": 3, "fx": 3, "eq": [3, 5], "injon": [3, 9], "theme": 3, "rel": [3, 5], "relativ": 3, "xpo": 3, "ypo": 3, "exp_log": 3, "ingredi": [3, 5, 7, 8], "assign": [3, 5, 6], "inhabit": [3, 5, 7], "appeal": [3, 6], "choose_spec": 3, "noncomput": [3, 5], "inverse_spec": 3, "dif_po": 3, "dif_neg": 3, "fulli": [3, 7], "alon": 3, "leftinvers": 3, "rightinvers": 3, "hack": 3, "half": 3, "dozen": 3, "condens": 3, "cantor": 3, "famou": 3, "j": [3, 5], "intuit": [3, 7], "cardin": 3, "biject": [3, 5], "nineteenth": 3, "centuri": 3, "infinit": [3, 7, 11], "dedekind": 3, "quickli": [3, 9], "behind": 3, "problem": [3, 4, 5, 6, 7], "shade": 3, "region": 3, "diagram": 3, "circ": [3, 5], "scale": 3, "inner": 3, "smaller": [3, 4, 7], "concentr": 3, "unshad": 3, "compos": [3, 5, 7], "disjoint": [3, 9], "sound": [3, 5, 6], "plausibl": 3, "delic": 3, "improv": [3, 4], "confid": 3, "better": [3, 4, 5, 6, 7], "invfun": [3, 5], "leftinverse_invfun": 3, "invfun_eq": 3, "sbaux": 3, "sbset": 3, "sb_aux": 3, "s_": 3, "sb_set": 3, "bigcup_": 3, "mathbb": [3, 4, 5], "sbfun": 3, "complement": [3, 7, 9], "outermost": 3, "setminu": 3, "inv_fun": 3, "inv_fun_eq": 3, "sb_right_inv": 3, "goe": [3, 4, 5, 6, 7], "neither": [3, 5, 6], "nor": [3, 5], "sb_inject": 3, "hf": [3, 7, 8, 9], "hg": [3, 7, 8, 9], "a_def": 3, "h_def": 3, "hxeq": 3, "xa": [3, 5], "wlog": 3, "x\u2081a": 3, "resolve_left": 3, "x\u2082a": 3, "not_imp_self": 3, "x\u2082na": 3, "if_po": 3, "if_neg": 3, "x\u2082eq": 3, "hn": [3, 4, 7, 8], "sb_fun": 3, "bring": [3, 4, 7], "tradeoff": 3, "encapsul": [3, 5, 8], "symmetri": [3, 6], "dwell": 3, "succ": [3, 4, 6], "sb_surject": 3, "gya": 3, "xmem": 3, "sweet": 3, "schroeder_bernstein": 3, "substant": 4, "ancient": 4, "fraction": 4, "lowest": 4, "2c": 4, "4c": 4, "factor": [4, 5], "coprim": 4, "smart": 4, "12": 4, "encount": [4, 6], "algebra": [4, 6, 7, 8, 9, 11], "prime_def_lt": 4, "eq_one_or_self_of_dvd": 4, "prime_p": 4, "17": 4, "commonli": [4, 5], "prime_two": 4, "prime_thre": 4, "broader": [4, 8], "irreduc": [4, 5], "coincid": [4, 5, 7], "rise": [4, 6], "dvd_mul": 4, "even_of_even_sqr": 4, "dvd_of_dvd_pow": 4, "proce": [4, 6], "profici": 4, "prefix": [4, 6], "search": [4, 5, 6], "engin": 4, "hesit": 4, "mul_right_inj": 4, "heart": 4, "irration": 4, "dvd_gcd": 4, "coprime_mn": 4, "sqr_eq": 4, "meq": 4, "dvd_iff_exists_eq_mul_left": 4, "two_l": 4, "le_of_dvd": 4, "approach": [4, 5, 6, 7], "quick": [4, 8], "ne": [4, 5], "occur": 4, "suffici": [4, 7], "permut": 4, "prime_of_mem_factor": 4, "prod_factor": 4, "factors_uniqu": 4, "talk": [4, 7, 8], "factorization_mul": 4, "mnez": 4, "nnez": 4, "factorization_pow": 4, "black": [4, 6], "box": 4, "simpa": [4, 8], "nnz": 4, "nsqr_nez": 4, "eq1": 4, "eq2": 4, "add_mul_mod_self_left": 4, "mul_mod_right": 4, "count_factors_mul_of_po": 4, "successor": 4, "succ_ne_zero": 4, "npow_nz": 4, "dvd_sub": 4, "pow_eq": 4, "npowz": 4, "add_sub_cancel": 4, "understood": [4, 7], "quotient": [4, 5, 6, 7], "pictur": [4, 5], "mediat": 4, "headach": 4, "contend": 4, "issu": [4, 5, 6, 7], "th": 4, "topic": [4, 6], "enat": 4, "infin": [4, 7, 9], "appreci": 4, "role": [4, 5, 7], "datatyp": 4, "freeli": 4, "translat": [4, 6, 7], "mathematician": [4, 7], "inj": 4, "factori": 4, "fac": 4, "ih": 4, "fac_po": 4, "succ_po": 4, "dvd_fac": 4, "ipo": 4, "il": 4, "of_le_succ": 4, "dvd_mul_of_dvd_right": 4, "crude": 4, "remaind": [4, 5], "pow_two_le_fac": 4, "finset": [4, 5, 7], "bigoper": [4, 5], "prod": [4, 7, 9], "sum_range_zero": 4, "sum_range_succ": 4, "summat": 4, "prod_range_zero": 4, "prod_range_succ": 4, "deserv": 4, "danger": [4, 5], "ordinarili": [4, 5], "loop": 4, "indefinit": 4, "fix": [4, 6, 7], "placement": 4, "re": [4, 5], "handi": 4, "sum_id": 4, "div_eq_of_eq_mul_right": 4, "succ_eq_add_on": 4, "sum_sqr": 4, "mynat": 4, "thumb": 4, "decid": [4, 7], "preced": 4, "truncat": 4, "exponenti": 4, "cut": 4, "predecessor": 4, "pred": 4, "mul": [4, 5, 6, 7], "succ_add": 4, "succ_mul": 4, "explor": [4, 7], "standard": [4, 5, 6, 7], "formul": [4, 7], "quirki": 4, "among": 4, "annoi": [4, 6], "h0": 4, "succ_le_succ": 4, "zero_l": [4, 5], "interval_cas": 4, "interv": [4, 7, 9], "decis": 4, "procedur": [4, 6], "revert": [4, 5], "minfac": 4, "smallest": [4, 6, 7], "strong_induction_on": 4, "subsum": 4, "exists_prime_factor": 4, "np": 4, "mltn": 4, "mdvdn": 4, "mne1": 4, "mz": 4, "zero_dvd_iff": 4, "mgt2": 4, "pp": 4, "pdvd": 4, "factorial_po": 4, "dvd_factori": 4, "primes_infinit": 4, "refin": [4, 8], "ple": 4, "p_1": 4, "p_n": 4, "prod_": 4, "p_i": [4, 7], "computation": 4, "test": 4, "decidableeq": 4, "abandon": 4, "ourselv": [4, 6], "subset_iff": 4, "mem_int": 4, "mem_sdiff": 4, "tauto": 4, "dispens": 4, "tautolog": 4, "dvd_prod_of_mem": 4, "eq_of_dvd_of_prim": 4, "prime_q": 4, "preserv": [4, 6, 7], "induction_on": 4, "singleton": 4, "prod_empti": 4, "prod_insert": 4, "mem_of_dvd_prod_prim": 4, "mem_insert": 4, "wrote": 4, "filter": [4, 8, 9, 11], "mem_filt": 4, "aim": 4, "prod_po": 4, "_def": 4, "mem_": 4, "id": [4, 6, 7, 8], "bounded_of_ex_finset": 4, "qk": 4, "lt_succ_of_l": 4, "le_sup": 4, "ex_finset_of_bound": 4, "decidablepr": 4, "lt_succ_iff": 4, "congruent": 4, "p_k": 4, "loss": 4, "27": 4, "mod_4_eq_3_or_mod_4_eq_3": 4, "mul_mod": 4, "mod_lt": 4, "hm": [4, 8], "two_le_of_mod_4_eq_3": 4, "neq": 4, "div_dvd_of_dvd": 4, "div_lt_self": 4, "exists_prime_factor_mod_4_eq_3": 4, "dvd_rfl": 4, "mge2": 4, "home": [4, 5], "stretch": [4, 5], "remov": [4, 7], "eras": 4, "mem_eras": 4, "readi": [4, 6, 7, 8], "dvd_add_iff_left": 4, "primes_mod_4_eq_3_infinit": 4, "p4": 4, "pltn": 4, "p4eq": 4, "ps": 4, "pne3": 4, "seriou": [4, 6, 7], "feat": 4, "modern": 5, "subject": 5, "mysteri": [5, 6], "consult": 5, "ann": 5, "baanen": 5, "abus": 5, "paramet": [5, 6], "broadest": 5, "constraint": [5, 7], "bundl": [5, 6, 7, 8], "tupl": 5, "hy": [5, 6], "hz": [5, 6], "mypoint1": 5, "mypoint2": 5, "mypoint3": 5, "mk": [5, 6, 7], "former": 5, "latter": [5, 7], "quot": [5, 7], "protect": 5, "intern": 5, "add_x": 5, "addalt": 5, "etc": [5, 7], "y\u2081": 5, "z\u2081": 5, "y\u2082": 5, "z\u2082": 5, "addalt_x": 5, "addalt_comm": 5, "ya": 5, "za": 5, "xb": 5, "yb": 5, "zb": 5, "apart": [5, 6], "effici": [5, 7], "scalar": [5, 6, 8], "smul": [5, 6], "smul_distrib": 5, "road": 5, "link": [5, 6], "belong": [5, 6, 7], "simplex": 5, "convinc": 5, "equilater": 5, "interior": [5, 8], "standardtwosimplex": 5, "x_nonneg": 5, "y_nonneg": 5, "z_nonneg": 5, "sum_eq": 5, "swap": 5, "swapxi": 5, "interestingli": [5, 8], "midpoint": 5, "div_nonneg": 5, "weight": 5, "averag": 5, "weightedaverag": 5, "lambda_nonneg": 5, "lambda_l": 5, "fin": [5, 9], "standardsimplex": 5, "sum_eq_on": 5, "div_eq_mul_inv": 5, "sum_mul": 5, "sum_add_distrib": 5, "mul_sum": 5, "islinear": 5, "is_addit": 5, "preserves_mul": 5, "linf": 5, "subtyp": [5, 6, 7], "preal": 5, "val": 5, "sigma": [5, 9], "wherebi": [5, 7], "stdsimplex": 5, "\u03c3": 5, "fst": [5, 7], "snd": [5, 7], "custom": 5, "robust": [5, 6], "interfac": 5, "redefin": [5, 6], "accessor": 5, "weav": 5, "rich": [5, 6], "interconnect": 5, "hierarchi": [5, 11], "clarifi": 5, "antireflex": 5, "cdot": 5, "mathcal": [5, 8], "proxi": 5, "bipartit": 5, "graph": 5, "categori": [5, 7, 8], "morphism": [5, 8, 11], "basi": [5, 7], "discret": [5, 8], "inherit": [5, 6], "polynomi": 5, "coeffici": 5, "dual": [5, 7], "accommod": 5, "almost": [5, 6, 7, 9], "marriag": 5, "heaven": 5, "group\u2081": [5, 6], "inv": [5, 6], "struc": 5, "counterpart": 5, "chosen": 5, "assur": 5, "groupcat": 5, "group\u2081cat": 5, "str": 5, "capit": 5, "roman": 5, "equiv": 5, "tofun": [5, 6], "right_inv": 5, "left_inv": 5, "creativ": 5, "evid": 5, "coercion": [5, 6, 7, 8], "omit": 5, "perm": 5, "under": [5, 6, 7], "orient": 5, "permgroup": 5, "trans_assoc": 5, "trans_refl": 5, "refl_tran": 5, "self_trans_symm": 5, "grouptheori": 5, "g_1": 5, "g_2": 5, "g_3": 5, "tightli": 5, "isomorph": [5, 8], "Its": [5, 6], "neg": [5, 6, 7, 9], "reproduc": 5, "accompani": 5, "addgroup\u2081": 5, "scheme": 5, "addgrouppoint": 5, "arrang": 5, "mul_inv_cancel_right": 5, "achiev": [5, 6, 7], "silent": [5, 6], "regist": [5, 6], "grp": 5, "contextu": 5, "cue": 5, "synthes": [5, 6], "whole": 5, "_inst_1": 5, "candid": 5, "group\u2082": 5, "mysquar": 5, "my_squar": 5, "remark": [5, 6], "headi": 5, "store": 5, "hasmulgroup\u2082": 5, "hasonegroup\u2082": 5, "hasinvgroup\u2082": 5, "suppli": 5, "accord": 5, "capabl": 5, "chain": 5, "recent": 5, "prioriti": 5, "bad": [5, 6, 7], "artifici": 5, "addgroup\u2082": 5, "subtl": [5, 7], "configur": 5, "invis": [5, 6], "wise": 5, "euclidean": 5, "terminolog": 5, "mid": 5, "imaginari": 5, "gaussint": 5, "im": 5, "pointwis": [5, 7, 8], "root": [5, 6, 11], "ac": 5, "bci": 5, "adi": 5, "bd": 5, "bc": 5, "hasmul": 5, "zero_def": 5, "one_def": 5, "add_def": 5, "neg_def": 5, "mul_def": 5, "zero_r": 5, "zero_im": 5, "one_r": 5, "one_im": 5, "add_r": 5, "add_im": 5, "neg_r": 5, "neg_im": 5, "mul_r": 5, "mul_im": 5, "surprisingli": [5, 6], "concept": [5, 7, 8], "light": 5, "bulb": 5, "skeleton": [5, 7], "scari": 5, "instcommr": 5, "left_distrib": [5, 6], "right_distrib": [5, 6], "ext_iff": 5, "bq": 5, "archetyp": 5, "int": [5, 6], "ediv_add_emod": 5, "emod_nonneg": 5, "emod_lt": 5, "unit": [5, 6, 7], "algorithm": 5, "conjug": 5, "frac": 5, "nearest": 5, "size": 5, "vi": 5, "multipli": 5, "emb": 5, "forth": 5, "quadrat": 5, "gaussianint": 5, "stai": 5, "face": [5, 6, 7], "machineri": [5, 6, 7], "adapt": 5, "invest": 5, "pragmat": 5, "seek": 5, "heather": 5, "macbeth": 5, "eleg": 5, "div": 5, "mod": 5, "_add_mod": 5, "abs_mod": 5, "_le": 5, "emod_lt_of_po": 5, "zero_lt_two": 5, "fixm": 5, "_eq": 5, "sq_add_sq_eq_zero": 5, "linearorderedr": 5, "norm_nonneg": [5, 8], "norm_eq_zero": [5, 8], "norm_po": 5, "norm_mul": [5, 8], "conj": 5, "conj_r": 5, "conj_im": 5, "norm_conj": 5, "bespok": 5, "quad": 5, "record": [5, 6], "div_def": 5, "mod_def": 5, "messi": 5, "nicer": [5, 7], "norm_mod_lt": 5, "norm_y_po": 5, "sq_ab": 5, "gcongr": 5, "ediv_mul_l": 5, "le_of_mul_le_mul_right": 5, "ediv_lt_of_lt_mul": 5, "natab": 5, "coe_natabs_norm": 5, "natabs_of_nonneg": 5, "natabs_norm_mod_lt": 5, "ofnat_lt": 5, "coe_natab": 5, "not_norm_mul_left_lt_norm": 5, "natabs_mul": 5, "le_mul_of_one_le_right": 5, "ofnat_l": 5, "add_one_le_of_lt": 5, "euclideandomain": 5, "quotient_mul_add_remainder_eq": 5, "quotient_zero": 5, "r_wellfound": 5, "remainder_lt": 5, "mul_left_not_lt": 5, "payoff": 5, "principalidealr": 5, "irreducible_iff_prim": 5, "studi": [6, 7], "prematur": 6, "technolog": 6, "simpler": 6, "ring\u2081": 6, "gradual": [6, 7], "bottom": [6, 7], "endow": 6, "one\u2081": 6, "heavier": 6, "inferr": 6, "resolut": 6, "ie": [6, 7], "attribut": 6, "ensur": [6, 7], "self": 6, "one\u2082": 6, "usabl": 6, "silli": 6, "affect": 6, "importantli": 6, "habit": 6, "ascript": 6, "messag": 6, "typeclass": 6, "stuck": 6, "metavari": 6, "263": 6, "auto": 6, "sever": [6, 7, 9], "unknown": 6, "collis": 6, "builtin": 6, "\ud835\udfd9": 6, "inherit_doc": 6, "diamond": 6, "dia\u2081": 6, "dia": 6, "infixl": 6, "70": 6, "semigroup": 6, "dia_assoc": 6, "semigroup\u2081": 6, "todia\u2081": 6, "previous": 6, "semigroup\u2082": 6, "hurdl": 6, "neutral": 6, "diaoneclass\u2081": 6, "one_dia": 6, "dia_on": 6, "trace": 6, "info": 6, "ters": 6, "expend": 6, "attempt": 6, "succe": 6, "success": 6, "set_opt": 6, "synthinst": 6, "monoid\u2081": 6, "hide": [6, 7], "subtleti": 6, "fear": 6, "unrel": 6, "tosemigroup\u2081": 6, "todiaoneclass\u2081": 6, "monoid\u2082": 6, "toone\u2081": 6, "overlap": 6, "tear": 6, "signatur": 6, "restor": 6, "optim": [6, 9], "reusabl": 6, "inv\u2081": 6, "postfix": 6, "inv_dia": 6, "weak": 6, "preliminari": 6, "left_inv_eq_right_inv\u2081": 6, "hba": 6, "hac": 6, "export": 6, "inv_eq_of_dia": 6, "dia_inv": 6, "naiv": [6, 7], "duplic": 6, "to_addit": 6, "semi": 6, "left_inv_eq_right_inv": 6, "left_neg_eq_right_neg": 6, "whatsnew": 6, "addsemigroup\u2083": 6, "add_assoc\u2083": 6, "semigroup\u2083": 6, "mul_assoc\u2083": 6, "addmonoid\u2083": 6, "addzeroclass": 6, "monoid\u2083": 6, "muloneclass": 6, "tomuloneclass": 6, "addcommsemigroup\u2083": 6, "commsemigroup\u2083": 6, "addcommmonoid\u2083": 6, "commmonoid\u2083": 6, "addgroup\u2083": 6, "neg_add": 6, "group\u2083": 6, "inv_mul": 6, "inv_eq_of_mul": 6, "propag": 6, "attr": 6, "mul_inv": 6, "mul_left_cancel\u2083": 6, "mul_right_cancel\u2083": 6, "addcommgroup\u2083": 6, "commgroup\u2083": 6, "demonstr": [6, 7], "opposit": [6, 7], "gain": 6, "besid": 6, "parent": 6, "ring\u2083": 6, "mulzeroclass": 6, "toaddgroup\u2083": 6, "mayb": 6, "le\u2081": 6, "50": 6, "\u2081": 6, "preorder\u2081": 6, "partialorder\u2081": 6, "orderedcommmonoid\u2081": 6, "modul": 6, "pretend": 6, "smul\u2083": 6, "infixr": 6, "73": 6, "module\u2081": 6, "zero_smul": 6, "one_smul": 6, "mul_smul": 6, "add_smul": 6, "smul_add": 6, "surpris": 6, "toaddcommgroup\u2083": 6, "inst": 6, "module\u2083": 6, "hunt": 6, "unspecifi": 6, "embark": 6, "main": [6, 7, 8], "quest": 6, "huge": 6, "trap": 6, "refus": [6, 7], "tosmul\u2083": 6, "inst_1": 6, "safe": 6, "selfmodul": 6, "invert": 6, "nsmul\u2081": 6, "zsmul\u2081": 6, "ofnat": 6, "negsucc": 6, "intermedi": [6, 7], "abgrpmodul": 6, "failur": 6, "synth": 6, "indirect": 6, "path": 6, "thank": [6, 7], "offend": 6, "poor": 6, "forget": 6, "http": 6, "inria": 6, "hal": 6, "scienc": 6, "02463336": 6, "modifi": 6, "nsmul": 6, "addmonoid\u2084": 6, "nsmul_zero": 6, "nsmul_succ": 6, "mysmul": 6, "stori": 6, "incorpor": 6, "zsmul": 6, "lt\u2081": 6, "comparison": 6, "ismonoidhom\u2081": 6, "unpleas": [6, 7], "conjunct": [6, 11], "chose": 6, "ismonoidhom\u2082": 6, "map_on": 6, "map_mul": 6, "tempt": 6, "higher": 6, "unif": 6, "psycholog": 6, "rare": 6, "adject": 6, "bare": 6, "noun": 6, "argu": 6, "continuous_id": [6, 7], "primari": 6, "monoidhom\u2081": 6, "coefun": 6, "coerc": 6, "coe": 6, "addmonoidhom\u2081": 6, "addmonoid": 6, "map_zero": 6, "map_add": [6, 8], "ringhom\u2081": 6, "minor": [6, 8], "tomonoidhom\u2081": 6, "juggl": 6, "monoidhomclass\u2081": 6, "badinst": 6, "wouldn": 6, "priori": 6, "boil": 6, "hopelessli": 6, "checksynthord": 6, "random": 6, "deduc": [6, 7], "outparam": 6, "trigger": 6, "retri": 6, "monoidhomclass\u2082": 6, "promis": [6, 7], "map_inv_of_inv": 6, "sight": 6, "got": 6, "presenc": 6, "layer": [6, 7], "funlik": 6, "monoidhomclass": 6, "monoidhomclass\u2083": 6, "coe_inject": 6, "stop": 6, "ringhomclass\u2083": 6, "ringhom": 6, "algebrahom": 6, "ve": [6, 7], "primarili": [6, 7], "unbundl": 6, "orderpreshom": 6, "le_of_l": 6, "orderpresmonoidhom": 6, "orderpreshomclass": 6, "subgroup": 6, "subr": 6, "reus": 6, "led": 6, "descend": 6, "break": 6, "barrier": 6, "setlik": 6, "wrap": [6, 7], "submonoid\u2081": 6, "submonoid": 6, "mul_mem": 6, "one_mem": 6, "tackl": 6, "setco": 6, "submonoid\u2081monoid": 6, "destructur": 6, "binder": 6, "submonoidclass\u2081": 6, "subgroup\u2081": 6, "subgroupclass\u2081": 6, "subobject": 6, "s\u2081": 6, "s\u2082": 6, "shame": 6, "across": 6, "weird": [6, 7], "distract": 6, "emphas": 6, "anecdot": 6, "devic": 6, "hasquoti": 6, "bewar": 6, "regular": [6, 7], "ascii": 6, "setoid": 6, "commmonoid": 6, "iseqv": 6, "hw": 6, "quotientmonoid": 6, "map\u2082": 6, "calculu": [7, 9, 11], "quantiti": 7, "begun": 7, "paradox": 7, "exot": 7, "x\u2080": [7, 8], "convention": 7, "eight": 7, "varieti": 7, "wish": 7, "64": 7, "y\u2080": 7, "z\u2080": 7, "paragraph": 7, "512": 7, "bourbaki": 7, "spell": 7, "dualli": 7, "arbitrarili": 7, "neighborhood": 7, "attop": [7, 9], "\ud835\udcdd": [7, 8, 9], "\ud835\udce4": 7, "entourag": 7, "\u03bc": [7, 9], "a_": 7, "univ_set": 7, "sets_of_superset": 7, "inter_set": 7, "blur": 7, "princip": 7, "\ud835\udcdf": 7, "opportun": 7, "x_0": 7, "ioo": [7, 8], "tendsto\u2081": 7, "tendsto": [7, 9], "lim_": 7, "abstractli": 7, "salient": 7, "pushforward": 7, "f_": 7, "tendsto\u2082": 7, "via": 7, "leverag": 7, "map_mono": 7, "map_map": 7, "shot": 7, "256": 7, "pullback": 7, "comap": 7, "map_le_iff_le_comap": 7, "contravari": 7, "comap_comap": 7, "plane": 7, "\u02e2": 7, "nhds_prod_eq": 7, "aforement": 7, "le_inf_iff": 7, "shouldn": 7, "prohibit": 7, "global": 7, "precondit": 7, "closur": 7, "nebot": 7, "tour": [7, 8], "claim": 7, "recaptur": 7, "superfici": 7, "stronger": 7, "famili": [7, 8], "\u03b9": [7, 8, 9], "hasbasi": 7, "nhds_basis_ioo_po": 7, "has_basi": 7, "tendsto_iff": 7, "reformul": 7, "ici": 7, "attop_basi": 7, "knew": 7, "gave": 7, "n_p": 7, "n_q": 7, "tiresom": 7, "\u1da0": [7, 8, 9], "superscript": 7, "hp": 7, "hq": 7, "eventually_eq": 7, "tendsto_congr": 7, "review": 7, "eventually_of_foral": 7, "mono": 7, "item": 7, "filter_upward": 7, "hr": 7, "ae": [7, 9], "aka": 7, "occasion": 7, "frequent": 7, "sophist": 7, "mem_closure_of_tendsto": 7, "clusterpt": 7, "mem_closure_iff_clusterpt": 7, "le_principal_iff": 7, "nebot_of_l": 7, "hux": 7, "hum": 7, "dist_eq_zero": 7, "emetricspac": 7, "pseudometricspac": 7, "pseudoemetricspac": 7, "journei": 7, "recast": 7, "tendsto_attop": 7, "continuous_iff": 7, "devot": 7, "uncurri": 7, "slow": 7, "continuous_fst": 7, "comp": 7, "assembl": 7, "prod_mk": 7, "continuous_snd": 7, "continuous_dist": 7, "clunki": 7, "crucial": 7, "elabor": 7, "prod_map": 7, "sad": 7, "border": 7, "obfusc": 7, "continuous_pow": 7, "continuousat": [7, 9], "continuousat_iff": 7, "geometr": 7, "closedbal": 7, "sign": 7, "radiu": 7, "mem_ball_self": 7, "mem_closedball_self": 7, "isopen": 7, "isopen_iff": 7, "Their": [7, 8], "isclos": [7, 8], "s\u1d9c": [7, 9], "isopen_compl_iff": 7, "hu": [7, 8], "mem_of_tendsto": 7, "mem_closure_iff": 7, "mem_closure_iff_seq_limit": 7, "nhds_basis_bal": 7, "nhds_basis_closedbal": 7, "mem_iff": 7, "segment": [7, 9], "somewher": 7, "continuouson": [7, 8], "minimum": 7, "iscompact": 7, "icc": [7, 8], "iscompact_icc": 7, "\u03c6": 7, "strictmono": 7, "tendsto_subseq": 7, "exists_forall_l": 7, "exists_forall_g": 7, "compactspac": 7, "iscompact_univ": 7, "cauchi": 7, "uniformcontinu": 7, "uniformcontinuous_iff": 7, "clearli": 7, "isclosed_l": 7, "eq_empty_or_nonempti": 7, "attain": 7, "closer": 7, "cauchyseq": 7, "cauchyseq_iff": 7, "completespac": [7, 8, 9], "cauchyseq_tendsto_of_complet": 7, "criterion": 7, "tendsto_pow_attop_nhds_0_of_lt_1": 7, "dist_le_range_sum_dist": 7, "cauchyseq_of_le_geometric_two": 7, "\u03b5_po": [7, 8], "le_iff_exists_add": 7, "boss": 7, "bair": [7, 8], "exclam": 7, "induct": [7, 11], "rec_on": 7, "ho": 7, "hd": 7, "dens": 7, "densiti": 7, "\u03b4po": 7, "hpo": 7, "hball": 7, "mem_closure_iff_nhds_basi": 7, "recon": 7, "rpo": 7, "rb": 7, "incl": 7, "cdist": 7, "ylim": 7, "yball": 7, "categor": 7, "topologicalspac": [7, 8], "isopen_univ": 7, "isopen_empti": 7, "isopen_iunion": 7, "fintyp": 7, "isopen_iint": 7, "continuous_def": 7, "attach": 7, "filteri": 7, "sent": 7, "mem_nhds_iff": 7, "digress": 7, "pure_le_nhd": 7, "eventually_eventually_nhd": 7, "topological_spac": 7, "mk_of_nhd": 7, "nhds_mk_of_nhd": 7, "functori": 7, "induc": 7, "sensibl": 7, "uncount": 7, "relatedli": 7, "coinduc": 7, "t_x": 7, "t_y": 7, "coinduced_le_iff_le_induc": 7, "covari": 7, "coinduced_compos": 7, "induced_compos": 7, "topological_structur": 7, "focus": 7, "nhd": 7, "recov": 7, "continuous_iff_coinduced_l": 7, "g_": 7, "t_z": 7, "wasn": 7, "\u03c0": [7, 8], "t_": 7, "x_i": 7, "pi": 7, "price": 7, "patholog": 7, "t2_space": 7, "hausdorff": 7, "t2space": 7, "tendsto_nhds_uniqu": 7, "regularspac": 7, "closed_nhds_basi": 7, "nhds_basis_open": 7, "denseinduc": 7, "continuousat_extend": 7, "funni": 7, "_in": 7, "nhds_induc": 7, "is_open": 7, "fortiori": 7, "f_cont": 7, "tendsto_right_iff": 7, "firstcountabletopolog": 7, "cluster": 7, "at_top": 7, "hfx": 7, "push_pul": 7, "of_map": 7, "f_ne": 7, "f_le": 7, "map_eq": 7, "hne": 7, "hle": 7, "huo": 7, "hsu": 7, "elim_finite_subcov": 7, "9": 8, "introductori": 8, "hasderivat": [8, 9], "hasderivat_sin": 8, "differentiable_at": 8, "differentiableat": 8, "inconveni": 8, "deriv_zero_of_not_differentiableat": 8, "deriv_add": 8, "islocalmin": 8, "deriv_eq_zero": 8, "ev": 8, "roll": 8, "weirder": 8, "hab": 8, "hfc": 8, "hfi": 8, "exists_deriv_eq_zero": 8, "differentiableon": 8, "exists_deriv_eq_slop": 8, "normedaddcommgroup": [8, 9], "norm_add_l": 8, "infer_inst": [8, 9], "normed_spac": 8, "normed_add_group": 8, "stipul": 8, "normedspac": [8, 9], "norm_smul": 8, "banach": [8, 9], "dimension": [8, 9], "finitedimension": [8, 9], "\ud835\udd5c": [8, 9], "nontriviallynormedfield": [8, 9], "normedfield": 8, "exists_one_lt_norm": 8, "nondiscret": 8, "continuouslinearmap": 8, "cont": 8, "map_smul": 8, "le_op_norm": 8, "hmp": 8, "op_norm_le_bound": 8, "steinhau": 8, "bounded": 8, "uniformli": 8, "nonempty_interior_of_union_of_clos": 8, "continuous_linear_map": 8, "op_norm_le_of_shel": 8, "interior_subset": 8, "interior_inter_subset": 8, "is_closed_l": 8, "hc": 8, "h\u03b5": 8, "real_norm_l": 8, "\u03b5k_po": 8, "o": 8, "normedgroup": 8, "isbigowith": 8, "isbigowith_iff": 8, "isbigo_iff_isbigowith": 8, "islittleo_iff_forall_isbigowith": 8, "hasfderivat": 8, "fderiv": 8, "fr\u00e9chet": 8, "hff": 8, "iter": 8, "multilinear": 8, "with_top": 8, "infti": 8, "cont_diff": 8, "iteratedfderiv": 8, "withtop": 8, "contdiff": 8, "contdiff_iff_continuous_differenti": 8, "stricter": 8, "hasstrictfderivat": 8, "\ud835\udd42": 8, "isrorc": 8, "contdiffat": 8, "localinvers": 8, "eventually_left_invers": 8, "eventually_right_invers": 8, "to_localinvers": 8, "hasfderivwithinat": [8, 9], "hasfderivatfilt": 8, "measuretheori": 9, "intervalintegr": 9, "integral_id": 9, "integral_one_div": 9, "differenti": [9, 11], "integral_hasstrictderivat_right": 9, "stronglymeasurableatfilt": 9, "volum": 9, "integral_eq_sub_of_hasderivat": 9, "convolut": 9, "bochner": 9, "lebesgu": 9, "measurablespac": 9, "countabl": 9, "encod": 9, "measurableset": 9, "compl": 9, "iunion": 9, "iinter": 9, "measure_eq_iinf": 9, "measure_iunion_l": 9, "hmea": 9, "hdi": 9, "pairwis": 9, "m_iunion": 9, "\u1d50": 9, "integral_add": 9, "ennreal": 9, "toreal": 9, "send": 9, "to_real": 9, "set_integral_const": 9, "domin": 9, "converg": [9, 11], "aestronglymeasur": 9, "hbound": 9, "hlim": 9, "tendsto_integral_of_dominated_converg": 9, "fubini": 9, "sigmafinit": 9, "\u03bd": 9, "integral_prod": 9, "bilinear": 9, "formula": 9, "borelspac": 9, "isaddhaarmeasur": 9, "invari": 9, "mass": 9, "compact": 9, "h_inj": 9, "det": 9, "integral_image_eq_integral_abs_det_fderiv_smul": 9, "overview": 11, "schr\u00f6der": 11, "bernstein": 11, "irrat": 11}, "objects": {}, "objtypes": {}, "objnames": {}, "titleterms": {"introduct": 0, "get": 0, "start": 0, "overview": 0, "basic": [1, 6], "calcul": 1, "prove": 1, "ident": 1, "algebra": [1, 5], "structur": [1, 5], "us": 1, "theorem": [1, 3], "lemma": 1, "more": 1, "exampl": 1, "appli": 1, "rw": 1, "fact": 1, "about": 1, "logic": 2, "implic": 2, "univers": 2, "quantifi": 2, "The": [2, 3], "existenti": 2, "negat": 2, "conjunct": 2, "bi": 2, "disjunct": 2, "sequenc": 2, "converg": [2, 7], "set": [3, 7], "function": [3, 7], "schr\u00f6der": 3, "bernstein": 3, "elementari": [4, 8, 9], "number": 4, "theori": [4, 9], "irrat": 4, "root": 4, "induct": 4, "recurs": 4, "infinit": 4, "mani": 4, "prime": 4, "defin": 5, "build": 5, "gaussian": 5, "integ": 5, "hierarchi": 6, "morphism": 6, "sub": 6, "object": 6, "topolog": 7, "filter": 7, "metric": 7, "space": [7, 8], "continu": [7, 8], "ball": 7, "open": 7, "close": 7, "compact": 7, "uniformli": 7, "complet": 7, "fundament": 7, "separ": 7, "countabl": 7, "differenti": 8, "calculu": 8, "norm": 8, "linear": 8, "map": 8, "asymptot": 8, "comparison": 8, "integr": 9, "measur": 9, "index": 10, "mathemat": 11, "lean": 11}, "envversion": {"sphinx.domains.c": 2, "sphinx.domains.changeset": 1, "sphinx.domains.citation": 1, "sphinx.domains.cpp": 6, "sphinx.domains.index": 1, "sphinx.domains.javascript": 2, "sphinx.domains.math": 2, "sphinx.domains.python": 3, "sphinx.domains.rst": 2, "sphinx.domains.std": 2, "sphinx": 56}})
mathematics_in_lean.pdf