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