b6b0a5ec - mathematics_in

Authored by: Patrick Massot
Authored at: 2023-09-19 09:14:57 -0400
Committed by: Patrick Massot
Committed at: 2023-09-19 09:14:57 -0400
Object name: b6b0a5ece1d7ce2bcd1a902015ccba87f936a587
Parent: 67f37eaf

Update mar. 19 sept. 2023 09:14:57 EDT

Changes

12 changed files (+23/-45)

MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
- @@ -108,7 +108,7 @@ theorem self_sub (a : R) : a - a = 0 := by
  theorem one_add_one_eq_two : 1 + 1 = (2 : R) := by norm_num - theorem two_mul (a : R) : 2 * a = a + a := + theorem two_mul (a : R) : 2 * a = a + a := by sorry end MyRing
MIL/C08_Topology/S02_Metric_Spaces.lean
- @@ -155,7 +155,7 @@ theorem cauchySeq_of_le_geometric_two' {u : ℕ → X}
 dist (u (N + k)) (u N) = dist (u (N + 0)) (u (N + k)) := sorry _ ≤ ∑ i in range k, dist (u (N + i)) (u (N + (i + 1))) := sorry _ ≤ ∑ i in range k, (1 / 2 : ℝ) ^ (N + i) := sorry - _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2) ^ i := sorry + _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2 : ℝ) ^ i := sorry _ ≤ 1 / 2 ^ N * 2 := sorry _ < ε := sorry
MIL/C08_Topology/S03_Topological_Spaces.lean
- @@ -104,13 +104,13 @@ example [TopologicalSpace X] {x : X} :
  theorem aux {X Y A : Type*} [TopologicalSpace X] {c : A → X} {f : A → Y} {x : X} {F : Filter Y} (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) : - ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := + ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := by sorry - example [TopologicalSpace X] [TopologicalSpace Y] [RegularSpace Y] {A : Set X} + example [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {A : Set X} (hA : ∀ x, x ∈ closure A) {f : A → Y} (f_cont : Continuous f) (hf : ∀ x : X, ∃ c : Y, Tendsto f (comap (↑) (𝓝 x)) (𝓝 c)) : - ∃ φ : X → Y, Continuous φ ∧ ∀ a : A, φ a = f a := + ∃ φ : X → Y, Continuous φ ∧ ∀ a : A, φ a = f a := by sorry #check HasBasis.tendsto_right_iff
MIL/C08_Topology/solutions/Solutions_S02_Metric_Spaces.lean
- @@ -194,7 +194,7 @@ theorem cauchySeq_of_le_geometric_two' {u : ℕ → X}
 dist (u (N + k)) (u N) = dist (u (N + 0)) (u (N + k)) := sorry _ ≤ ∑ i in range k, dist (u (N + i)) (u (N + (i + 1))) := sorry _ ≤ ∑ i in range k, (1 / 2 : ℝ) ^ (N + i) := sorry - _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2) ^ i := sorry + _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2 : ℝ) ^ i := sorry _ ≤ 1 / 2 ^ N * 2 := sorry _ < ε := sorry
MIL/C08_Topology/solutions/Solutions_S03_Topological_Spaces.lean
- @@ -112,26 +112,12 @@ example [TopologicalSpace X] {x : X} :
  theorem aux {X Y A : Type*} [TopologicalSpace X] {c : A → X} {f : A → Y} {x : X} {F : Filter Y} (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) : - ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := - sorry - - example {X Y A : Type*} [TopologicalSpace X] {c : A → X} - {f : A → Y} {x : X} {F : Filter Y} - (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) : ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := by simpa [and_assoc] using ((nhds_basis_opens' x).comap c).tendsto_left_iff.mp h V' V'_in - example [TopologicalSpace X] [TopologicalSpace Y] [RegularSpace Y] {A : Set X} + example [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {A : Set X} (hA : ∀ x, x ∈ closure A) {f : A → Y} (f_cont : Continuous f) (hf : ∀ x : X, ∃ c : Y, Tendsto f (comap (↑) (𝓝 x)) (𝓝 c)) : - ∃ φ : X → Y, Continuous φ ∧ ∀ a : A, φ a = f a := - sorry - - #check HasBasis.tendsto_right_iff - - example [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {A : Set X} (hA : ∀ x, x ∈ closure A) - {f : A → Y} (f_cont : Continuous f) - (hf : ∀ x : X, ∃ c : Y, Tendsto f (comap (↑) (𝓝 x)) (𝓝 c)) : ∃ φ : X → Y, Continuous φ ∧ ∀ a : A, φ a = f a := by choose φ hφ using hf use φ
- @@ -177,14 +163,6 @@ example {x : X} {F : Filter X} {G : Filter Y} (H : ClusterPt x F) {f : X → Y}
  (hfx : ContinuousAt f x) (hf : Tendsto f F G) : ClusterPt (f x) G := ClusterPt.map H hfx hf - example [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) {s : Set X} (hs : IsCompact s) : - IsCompact (f '' s) := by - intro F F_ne F_le - have map_eq : map f (𝓟 s ⊓ comap f F) = 𝓟 (f '' s) ⊓ F := by sorry - have Hne : (𝓟 s ⊓ comap f F).NeBot := by sorry - have Hle : 𝓟 s ⊓ comap f F ≤ 𝓟 s := inf_le_left - sorry - example [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) {s : Set X} (hs : IsCompact s) : IsCompact (f '' s) := by intro F F_ne F_le
html/C02_Basics.html
- @@ -650,7 +650,7 @@ the last section:
 <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem one_add_one_eq_two : 1 + 1 = (2 : R) := by norm_num - theorem two_mul (a : R) : 2 * a = a + a := + theorem two_mul (a : R) : 2 * a = a + a := by sorry </pre></div> </div>
html/C04_Sets_and_Functions.html
- @@ -113,9 +113,9 @@ or apply a function to arguments of the wrong type.
 Lean’s library does define elementary set-theoretic notions. In contrast to set theory, in Lean a set is always a set of objects of some type, - such as a set natural numbers or a set of functions + such as a set of natural numbers or a set of functions from real numbers to real numbers. - The distinction between types and set takes some getting used to, + The distinction between types and sets takes some getting used to, but this chapter will take you through the essentials. <div class="section" id="sets"> <h2>4.1. Sets<a class="headerlink" href="#sets" title="Permalink to this headline"></a></h2>
html/C07_Hierarchies.html
- @@ -371,7 +371,7 @@ groups, and then define rings.
 inv_mul : ∀ a : G, a⁻¹ * a = 1 </pre></div> </div> - We should remember to tagged lemmas with <code class="docutils literal notranslate">simp</code> when appropriate. + We should remember to tag lemmas with <code class="docutils literal notranslate">simp</code> when appropriate. <div class="highlight-lean notranslate"><div class="highlight"><pre>attribute [simp] Group₃.inv_mul AddGroup₃.neg_add </pre></div> </div>
html/C08_Topology.html
- @@ -792,7 +792,7 @@ a geometric context. In addition to the explanations from the filters section, y
 dist (u (N + k)) (u N) = dist (u (N + 0)) (u (N + k)) := sorry _ ≤ ∑ i in range k, dist (u (N + i)) (u (N + (i + 1))) := sorry _ ≤ ∑ i in range k, (1 / 2 : ℝ) ^ (N + i) := sorry - _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2) ^ i := sorry + _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2 : ℝ) ^ i := sorry _ ≤ 1 / 2 ^ N * 2 := sorry _ < ε := sorry </pre></div>
- @@ -1046,10 +1046,10 @@ by being a more functorial theory and having a complete lattice structure for an
 We saw that the category of topological spaces have very nice properties. The price to pay for this is existence of rather pathological topological spaces. There are a number of assumptions you can make on a topological space to ensure its behavior - is closer to what metric spaces do. The most important is <code class="docutils literal notranslate">t2_space</code>, also called “Hausdorff”, + is closer to what metric spaces do. The most important is <code class="docutils literal notranslate">T2Space</code>, also called “Hausdorff”, that will ensure that limits are unique. - A stronger separation property is regularity that ensure that each point has a basis of closed - neighborhood. + A stronger separation property is <code class="docutils literal notranslate">T3Space</code> that ensures in addition the <cite>RegularSpace</cite> property: + each point has a basis of closed neighborhoods. <div class="highlight-lean notranslate"><div class="highlight"><pre>example [TopologicalSpace X] [T2Space X] {u : ℕ → X} {a b : X} (ha : Tendsto u atTop (𝓝 a)) (hb : Tendsto u atTop (𝓝 b)) : a = b := tendsto_nhds_unique ha hb
- @@ -1068,8 +1068,8 @@ neighborhood.
 Our main goal is now to prove the basic theorem which allows extension by continuity. From Bourbaki’s general topology book, I.8.5, Theorem 1 (taking only the non-trivial implication): Let \(X\) be a topological space, \(A\) a dense subset of \(X\), \(f : A → Y\) - a continuous mapping of \(A\) into a regular space \(Y\). If, for each \(x\) in \(X\), - \(f(y)\) tends to a limit in \(Y\) when \(y\) tends to \(x\) + a continuous mapping of \(A\) into a \(T_3\) space \(Y\). If, for each \(x\) in + \(X\), \(f(y)\) tends to a limit in \(Y\) when \(y\) tends to \(x\) while remaining in \(A\) then there exists a continuous extension \(φ\) of \(f\) to \(X\). Actually Mathlib contains a more general version of the above lemma, <code class="docutils literal notranslate">DenseInducing.continuousAt_extend</code>,
- @@ -1083,7 +1083,7 @@ The assumption “tends to \(x\)<
 <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem aux {X Y A : Type*} [TopologicalSpace X] {c : A → X} {f : A → Y} {x : X} {F : Filter Y} (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) : - ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := + ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := by sorry </pre></div> </div>
- @@ -1110,10 +1110,10 @@ Because we know <code class="docutils literal notranslate">Ten
 <code class="docutils literal notranslate">φ y ∈ closure V'</code> and, since <code class="docutils literal notranslate">V'</code> is closed, we have proved <code class="docutils literal notranslate">φ y ∈ V'</code>. It remains to prove that <code class="docutils literal notranslate">φ</code> extends <code class="docutils literal notranslate">f</code>. This is were continuity of <code class="docutils literal notranslate">f</code> enters the discussion, together with the fact that <code class="docutils literal notranslate">Y</code> is Hausdorff. - <div class="highlight-lean notranslate"><div class="highlight"><pre>example [TopologicalSpace X] [TopologicalSpace Y] [RegularSpace Y] {A : Set X} + <div class="highlight-lean notranslate"><div class="highlight"><pre>example [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {A : Set X} (hA : ∀ x, x ∈ closure A) {f : A → Y} (f_cont : Continuous f) (hf : ∀ x : X, ∃ c : Y, Tendsto f (comap (↑) (𝓝 x)) (𝓝 c)) : - ∃ φ : X → Y, Continuous φ ∧ ∀ a : A, φ a = f a := + ∃ φ : X → Y, Continuous φ ∧ ∀ a : A, φ a = f a := by sorry #check HasBasis.tendsto_right_iff
html/_sources/C04_Sets_and_Functions.rst.txt
- @@ -33,9 +33,9 @@ or apply a function to arguments of the wrong type.
  Lean's library does define elementary set-theoretic notions. In contrast to set theory, in Lean a set is always a set of objects of some type, - such as a set natural numbers or a set of functions + such as a set of natural numbers or a set of functions from real numbers to real numbers. - The distinction between types and set takes some getting used to, + The distinction between types and sets takes some getting used to, but this chapter will take you through the essentials. .. include:: C04_Sets_and_Functions/S01_Sets.inc
html/searchindex.js
- @@ -1,1 +1,1 @@
 - Search.setIndex({docnames:["C01_Introduction","C02_Basics","C03_Logic","C04_Sets_and_Functions","C05_Elementary_Number_Theory","C06_Structures","C07_Hierarchies","C08_Topology","C09_Differential_Calculus","C10_Integration_and_Measure_Theory","genindex","index"],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_Topology.rst","C09_Differential_Calculus.rst","C10_Integration_and_Measure_Theory.rst","genindex.rst","index.rst"],objects:{},objnames:{},objtypes:{},terms:{"0":[0,1,2,3,4,5,6,7,8,9],"02463336":6,"1":[1,2,3,4,5,6,7,8,9],"10":2,"12":4,"15":2,"17":4,"2":[0,1,2,3,4,5,6,7,8,9],"256":7,"263":6,"27":4,"2c":4,"3":[0,1,2,3,4,5,6,7],"37":2,"4":[0,1,2,4,5,7,8],"4c":4,"5":[1,2,5,7,8],"50":6,"512":7,"6":[2,4,5,6,7,8],"64":7,"7":[2,4],"70":6,"73":6,"8":[2,4,7],"9":8,"\u00b9":[1,3,5,6,7],"\u02e2":7,"\u03b1":[1,2,3,4,5,6,7,8,9],"\u03b2":[1,2,3,5,6,7,9],"\u03b3":[1,2,5,7],"\u03b4":[2,7],"\u03b4po":7,"\u03b5":[2,7,8],"\u03b52po":2,"\u03b5_po":[7,8],"\u03b5k_po":8,"\u03b5po":[2,7],"\u03b9":[7,8,9],"\u03bc":[7,9],"\u03bd":9,"\u03c0":[7,8],"\u03c3":5,"\u03c6":7,"\u1d50":9,"\u1da0":[7,8,9],"\u2080":3,"\u2081":6,"\u2102":[1,5,8],"\u2115":[0,1,2,3,4,5,6,7,8,9],"\u211a":[1,4,7],"\u211d":[1,2,3,5,6,7,8,9],"\u2124":[1,4,5,6],"\ud835\udcdd":[7,8,9],"\ud835\udcdf":7,"\ud835\udce4":7,"\ud835\udd42":8,"\ud835\udd5c":[8,9],"\ud835\udfd9":6,"abstract":[1,2,5,6,7],"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,9],"class":[1,4,5,6,7,8,9],"commgroup\u2083":6,"commmonoid\u2083":6,"commsemigroup\u2083":6,"default":[1,2,3,4,5,6,8],"dia\u2081":6,"diaoneclass\u2081":6,"do":[0,1,2,3,4,5,6,7,8,9],"export":6,"final":[1,2,3,5,7,9],"fr\u00e9chet":8,"function":[1,2,4,5,6,8,9,11],"group\u2081":[5,6],"group\u2081cat":5,"group\u2082":5,"group\u2083":6,"h\u03b5":8,"h\u2080":[1,2,3,4,7],"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,9],"int":[5,6],"inv\u2081":6,"ismonoidhom\u2081":6,"ismonoidhom\u2082":6,"k\u00fclshammer":0,"le\u2081":6,"left_inv_eq_right_inv\u2081":6,"long":[1,2,3,5,6,8],"lt\u2081":6,"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],"nsmul\u2081":6,"one\u2081":6,"one\u2082":6,"orderedcommmonoid\u2081":6,"partialorder\u2081":6,"pos\u2080":2,"preorder\u2081":6,"return":[0,2,3,4,5,7],"ring\u2081":6,"ring\u2083":6,"ringhom\u2081":6,"ringhomclass\u2083":6,"s\u1d9c":[7,9],"s\u2081":6,"s\u2082":6,"schr\u00f6der":11,"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":7,"tendsto\u2082":7,"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,7],"try":[0,1,2,3,4,5,6,7],"while":[0,1,2,6,7],"x\u2080":[7,8],"x\u2081":[2,3,5,7],"x\u2081a":3,"x\u2082":[2,3,5],"x\u2082a":3,"x\u2082eq":3,"x\u2082na":3,"y\u2080":7,"y\u2081":5,"y\u2082":5,"z\u2080":7,"z\u2081":5,"z\u2082":5,"zsmul\u2081":6,A:[1,2,3,4,5,6,7,8],And:[2,4,6,7],As:[0,1,2,3,4,5,6,7,8,9],At:[0,1,2,4,5,6],Be:[1,3],But:[0,1,2,3,4,5,6,7],By:[1,3,5,6],For:[0,1,2,3,4,5,6,7,8,9],If:[0,1,2,3,4,5,6,7],In:[0,1,2,3,4,5,6,7,8,9],It:[0,1,2,3,4,5,6,7,8],Its:[5,6],Not:[1,5,7],Of:[1,2,4,6,7,8,9],On:[1,2,3,5,6,7,9],One:[1,2,3,4,5,6,7],Or:[2,3],Such:[0,1,2,6],That:[0,4,5,6],The:[0,1,4,5,6,7,8,9,11],Their:[7,8],Then:[2,3,5,6,7,9],There:[0,1,2,3,4,6,7,8,9],These:[0,1,3,4,5,8,9],To:[0,1,2,3,4,5,6,7],With:[1,3,4,6,7],_:[0,1,2,3,4,5,6,7,8,9],_add_mod:5,_def:4,_eq:5,_in:7,_inst_1:5,_le:5,_root_:[1,4],a_0:3,a_1:3,a_2:3,a_def:3,a_of_b_of_c:1,ab:[2,5],abandon:4,abbrevi:[1,2,3,5],abel:1,abelian:[1,5,6],abgrpmodul:6,abil:0,abl:[0,1,2,3,4,5,6,8],abn:2,about:[0,2,3,4,5,6,7,8,11],abov:[0,1,2,3,4,5,6,7,9],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,absorpt:1,abstractli:7,absurd:[2,4],abus:5,ac:5,accept:[0,1,2,7],access:[1,3,5,6,7,9],accessor:5,accommod:5,accompani:5,accord:5,achiev:[5,6,7],acknowledg:0,acpo:2,across:6,act:1,activ:0,actual:[2,3,4,6,7],ad:[1,2,3,4,5,6,7],adapt:5,add:[2,4,5,6,7,8],add_assoc:[1,4,5,6],add_comm:[1,4,5,6],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_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,add_sub:1,add_sub_cancel:4,add_x:5,add_zero:[1,5,6],addalt:5,addalt_comm:5,addalt_x:5,addcommgroup:1,addgroup:[1,5],addgrouppoint:5,addit:[1,2,4,5,6,7,8,9],addmonoid:6,addzeroclass:6,adi:5,adject:6,adopt:1,advantag:[2,3,4,5,8],ae:[7,9],aestronglymeasur:9,affect:6,aforement:7,after:[1,2,4,6,7,8],again:[1,2,3,4,5,6,7],against:2,agre:3,ai:3,aim:4,aka:7,aleb:2,alex:0,algebra:[4,6,7,8,9,11],algebrahom:6,algorithm:5,all:[0,1,2,3,4,5,6,7,8,9],allow:[1,2,3,4,5,6,7,8,9],almost:[5,6,7,9],alon:3,along:[1,4,7],alpha:[2,3],alreadi:[0,1,2,3,4,5,6,7],also:[0,1,2,3,4,5,6,7,8,9],altern:[0,2,3,4,5,6,7],although:[0,3,4,5,6,7],alwai:[0,1,2,3,5,6],ambigu:[1,5],among:4,an:[0,1,2,3,4,5,6,7,8,9],analog:[1,2,3,4,5,7,8],analysi:[0,5,8],ancient:4,and_comm:3,anecdot:6,angl:2,ani:[0,1,2,3,4,5,6,7,8,9],ann:5,annoi:[4,6],annot:[1,2,3,4,5,6],anonym:[2,3,4,5],anoth:[0,1,2,3,4,5,6,7],answer:[0,5,7],antireflex:5,antisymm:3,antisymmetr:2,anyhow:2,anyth:[2,5,7],apart:[5,6],api:1,appeal:[3,6],appear:[0,1,2,5,6,7],appli:[2,3,4,5,6,7,8,9,11],applic:[1,2,4,5,9],appreci:4,approach:[4,5,6,7],appropri:[1,2,3,5,6],approxim:1,ar:[0,1,2,3,4,5,6,7,8,9],arbitrari:[1,2,3,4,5],arbitrarili:[2,7],archetyp:5,argu:6,argument:[1,2,3,4,5,6,7],aris:2,arithmet:1,around:[1,3,6,7,9],arrang:5,arrow:[1,2,6,7],artifici:5,ascii:6,ascript:6,asid:3,ask:[2,4,5,6,7],aspect:[0,5],assembl:7,assert:[2,3,6],assign:[2,3,5,6],assist:[0,2,5],associ:[0,1,2,4,5,6,7,9],assum:[0,1,2,3,4,6,7],assumpt:[0,1,2,3,4,5,7,8,9],assur:5,asymmetri:2,attach:7,attain:7,attempt:6,attent:[1,2,4,6,7],attop:[7,9],attop_basi:7,attr:6,attract:2,attribut:6,auto:6,autom:[0,1,5],automat:[0,1,2,3,4,5,6,7,8],aux:[1,2,4,7],auxiliari:[2,7],avail:[0,1,2,4,5,6],averag:5,avoid:[1,2,3,4,5,6,8],awai:[2,5],axiom:[1,2,3,5,6,7,9],axiomat:[1,2,3,5],b:[1,2,3,4,5,6,7,8,9],baanen:5,back:[0,1,2,3,5,6,7],background:0,backslash:[1,3],backward:[2,7],bad:[5,6,7],badinst:6,bair:[7,8],balanc:1,ball:[3,8],banach:[8,9],bar:[0,1,2],bare:6,barrier:6,bartosz:0,base:[0,2,3,4,6,7,8],basi:[5,7],basic:[0,2,4,5,7,9,11],baz:1,bbb:[2,5],bc:5,bci:5,bd:5,becaus:[1,2,3,4,5,6,7,8],becom:[1,4,5,6,7],been:[0,1,2,4,5,6,8],befor:[0,1,2,3,4,5,6],begin:[1,2,3,4,5,6],begun:7,behav:[2,3,6,7],behavior:[3,6,7],behind:3,being:[1,3,5,7,8],belong:[5,6,7],below:[0,2,3,4,5,6,7,8,9],beq:2,berman:0,bernstein:11,besid:6,bespok:5,best:0,beta:[2,3],better:[3,4,5,6,7],between:[0,1,2,3,4,5,6,7,8,9],bewar:6,bex:3,bex_def:3,beyond:[2,6,8],bi:[1,2,5],big:[0,5,7,8],bigcup_:3,bigger:[0,3,8],bigoper:[4,5],biject:[3,5],bilinear:9,binari:[1,2,4,5,6],bind:[1,3],binder:6,bipartit:5,bit:[1,2,4,6,7],black:[4,6],block:[1,4],blur:7,bochner:9,boil:6,bold:2,bolt:1,book:[0,2,7],border:7,borelspac:9,boss:7,both:[1,2,3,4,5,6,7,8],bother:[1,3],bottom:[6,7],bound:[1,2,3,4,5,7,8,9],bounded:8,bounded_of_ex_finset:4,bourbaki:7,box:4,bpo:[2,7],bq:5,brace:1,bracket:[1,2,5,6],branch:[2,3,6],breviti:[1,5],bring:[3,4,7],broader:[4,8],broadest:5,brows:[0,1,4],bryan:0,build:[0,2,4,6,7,11],builder:3,built:[0,2,6],builtin:6,bulb:5,bulwi:0,bundl:[5,6,7,8],button:0,by_cas:[2,3,4],by_contra:[2,4],c:[0,1,2,4,5,6,7,8,9],cach:0,calc:[1,2,3,5,7],calcul:[0,2,4,5,11],calculu:[7,9,11],call:[0,1,2,3,4,5,6,7,8,9],can:[0,1,2,3,4,5,6,7,8,9],candid:5,cannot:[2,3,4,5,6,7],canon:[2,3,4,5],cantor:3,cap:3,capabl:5,capit:5,cardin:3,care:[1,2,3,5],carneiro:0,carri:[0,1,2,3,4,5,6,7,9],carrier:[1,5,6],categor:7,categori:[5,7,8],cauchi:7,cauchyseq:7,cauchyseq_iff:7,cauchyseq_of_le_geometric_two:7,cauchyseq_tendsto_of_complet:7,cdist:7,cdot:5,center:[0,7],central:[0,4],centuri:3,ceq:2,certain:[2,6,7],certifi:0,cha:0,chain:5,challeng:[0,1,2,3,5,8],chanc:2,chang:[0,1,2,4,5,7,9],chapter:[0,1,2,3,4,5,6,7,8],charact:[1,3,6],character:[1,3,4,7,8],chat:0,cheat:[0,1],check:[0,1,2,3,4,5,6,7],checksynthord:6,chen:0,chestnut:2,choic:[1,2,3,5,7],choos:[0,2,3,4,5,6,7],choose_spec:3,chose:6,chosen:[2,5],circ:[3,5],claim:7,clarifi:5,clash:1,classic:[2,3,4],claus:6,clean:[2,7],clear:[1,2,4,5,6],clearer:[1,3,5],clearli:7,clever:1,click:[0,1,3,4,5,6],clock:0,close:[1,2,3,6,8,9],closed_nhds_basi:7,closedbal:7,closer:[2,7],closur:7,cloud:0,clunki:7,cluster:7,clusterpt:7,cmd:[1,2],co:2,cocki:1,code:[0,1,2,3,5,6],codomain:[2,4,7],coe:6,coe_inject:6,coe_natab:5,coe_natabs_norm:5,coeffici:5,coefun:6,coerc:6,coercion:[5,6,7,8],coincid:[4,5,7],coinduc:7,coinduced_compos:7,coinduced_le_iff_le_induc:7,collari:0,collect:[1,2,3,5,7,9],collis:6,colon:2,comap:7,comap_comap:7,combin:[1,2,5,6,7],come:[0,1,2,3,4,5,6,7],comfort:0,comma:1,command:[0,1,2,3,4,5,6],commelin:0,comment:[0,4],commgroup:1,commmonoid:6,common:[1,2,3,4,5,7],commonli:[4,5],commr:[1,2,5],commun:[0,4],commut:[1,2,3,4,5,6,8],comp:7,compact:9,compactspac:7,compani:2,companion:[0,1],compar:[0,5,6,7],comparison:6,compat:[1,7],compl:9,complain:1,complement:[3,7,9],complementari:0,complet:[0,1,2,3,4,6,8],completespac:[7,8,9],complex:[0,1,2,4,5,8,9],complic:[1,2,6],compon:[2,3,5,7,9],compos:[3,5,7],composit:[2,3,5,6,7],compound:[1,2,7],compress:[0,1,7],comput:[0,2,3,4,5,8,9],computation:4,concentr:3,concept:[5,7,8],conceptu:3,concis:[1,5],conclud:[2,8],conclus:[1,2,4],concret:[1,2,4,5,6,7],condens:3,condit:[3,4,6,7,8],confid:3,configur:5,confirm:[1,2,3,4],confus:[3,4,6,7],congr:2,congratul:[1,2,4],congruent:4,conj:5,conj_im:5,conj_r:5,conjug:5,conjunct:[6,11],connect:[1,3,5,7],consid:[1,2,3,4,5,6,7,8,9],consist:[1,3,5,6,7,8],constant:[1,2,9],constitut:1,constraint:[5,7],construct:[0,2,3,4,5,6,7],constructor:[2,3,4,5,6],consult:5,cont:8,contain:[0,2,3,4,5,6,7,8,9],contdiff:8,contdiff_iff_continuous_differenti:8,contdiffat:8,contend:4,content:[0,1,2,4,7],context:[1,2,4,5,6,7,8,9],contextu:5,continu:[0,1,4,5,6,9],continuous_def:7,continuous_dist:7,continuous_fst:7,continuous_id:[6,7],continuous_iff:7,continuous_iff_coinduced_l:7,continuous_linear_map:8,continuous_pow:7,continuous_snd:7,continuousat:[7,9],continuousat_extend:7,continuousat_iff:7,continuouslinearmap:8,continuouson:[7,8],continuum:2,contract:2,contradict:[2,3,4],contradictori:2,contrapos:[2,3,4],contrari:2,contrast:[2,3,5,6,7],contravari:7,contribut:[0,3],control:2,conveni:[1,2,3,5,6,7],convent:[1,5,9],convention:7,converg:[9,11],convergesto:2,convergesto_add:2,convergesto_const:2,convergesto_mul:2,convergesto_mul_const:2,convergesto_uniqu:2,convers:[0,2,4,7],convert:[2,4],convinc:5,convolut:9,copi:[0,3,4,6,7],coprim:4,coprime_mn:4,core:[0,4,5],correct:[0,1],correctli:3,correspond:[0,1,2,3,4,5,6,7,8],could:[0,1,2,4,5,6,7],count_factors_mul_of_po:4,countabl:9,counterexampl:[2,8],counterpart:5,coupl:[1,2,6,7],cours:[1,2,4,6,7,8,9],covari:7,cover:[0,1,3,6,7,8],creat:[0,1,6],creativ:5,criterion:7,crucial:7,crude:4,cryptic:2,cs:2,ct:2,ctrl:[0,1,2,4,5],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,czubin:0,d:[1,2,4,5,8],dai:3,danger:[4,5],data:[1,2,4,5,6,7],databas:[3,4,6,7],datatyp:4,de:0,deal:[1,2,3,4,5,7],dealt:2,decid:[4,7],decidableeq:4,decidablepr:4,decis:4,declar:[0,1,4,5,6],decompos:[0,3],decreas:[1,5],dedekind:3,deduc:[6,7],def:[0,2,3,4,5,6,7],defect:[2,6,7],defin:[1,2,3,4,6,7,8,9,11],definit:[0,1,2,3,4,5,6,7,8,9],definition:[1,4,5,6,7],delet:[1,2,3,4],delic:3,delimit:1,demonstr:[6,7],deni:0,denomin:[2,4,5],denot:[1,3,4,6,7],dens:7,denseinduc:7,densiti:7,depend:[0,2,3,4,5,6,7],deriv:[1,2,4,8,9],deriv_add:8,deriv_eq_zero:8,deriv_zero_of_not_differentiableat:8,descend:6,describ:[0,1,2,3,4,5,6,7],descript:[0,1,2,4,7],deserv:4,design:[0,1,2,3,5,7],desir:[1,3,6,7],destruct:2,destructur:6,det:9,detail:[1,2,3,4,5,6],detect:2,determin:[1,5,7],develop:[0,1,4,9],devic:6,devot:7,di:[2,5],dia:6,dia_assoc:6,dia_inv:6,dia_on:6,diagram:3,diamond:6,dictionari:1,did:[0,2,6,7],dif_neg:3,dif_po:3,diff_eq:3,differ:[0,1,2,3,4,5,6,7,8],differenti:[9,11],differentiableat:8,differentiableon:8,difficult:[2,6],digress:7,dimension:[8,9],direct:[1,2,3,6,7,8],directli:[2,4,5,6,7],discret:5,discuss:[1,2,4,5,6,7,8],dishwash:0,disjoint:[3,9],disjunct:[1,3,11],dispens:4,displai:[0,1,2,6],dispos:2,dist:[1,7],dist_comm:[1,7],dist_eq_zero:7,dist_le_range_sum_dist:7,dist_nonneg:[1,7],dist_self:1,dist_triangl:[1,7],distanc:[1,2,7,8],distinct:[0,2,3,4,5,7],distinguish:[0,5,6,7,8],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],divis:[1,2,4,5,6],divisor:[1,2,4,5],document:[0,1,3,4,6],doe:[0,1,2,3,4,5,6,7,8],doesn:[1,2,7],domain:[1,2,3,4,5,7],domin:9,don:[0,1,2,3,4,5,6,7,9],done:[0,2,3,4,6,7],doorn:0,dot:[1,7],doubl:[2,3],doubt:0,down:[0,3,4,6,7],dozen:3,draw:[1,5,6],drop:2,dsimp:[2,3,4,5],dual:[5,7],dualli:7,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],each:[0,1,2,3,4,5,6,7,8],earlier:1,easi:[0,4,5,6,7],easier:[0,1,3,4,6,7],easiest:[2,4],easili:[1,4,5,6],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,7],effici:[5,7],effort:[1,4],eg:2,eight:7,either:[1,2,3,5,6,7],elabor:7,ele1:2,eleg:5,element:[1,2,3,4,5,6,7,8,9],elementari:[0,3,5,7,11],elim:2,elim_finite_subcov:7,elimin:1,els:[2,3,4],em:[2,3],emb:5,embark:6,emetricspac:7,emod_lt:5,emod_lt_of_po:5,emod_nonneg:5,emphas:6,emphasi:[0,6],empti:[3,4,5,7,9],enabl:[2,3,4,5],enat:4,encapsul:[3,5,8],encod:9,encount:[4,6],encourag:[0,1,2,3,4,5],end:[1,2,3,4,5,6,7,8],endow:6,engin:4,enjoi:[2,3,4,7],ennreal:9,enough:[0,1,2,3,4,6,7],ensur:[6,7],enter:[0,1,2,3,7],enthusiast:0,entir:[1,3,5,7,8],entourag:7,entri:[0,5],enumer:[1,2],epo:2,eq1:4,eq2:4,eq:[3,5],eq_empty_or_nonempti:7,eq_neg_of_add_eq_zero:1,eq_of_dvd_of_prim:4,eq_one_or_self_of_dvd:4,eq_two_or_odd:3,eq_univ:3,eq_univ_of_foral:3,eq_zero_or_eq_zero_of_mul_eq_zero:2,equal:[1,2,3,4,5,6,7,9],equat:[1,2,3,4,5],equilater:5,equip:[1,3,5,6,7,8,9],equiv:5,equival:[1,2,3,4,5,7,8,9],eras:4,eric:0,error:[1,2,3,6],erw:2,especi:[1,2,5,6,7],essenti:[2,3,5,7],establish:[0,1,2,3,4,5],eta:5,etc:7,euclidean:5,euclideandomain:5,eval:0,even:[0,1,2,3,4,5,6,7,8,9],even_iff:3,even_of_even_sqr:4,eventu:[2,3,7],eventually_eventually_nhd:7,eventually_left_invers:8,eventually_of_foral:7,eventually_right_invers:8,eventuallyeq:7,ever:[0,7],everi:[0,1,2,3,4,5,6,7,8,9],everyth:[1,2,6,7],everywher:[2,3,6,7,9],evid:5,evolv:1,ex:[0,2],ex_finset_of_bound:4,exact:[1,2,3,4,5,7],exactli:[1,2,3,5,6,7],exampl:[0,2,3,4,5,6,7,8,9,11],except:[1,2,5],exclam:7,exclud:[2,4],exercis:[0,1,2,3,5,6,7,8],exfalso:2,exhibit:[2,7],exist:[1,2,3,6,7],existenti:[3,11],exists_abs_le_of_convergesto:2,exists_deriv_eq_slop:8,exists_deriv_eq_zero:8,exists_forall_g:7,exists_forall_l:7,exists_infinite_prim:3,exists_one_lt_norm:8,exists_prime_and_dvd:3,exists_prime_factor:4,exists_prime_factor_mod_4_eq_3:4,exot:7,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],expend:6,experi:[0,1,7],explain:[1,2,3,4,5,6,7,9],explan:[0,7],explicit:[1,2,5,6,7],explicitli:[1,2,3,5,6,7,8],explor:[4,7],expon:1,exponenti:4,expos:[2,7],express:[0,1,2,3,4,5,6,7,8,9],ext:[2,3,4,5,6],ext_iff:5,extend:[1,3,4,5,6,7,9],extens:[0,1,6,7,8],extension:[3,5],extra:[1,2,3,5,6,7],extract:[2,7],extrem:[0,6,7],f:[0,1,2,3,4,5,6,7,8,9],f_:7,f_cont:7,f_le:7,f_ne:7,fac:4,fac_po:4,face:[5,6,7],facilit:[2,7],fact:[0,2,3,4,5,6,7,8,9,11],factor:[4,5],factori:4,factorial_po:4,factorization_mul:4,factorization_pow:4,factors_uniqu:4,fail:[1,2,3,4,5,6,7,9],failur:6,fairli:2,fall:3,fals:[1,2,3,4,6],falso:2,famili:[7,8],familiar:[0,1,4,5,7,8],famou:3,far:[2,3,6,7],favor:[1,5],fderiv:8,fear:6,feat:4,featur:[0,2,4],feedback:0,feel:[0,1,2,6,7],fermatlasttheorem:0,fetch:0,few:[1,2,3,4,7],field:[0,1,5,6,8],field_simp:[2,5],figur:[0,1,2,5],file:[0,1,4,5,6,7],fill:[2,3,4,5],filter:[4,8,9,11],filter_upward:7,filteri:7,fin:[5,9],find:[0,1,2,4,5,6,7],finicki:1,finish:[1,2,3,4],finit:[1,3,4,5,7,8,9],finitedimension:[8,9],finset:[4,5,7],fintyp:7,first:[0,1,2,3,4,5,6,7,8,9],firstcountabletopolog:7,fix:[4,6,7],fixm:5,flag:[2,3],flexibl:7,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,9],focus:7,folder:0,follow:[0,1,2,3,4,5,6,7,8,9],foo:[1,3,5],forc:[1,2,3],foreshadow:1,forewarn:0,forget:6,form:[0,1,2,3,4,5,6,7,9],formal:[0,1,2,3,4,5,6,7,8],format:1,former:5,formul:[4,7],formula:9,forth:5,fortiori:7,fortun:3,forward:[1,2,5,7],found:[1,5,8],foundat:[2,3,4,5],four:[2,5],fourth:[1,2],frac:5,fraction:4,fraenkel:2,framework:0,free:[0,1,7],freeli:4,frequent:7,friend:[2,5],from:[0,1,2,3,4,5,6,7,8,9],front:2,frustrat:[0,6],fst:[5,7],fubini:9,full:[1,2,3,4,5,6,7],fulli:[3,7],fun:[0,2,3,4,5,6,7,8,9],functori:7,fundament:[0,4,5,6,9],funlik:6,funni:7,further:[1,7],fx:3,fxeq:3,g:[1,2,3,5,6,7,8,9],g_1:5,g_2:5,g_3:5,g_:7,gabriel:0,gadget:[2,7],gain:6,galoi:[3,5,7],game:[0,6],gaussian:[2,11],gaussianint:5,gaussint:5,gave:7,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],genuin:2,geometr:7,get:[1,2,3,4,6,7,8,11],gin:0,giovanni:0,git:0,github:[0,1],gitpod:0,give:[1,2,3,4,6,7,9],given:[0,1,2,3,4,5,6,7],glb:1,global:7,go:[0,1,2,3,4,6,7],goal:[0,1,2,3,4,5,7],goe:[3,4,5,6,7],good:[1,2,3,4,5,6,7],gorbachev:0,got:6,govern:[1,5],gradual:[6,7],graph:5,grate:[0,5],great:[1,5],greater:[0,1,2,3,4,7],greatest:[1,5,7],greef:0,greek:[1,4],group:[0,1,2,3,5,6,7,8],groupcat:5,grouptheori:5,grow:[0,6],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],h_def:3,h_inj:9,ha:[0,1,2,3,4,5,6,7,8,9],hab:8,habit:6,hac:6,hack:3,had:[1,6],hal:6,half:3,hand:[1,2,3,4,5,6,7],handi:4,handl:[1,3,4,6],happen:[1,6,7],happi:0,hard:[0,1,3,5,6],harder:[2,5],harm:3,has_basi:7,hasbasi:7,hasderivat:[8,9],hasderivat_sin:8,hasfderivat:8,hasfderivatfilt:8,hasfderivwithinat:[8,9],haskel:1,hasmul:5,hasquoti:6,hasstrictfderivat:8,hausdorff:7,have:[0,1,2,3,4,5,6,7,8,9],haven:[0,2,6,7],hb:[2,7],hba:6,hball:7,hbound:9,hc:8,hd:7,hdi:9,headach:4,headi:5,heart:4,heather:5,heaven:5,heavier:6,heavili:[3,7],hello:0,help:[0,1,2,3,4,5,6,7],helper:1,henc:[0,2,3,4,5,6,7,8],here:[0,1,2,3,4,5,6,7,8,9],hesit:4,hf:[3,7,8,9],hfa:2,hfc:8,hff:8,hfi:8,hfx:7,hg:[3,7,8,9],hgb:2,hidden:2,hide:[6,7],hierarchi:[5,11],high:2,higher:6,highlight:[0,2],hint:[0,1,2,9],histor:1,hit:[0,1],hk:[0,8],hle:7,hlim:9,hm:[4,8],hmea:9,hmn:0,hmp:8,hn:[3,4,7,8],hna:2,hnb:2,hne:7,ho:7,hold:[1,2,3,4,5,7,9],home:[4,5],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,9],howev:[1,2,5,6,7,8],hp:7,hpo:7,hq:7,hr:7,hs:[2,4,7,9],hsu:7,ht:2,html:0,http:6,hu:[7,8],huge:6,hum:7,human:1,hunt:6,hunter:0,huo:7,hurdl:6,hurt:2,hux:7,hw:6,hx:[2,3,5,6,8],hxeq:3,hy:[5,6],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],icc:[7,8],ici:7,id:[4,6,7,8],idea:[1,2,3,5,6,7],ident:[3,4,5,6,7,11],identifi:[1,2,4],ie:[6,7],if_neg:3,if_po:3,iff:[1,3,7,8,9,11],ignor:[0,7],ih:4,iinter:9,il:4,illustr:[1,2,3,4,5],im:5,imag:[3,4,6,7],image_subset_iff:3,imagin:1,imaginari:5,immedi:[2,3,5,6],implement:[2,5,6,8],impli:[1,2,3,4,5,7],implic:[1,7,11],implicit:[1,2,5,6,7,8],implicitli:[1,2],importantli:6,imposs:1,impress:0,improv:[3,4],incl:7,includ:[0,1,2,3,4,6,7,8],inclus:[1,3,7],inconsist:1,inconveni:8,incorpor:6,increas:1,increment:[0,1],inde:[1,5,6,7,8],indefinit:4,indent:1,independ:[2,3,5],index:[3,6,7],indic:[1,2,3,5,6],indirect:6,indirectli:1,individu:1,induc:7,induced_compos:7,induct:[7,11],induction_on:4,inequ:[1,2,6,7],inf:[1,6,7],inf_assoc:1,inf_comm:1,inf_le_left:[1,7],inf_le_right:1,inf_sup_left:1,inf_sup_right:1,inf_sup_self:1,infer:[1,2,3,5,6],infer_inst:[8,9],inferenti:0,inferr:6,infimum:[1,6,7,9],infin:[4,7,9],infinit:[3,7,11],infix:[1,6],infixl:6,infixr:6,info:6,inform:[0,1,2,3,5,6,7],infoview:1,infrastructur:0,infti:8,ingredi:[3,5,7,8],inhabit:[3,5,7],inherit:[5,6],inherit_doc:6,inj:4,inject:[2,3,4,6,7],injf:[2,3],injg:2,injon:[3,9],inl:[2,3],inner:3,input:[1,3,7],inr:[2,3],inria:6,inscrut:[2,3],insert:[0,2,4,5,7,8],insid:[0,1,2,3],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],instanti:[2,5,6,7],instcommr:5,instead:[0,1,2,3,4,5,6,7],instruct:[0,1,2,7],intact:0,integ:[1,2,4,6,11],integr:[2,8,11],integral_add:9,integral_eq_sub_of_hasderivat:9,integral_hasstrictderivat_right:9,integral_id:9,integral_image_eq_integral_abs_det_fderiv_smul:9,integral_one_div:9,integral_prod:9,intend:[0,1,2,5],inter_def:3,inter_set:7,interact:[0,5,6,9],interchang:1,interconnect:5,interest:[1,2,3,5,6,7],interestingli:[5,8],interfac:5,interior:[5,8],interior_iinter_subset:8,interior_subset:8,intermedi:[6,7],intern:[2,5],interpret:[0,1,4,5,7],intersect:[1,3,5,6,7,9],interv:[4,7,9],interval_cas:4,intervalintegr:9,intro:[0,1,2,3,4,5,6,7],introduc:[0,1,2,3,4,7,9],introduct:[1,2,7,11],introductori:8,intuit:[3,7],inv:[5,6],inv_dia:6,inv_eq_of_dia:6,inv_eq_of_mul:6,inv_fun:3,inv_fun_eq:3,inv_mul:6,invari:9,invers:[1,3,5,6,8,9],inverse_spec:3,invert:6,invest:5,invfun:[3,5],invfun_eq:3,invis:[5,6],invok:[0,1,7],involv:[1,2,4,5,6,7],inward:2,ioo:[7,8],ipo:4,irrat:11,irration:4,irreduc:[4,5],irreducible_iff_prim:5,irreflex:2,is_addit:5,is_closed_l:8,isaddhaarmeasur:9,isaiah:0,isbigo_iff_isbigowith:8,isbigowith:8,isbigowith_iff:8,isclos:[7,8],isclosed_l:7,iscompact:7,iscompact_icc:7,iscompact_univ:7,isdomain:2,iseqv:6,islinear:5,islittleo_iff_forall_isbigowith:8,islocalmin:8,isn:[0,2,3,4,6],isomorph:[5,8],isopen:7,isopen_compl_iff:7,isopen_empti:7,isopen_iff:7,isopen_iint:7,isopen_iunion:7,isopen_univ:7,isrorc:8,issu:[4,5,6,7],item:7,iter:8,iteratedfderiv:8,its:[0,1,2,3,4,5,6,7,8,9],itself:[0,2,3,5,6,7,8],iunion:9,j:[3,5],job:1,johan:0,join:[0,1,5],journei:7,juggl:6,julian:0,jump:[1,4,5,7],just:[0,1,2,3,4,5,6,7],justif:[1,2],justifi:[0,1,2,7],k:[0,2,4,5,7,8],keep:[1,5,6],kei:[1,4,5,7],keyboard:1,keyword:[1,2,4,5],kind:[0,1,6,7],knew:7,know:[0,1,2,3,4,5,6,7,8],known:[0,1,2,3,4,5,6,7,8],l:[0,1,8,9],label:[1,2],lake:0,lambda:[2,5],lambda_l:5,lambda_nonneg:5,languag:[0,1,2,3],larg:[0,6,7],larger:[1,7],last:[1,2,3,4,5,6,7],later:[0,1,2,4,5,6,7],latter:[5,7],lattic:[1,5,6,7],law:1,layer:[6,7],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:7,le_inf:1,le_inf_iff:7,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:8,le_or_gt:2,le_principal_iff:7,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],leader:1,lean4:1,lean:[0,1,2,3,4,5,6,7,8],learn:[0,1,4,5],least:[1,5,6,7],leav:[0,1,2,3,5,6],lebesgu:9,led:6,left:[0,1,2,3,4,5,6,7,8,9],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,11],less:[1,2,3,4,5,6,7],let:[0,1,2,3,4,5,6,7,8,9],letter:[1,5,8],level:[1,2,6],leverag:7,librari:[0,1,2,3,4,5,7,8],life:[0,2],light:5,like:[0,1,2,3,4,5,6,7],lim_:7,limit:[2,6,7],linarith:[1,2,4,5],line:[0,1,2,3,4,6],linear:[1,2,5,7],linearord:2,linearorderedr:5,liner:0,linf:5,link:[5,6],list:[1,2,3,4,5],littl:[1,2,7,8],live:[0,5],ll:[0,2,4,6,7],local:[1,2,6,7,8],localinvers:8,log:[1,3,9],log_le_log:1,log_lt_log:1,logic:[0,1,3,4,5,11],logician:1,longer:[0,4,5],look:[1,2,3,4,6,7],loop:4,loss:4,lot:[0,3,5,6,7],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],m_iunion:9,mac:[1,2],macbeth:5,machineri:[5,6,7],maco:0,made:[1,2,3,5,7],magic:[2,5,6],mai:[0,1,2,3,5,6,7,8],main:[2,6,7,8],maintain:1,make:[0,1,2,3,4,5,6,7,8],manag:[0,1,4,5,7],mani:[1,2,3,5,6,7,8,9,11],manifest:[1,7],manipul:[2,5,7],manner:[2,5],manual:[0,3,4],map:[1,2,3,5,6,7],map_add:[6,8],map_eq:7,map_inv_of_inv:6,map_le_iff_le_comap:7,map_map:7,map_mono:7,map_mul:6,map_on:6,map_smul:8,map_zero:6,mapsto:[1,5],mario:0,mark:[0,1,2,6,7],marker:2,marriag:5,martin:0,mascellani:0,mass:9,master:[0,1,4],match:[1,2,5],mathbb:[3,4,5],mathcal:[5,8],mathemat:[0,1,2,3,4,5,6,7],mathematician:[4,7],mathematics_in_lean:0,mathieu:0,mathlib:[0,1,2,3,4,5,6,7,8,9],matric:[1,5],matter:[1,2],mauricio:0,max:[1,2,6,7,9],maximum:[2,4,7],mayb:6,mdvdn:4,mean:[1,2,3,4,5,6,7,8,9],meaningless:2,meant:[0,2,6],meanwhil:[1,4],measur:[0,5,7,8,11],measurableset:9,measurablespac:9,measure_eq_iinf:9,measure_iunion_l:9,measuretheori:9,mechan:[1,2,5],mediat:4,meet:[1,2,3,5],mem:3,mem_:4,mem_ball_self:7,mem_closedball_self:7,mem_closure_iff:7,mem_closure_iff_clusterpt:7,mem_closure_iff_nhds_basi:7,mem_closure_iff_seq_limit:7,mem_closure_of_tendsto:7,mem_diff:3,mem_eras:4,mem_filt:4,mem_iff:7,mem_iint:3,mem_image_of_mem:3,mem_insert:4,mem_int:4,mem_inter_iff:3,mem_iunion:3,mem_nhds_iff:7,mem_of_dvd_prod_prim:4,mem_of_tendsto:7,mem_sdiff:4,mem_setof:3,mem_union:[3,4],member:[3,7],membership:[3,4,6],mention:[2,3,5,6,7],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,8,11],metricspac:[1,7,8],mf:2,mg:2,mge2:4,mgt2:4,mid:5,middl:[0,1,2,7],midpoint:5,might:[1,2,3,4,5],mil:0,min:[1,2,7,9],min_le_left:1,min_le_right:1,mind:[1,2,5,6],mindich:0,minfac:4,minimum:7,minor:[6,8],miss:[1,3,4],mission:0,mk:[5,6,7],mkofnhd:7,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,7],modern:5,modifi:6,modu:1,modul:6,modular:1,modulo:[1,4,5],moment:[1,2,5],mono:7,monof:2,monoid:[2,3,4,6],monoidhomclass:6,monoton:[2,6,7],monro:0,monticon:0,moral:[0,5],more:[0,2,3,4,5,6,7,8,11],moreov:[0,1,4,5,7],morphism:[5,8,11],morrison:0,most:[1,2,3,4,5,6,7,9],motiv:2,move:[0,1,2,6,7],mp:[1,2,3,4,7],mpr:[1,2,5,7],much:[0,2,4,6,7,8],mul:[4,5,6,7],mul_add:[0,1,4,6],mul_assoc:[1,2,4,5,6],mul_comm:[1,2,4,5,6],mul_def:5,mul_div_cancel:[2,4],mul_im:5,mul_inv:6,mul_inv_cancel_right:5,mul_inv_rev:1,mul_le_mul:2,mul_left_comm:[0,4],mul_left_inv:[1,5],mul_left_not_lt:5,mul_lt_mul_right:2,mul_mem:6,mul_mod:4,mul_mod_right:4,mul_nonneg:1,mul_on:[1,5,6],mul_po:[1,4],mul_r:5,mul_right_inj:4,mul_right_inv:[1,5],mul_smul:6,mul_sub:1,mul_sum:5,mul_zero:[1,5,6],muloneclass:6,multilinear:8,multipl:[1,2,3,4,5,6,8],multipli:5,mulzeroclass:6,mundan:2,must:[1,5,6,7],my_fil:0,my_lemma2:2,my_lemma3:2,my_lemma4:2,my_lemma:2,my_squar:5,myab:2,mynat:4,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],n_p:7,n_q:7,na:2,naiv:[6,7],name:[1,2,3,4,5,6,7,8],namespac:[1,2,3,4,5,7],nash:0,nat:[0,1,2,3,4,5,7],natab:5,natabs_mul:5,natabs_norm_mod_lt:5,natabs_of_nonneg:5,natur:[0,1,2,3,4,5,6,7,8],nb:2,ne:[4,5],nearbi:[1,4],nearest:5,nebot:7,nebot_of_l:7,necessari:[0,2,4,5],necessarili:[1,9],need:[0,1,2,3,4,5,6,7],neg:[5,6,7,9],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_neg:1,neg_r:5,neg_zero:1,negat:[1,5,11],negsucc:6,neighborhood:7,neither:[3,5,6],neq:4,nest:[1,2],net:1,neutral:6,never:[0,6],newcom:0,next:[0,1,2,3,4,5,6,7,8],nge:2,nhd:7,nhds_basis_bal:7,nhds_basis_closedbal:7,nhds_basis_ioo_po:7,nhds_basis_open:7,nhds_induc:7,nhds_mkofnhd:7,nhds_prod_eq:7,nice:[1,2,4,6,7],nicer:[5,7],nicola:0,nineteenth:3,nna:2,nnc:2,nnez:4,nnf:2,nng:2,nnz:4,non:[1,3,6,7,9],noncomm_r:1,noncomput:[3,5],nondecreas:[2,4],nondistribut:1,nonempti:[3,7],nonempty_interior_of_iunion_of_clos:8,nonexist:2,nonneg:[1,5],nonneg_of_mul_nonneg_left:1,nontrivi:[2,3,4,5,7,8],nontriviallynormedfield:[8,9],nonzero:[2,4,5,9],nor:[3,5],norm:[2,5,7,11],norm_add_l:8,norm_conj:5,norm_eq_zero:[5,8],norm_mod_lt:5,norm_mul:[5,8],norm_nonneg:[5,8],norm_num:[1,2,4,5],norm_po:5,norm_smul:8,norm_y_po:5,normedaddcommgroup:[8,9],normedaddgroup:8,normedfield:8,normedgroup:8,normedspac:[8,9],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],note:[1,2,4,5,6,7,9],noth:[1,2,3,4,5,6],notic:[1,2,3,4,5,7],notin:3,notion:[1,2,3,4,5,7,8,9],noun:6,now:[0,1,2,3,4,5,6,7,8,9],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,11],numer:[1,4,5],nut:1,o:8,obfusc:7,object:[0,1,2,3,4,5,11],observ:[2,4,7],obtain:[1,2,4,5,7,8],obviou:[0,4,5,6],occasion:7,occur:4,occurr:1,odd:[1,2,3,4],of_le_succ:4,of_map:7,off:[2,3,4],offend:6,offer:[0,2,5,7],ofnat:6,ofnat_l:5,ofnat_lt:5,often:[0,1,2,3,4,5,6,7],og:2,old:[2,5,6],oliv:0,omit:5,onc:[1,2,3,4,5,6,7,9],one:[0,1,2,3,4,5,6,7,8,9],one_add_one_eq_two:1,one_def:5,one_dia:6,one_im:5,one_mem:6,one_mul:[1,2,5,6],one_r:5,one_smul:6,oner:1,ones:[0,1,2,3,5,9],onli:[0,1,2,3,4,5,6,7,8,9],onlin:0,op_norm_le_bound:8,op_norm_le_of_shel:8,open:[0,1,2,3,4,5,8,9],oper:[1,2,3,4,5,6,7,8],opportun:7,opposit:[6,7],optim:[6,9],option:[1,2,4,5,6,7],order:[1,2,3,4,5,6,7,8],orderedcanceladdcommmonoid:2,orderpreshom:6,orderpreshomclass:6,orderpresmonoidhom:6,ordinari:[1,2,4,5,7],ordinarili:[4,5],organ:0,organiz:1,orient:5,origin:[0,1,5],other:[1,2,3,4,5,6,7],otherwis:[1,2,3,4,5],our:[0,1,2,3,4,5,6,7,9],ourselv:[4,6],out:[0,1,2,3,4,5,6,7],outer:1,outermost:3,outlin:[1,2,4,7],outparam:6,output:1,outsid:[1,4],over:[0,1,2,3,4,5,6,7,8],overlap:6,overload:3,overview:11,own:[0,1,4,5,6],p4:4,p4eq:4,p:[0,1,2,3,4,5,6,7,9],p_1:4,p_i:[4,7],p_k:4,p_n:4,page:[0,1,4],pai:[1,2,6,7],pair:[1,2,4,5,7],pairwis:9,panel:0,paper:[2,3,5,7,9],paquet:0,paradox:7,paragraph:7,paramet:[5,6],parent:6,parenthes:[1,2,3,4],pariti:[0,4],parity_simp:0,pars:[1,3],part:[1,2,3,4,5,6,7,9],partial:[0,1,2,3,5,6],partialord:[1,2],particular:[1,2,5,6,7],partli:[1,6],pass:[1,5],past:[0,1],path:6,patholog:7,pattern:[1,2,3,5,6],payoff:5,pdf:0,pdvd:4,peel:2,pen:2,peopl:[0,1],perform:[1,2,3],perm:5,permgroup:5,permiss:1,permut:4,person:0,perspicu:2,phenomenon:3,phrase:[0,1,2,4,5],pi:7,pick:[0,6],pictur:[4,5],piec:[1,4,5,6,7],pietro:0,piotrowski:0,pitfal:3,place:[0,1,2,5,7],placehold:2,placement:4,plai:[1,3,4,6,7],plan:[1,6,7],plane:7,plausibl:3,ple:4,pltn:4,pne3:4,point:[0,1,2,3,5,6,7,8,9],pointwis:[5,7,8],polynomi:5,ponen:1,poor:6,pop:0,port:0,posit:[1,3,4,5,7,9],possibl:[1,2,3,4,5,7],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],pragmat:5,pre:2,preal:5,preced:4,precis:[1,3,7,8],precondit:7,pred:4,predecessor:4,predic:[2,3,4,6,7,8],prefer:[0,1,2,3],prefix:[4,6],preimag:[3,7],preliminari:6,prematur:6,preorder:[2,6,7],presenc:6,present:[1,2,4,7],preserv:[4,6,7],preserves_mul:5,press:0,presuppos:0,pretend:6,pretti:[2,6,7],previou:[1,2,3,5,6,7,8,9],previous:6,price:7,primari:6,primarili:[6,7],prime:[1,2,3,5,6,11],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:7,principalidealr:5,principl:[1,2,3,4,6,8],print:[0,3,4,5,9],priori:6,prioriti:5,probabl:[1,5,6,7],problem:[3,4,5,6,7],proce:[4,6],procedur:[4,6],process:3,prod:[4,7,9],prod_:4,prod_empti:4,prod_factor:4,prod_insert:4,prod_map:7,prod_mk:7,prod_po:4,prod_range_succ:4,prod_range_zero:4,produc:[2,8],product:[2,4,5,6,7,9],profici:4,program:[0,1,2],progress:[0,1,5],prohibit:7,project:[0,4,5,7],promis:[6,7],promot:1,proof:[0,1,2,3,4,5,6,7,8],prop:[0,2,3,4,5,6,7,9],propag:6,properti:[1,2,3,4,5,6,7,8,9],proposit:[0,2,3,4,5],protect:5,provabl:[1,3,6,7],prove:[0,2,3,4,5,6,7,8,9,11],provid:[0,1,2,3,4,5,6,7,8,9],proxi:5,ps:4,pseudoemetricspac:7,pseudometricspac:7,psycholog:6,pull:[0,7],pullback:7,pun:2,pure:[1,7],pure_le_nhd:7,purpos:[1,2,3,4,5,6,7],push:[2,4,7],push_neg:[2,3,4],push_pul:7,pushforward:7,put:[0,1,2,3,4,5,6,7],q:[2,4,5,6,7],qk:4,quad:5,quadrat:5,quantifi:[1,3,4,5,7,11],quantiti:7,quest:6,question:[0,4,6,7,9],quick:[4,8],quicker:0,quickli:[3,9],quirk:3,quirki:4,quit:[2,6,7],quot:[5,7],quotient:[4,5,6,7],quotient_mul_add_remainder_eq:5,quotient_zero:5,quotientmonoid:6,r:[1,2,4,5,6,7],r_wellfound:5,radiu:7,raini:3,rais:[1,4],random:6,rang:[0,2,3,4,7],rare:6,rather:[0,1,2,4,5,6,7],ration:[1,2,4,7],rb:7,rcase:[2,3,4,7],re:[4,5],reach:[2,6],read:[0,1,4,5,6,7],readabl:[1,2,3,4,7],reader:[1,7],readi:[4,6,7,8],real:[1,2,3,4,5,6,7,8,9],real_norm_l:8,realli:[1,2,3,4,6,7],reason:[0,1,2,4,5,6,7],rec_on:7,recal:[1,2,4,5,7,9],recaptur:7,recast:7,recent:5,recogn:[1,2,4,5,6,7],recommend:[0,1,3],recon:7,reconcil:2,record:[5,6],recov:7,recurs:[2,3,5,11],redefin:[5,6],reduc:[0,2,3,4,5],reduct:[2,3,5],redund:[1,5,7,9],refer:[0,1,2,4,5,6,7,8],refin:[4,8],refl:[2,3,5,6],refl_tran:5,reflect:2,reflex:[1,2],reformul:7,refus:[6,7],regiment:0,region:3,regist:[5,6],regular:[6,7],regularspac:7,rel:[3,5],relat:[1,2,3,5,6,7,8,9],relatedli:7,relationship:[3,4],relativ:3,relev:[0,1,2,4,5,6,7],reli:[1,2,3,5,7],remain:[0,1,2,3,5,6,7],remaind:[4,5],remainder_lt:5,remark:[5,6],rememb:[1,2,3,4,5,6,7],remov:[4,7],renam:0,render:[2,4],repeat:[1,4,5,6],repeatedli:[2,7],repetit:[1,6],replac:[0,1,2,3,4,6],replai:0,report:1,repositori:[0,1],repres:[0,1,2,3,4,5,6,8],represent:[3,4,5],reproduc:5,reprov:1,requir:[0,1,2,3,4,5,6,7,8,9],resolut:6,resolve_left:3,respect:[1,2,3,4,5,7],respons:[0,1],rest:[2,3,5,7],restat:[2,6],restor:6,restrict:[3,4,7],result:[0,1,2,3,4,5,6,7],retri:6,reus:6,reusabl:6,reveal:1,revers:[1,2,3,5,7],revert:[4,5],review:7,rewrit:[0,1,2,3,4,5,6,7],rewritten:3,rfl:[0,1,2,3,4,5,6,7,8,9],rich:[5,6],rid:2,right:[1,2,3,4,5,6,7,8],right_distrib:[5,6],right_inv:5,rightinvers:3,ring:[0,1,2,3,4,5,6],ringhom:6,rintro:[0,2,3,4,7],rise:[4,6],road:5,robust:[5,6],role:[4,5,7],roll:8,rolland:0,roman:5,root:[5,6,11],roughli:[2,3,4],round:[0,1,5],routin:2,rpo:7,rule:[0,2,4,5,6,7],run:0,rush:0,rw:[0,2,3,4,5,6,7,11],rwa:[3,4,5],s:[0,1,2,3,4,5,6,7,8,9],s_0:[2,3],s_1:2,s_2:2,s_:3,s_n:[2,3],sa:2,sad:7,safe:6,sai:[0,1,2,3,4,5,6,7,9],said:[0,2,4,5],sake:[1,4],salient:7,same:[0,1,2,3,4,5,6,7],satisfi:[1,3,4,5,6,7,8],save:2,saw:[1,5,6,7],sb:2,sb_aux:3,sb_fun:3,sb_inject:3,sb_right_inv:3,sb_set:3,sb_surject:3,sbaux:3,sbfun:3,sbset:3,scalar:[5,6,8],scale:3,scari:5,scheme:5,schroeder_bernstein:3,scienc:6,scientist:2,scope:[1,2,3,5],scott:0,scratch:2,script:1,search:[4,5,6],second:[0,1,2,3,4,5,6,7,9],section:[0,1,2,3,4,5,6,7,8,9],see:[0,1,2,3,4,5,6,7,8,9],seek:5,seem:[1,2,4,6,7,8],seen:[0,1,2,4,5,6,7],segment:[7,9],select:[0,7],self:6,self_of_nhd:7,self_sub:1,self_trans_symm:5,selfmodul:6,semi:6,semicolon:[2,4],semigroup:6,send:9,sens:[0,2,3,4,5,6,7,8],sensibl:7,sent:7,separ:[0,1,2,4,5],sequenc:[3,6,7,8,11],seriou:[4,6,7],serv:[1,3,4,5,9],set:[0,1,2,4,5,6,8,9,11],set_integral_const:9,set_opt:6,setco:6,setlik:6,setminu:3,setoid:6,sets_of_superset:7,setub:2,sever:[6,7,9],shade:3,shame:6,sharp:0,shift:[0,1,6,7],shorten:2,shorter:[1,3,4,7],shot:7,should:[0,1,2,3,4,5,6,7,8],shouldn:7,show:[0,1,2,3,4,5,6,7,8,9],shown:[1,5,8,9],side:[0,1,2,3,4,5,6,7,8],sight:[2,6],sigma:[5,9],sigmafinit:9,sign:7,signatur:6,signific:3,silent:[5,6],silli:6,silva:0,similar:[1,2,3,5,6,7],similarli:[2,3,4,5],simp:[0,2,3,4,5,6,7,8],simpa:[4,8],simpl:[2,4,5,6,8],simpler:6,simplex:5,simpli:[0,1,2,3,4,5,6,7],simplif:[2,3,4],simplifi:[0,2,3,4,5,7,9],sin:[2,8],sinc:[0,1,2,3,4,5,6,7],singl:[0,1,2,3,4,5,6,8],singleton:4,sinter:3,sinter_eq_biint:3,situat:[1,3,6,7],size:5,skeleton:[5,7],sketch:[2,3,4,7],skill:[0,1,2,3,4],slick:2,slight:3,slightli:[1,6,7,8],slow:7,small:[0,2,4,5,7],smaller:[3,4,7],smallest:[4,6,7],smart:4,smul:[5,6],smul_add:6,smul_distrib:5,snd:[5,7],snippet:[2,4,5],so:[0,1,2,3,4,5,6,7,8,9],solut:[0,1,4,6],solv:[0,1,2,3,4,5,6,7],some:[0,1,2,3,4,5,6,7,8],someth:[0,1,2,4,6,7],sometim:[1,2,3,4,5,6,7],somewhat:[1,3,7],somewher:7,soon:[0,2,6,7],sophist:7,sorri:[0,1,2,3,4,5,6,7,8],sort:[1,3,4],sosi:2,sosx:2,sound:[3,5,6],sourc:[2,7],space:[1,2,3,5,6,9,11],speak:[2,5,7],special:[3,4,5,6,7,9],specif:[0,1,3,4,5,6],specifi:[1,2,3,4,5,7,8,9],spell:7,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],squiggli:2,ss:3,ssubt:3,stage:[2,5,6],stai:5,stand:[1,2,5,7,8],standard:[4,5,6,7],standardsimplex:5,standardtwosimplex:5,start:[1,2,3,4,6,7,8,9,11],state:[0,1,2,3,4,6,7,8],statement:[0,1,2,3,4,5,6,7,8,9],stdsimplex:5,steep:0,steinhau:8,step:[0,1,2,3,4,5,6],stick:[1,2,7,8],still:[0,1,2,3,4,5,6,7,9],stipul:8,stop:6,store:5,stori:6,str:5,straightforward:[2,6],strang:[2,4],strategi:[1,2,4],strength:1,strengthen:[1,2,4],stretch:[4,5],strict:[1,2],stricter:8,strictli:[1,2,8],strictmono:7,strictorderedr:1,strike:[1,2],strong:[2,4],strong_induction_on:4,stronger:7,strongli:0,stronglymeasurableatfilt:9,struc:5,structur:[2,4,6,7,8,9,11],stuck:6,studi:[6,7],style:[0,1],sub:[3,7,9,11],sub_add_cancel:[1,5],sub_eq_add_neg:1,sub_self:[1,2],sub_sub:1,subgoal:2,subgroup:6,subject:5,submonoid:6,subobject:6,subproof:1,subr:6,subscript:1,subsequ:[2,4,7],subset:[1,2,3,5,7,8],subset_def:3,subset_iff:4,subspac:[1,6],substant:4,substanti:0,substitut:[0,2],subsum:4,subtl:[5,7],subtleti:6,subtract:[1,4,5],subtyp:[5,6,7],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],suffici:[4,7],suggest:[0,2,4,5,7],suitabl:[0,1,2,5,7],sum:[1,2,4,5,6,7],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,7],sup_assoc:1,sup_comm:1,sup_inf_left:1,sup_inf_right:1,sup_inf_self:1,sup_l:1,superfici:7,superscript:7,suppli:5,support:[0,1,2,3,4,5,6,7],suppos:[1,2,3,4,5,7],suppress:1,supremum:[1,4,6],sure:[0,1,2,3,5,6],surject:[2,3,7],surjf:[2,3],surjg:2,surpris:6,surprisingli:[5,6],swap:5,swapxi:5,sweet:3,symbol:[1,2,5,6],symm:[3,4,5,6,7,8],symmetr:[2,3],symmetri:[3,6],syntact:2,syntax:[0,1,2,4,6],synth:6,synthes:[5,6],synthinst:6,system:[3,4,5,6],t2_space:7,t2space:7,t:[0,1,2,3,4,5,6,7,9],t_:7,t_x:7,t_y:7,t_z:7,tab:[1,3,4],tackl:6,tactic:[0,1,2,3,4,5,6,7,8],tag:[2,3,6],take:[1,2,3,4,5,6,7,8,9],taken:[1,2],talk:[4,7,8],tantamount:[1,3],target:[1,6,7,9],task:[0,2,4,5,6,7],tauto:4,tautolog:4,teach:0,tear:6,technic:[1,5,6],techniqu:[2,7],technolog:6,tediou:[1,2,6],tell:[0,2,3,4,5,6],temporarili:[1,2],tempt:6,tend:[1,7],tendsto:[7,9],tendsto_attop:7,tendsto_congr:7,tendsto_iff:7,tendsto_integral_of_dominated_converg:9,tendsto_nhds_uniqu:7,tendsto_pow_attop_nhds_0_of_lt_1:7,tendsto_right_iff:7,tendsto_subseq:7,term:[0,1,2,3,4,5,7],terminolog:5,ters:6,test:4,text:[0,3,5,7],textbook:[0,1,2],th:4,than:[0,1,2,3,4,5,6,7,8],thank:6,thei:[0,1,2,3,4,5,6,7,8],them:[0,1,2,3,4,5,6,7],theme:3,themselv:[0,4,5],theorem:[0,2,4,5,7,8,9,11],theoret:[2,3,7],theori:[0,1,2,3,6,7,8,11],therefor:[1,4,5,7],thereof:0,thi:[0,1,2,3,4,5,6,7,8,9],thing:[0,1,2,3,4,5,6,7],think:[0,1,2,3,4,5,6,7,8],third:[1,2,3,5,7],thorough:0,those:[0,1,2,3,5,6,7,8],though:[2,3,4,5],three:[1,2,4,5,7],through:[0,1,3,4,5,6,7],thu:[1,3,4,5,7],thumb:4,tighter:[1,3],tightli:5,time:[1,4,5,6,7,8,9],timesav:1,tiresom:7,to_addit:6,to_localinvers:8,tofun:[5,6],togeth:[1,2,3,4,5,7],tomuloneclass:6,too:[0,1,3,5,6,7],tool:[0,1,5,6],top:[0,6,7,8],topic:[4,6],topolog:[1,5,6,8,11],topologicalspac:[7,8],toreal:9,total:1,tour:[7,8],trace:6,tradeoff:3,train:[1,6],tran:[2,4,5,6],trans_assoc:5,trans_refl:5,transform:[2,3],transit:[1,2,5,7],translat:[4,6,7],trap:6,treat:[2,3,5,6,7,8],tri:[1,2,4,6],triangl:[1,2,5],trick:[1,2,4,6,8],tricki:[2,3,4,6],trigger:6,tripl:3,trivial:[3,4,7],troubl:[2,3,5],truncat:4,truth:[1,4],tupl:5,turn:[2,3,4,5,6,7,8],tutori:0,twice:[0,1,7],two:[0,1,2,3,4,5,6,7,9],two_l:4,two_le_of_mod_4_eq_3:4,two_mul:1,type:[0,1,2,3,4,5,6,7,8,9],typeclass:6,typic:1,u:[2,3,5,7,9],ubf:2,ubfa:2,ubg:2,ubgb:2,ultim:0,un:3,unbundl:6,unchang:[1,2],uncom:1,uncount:7,uncurri:7,under:[5,6,7],underli:[0,1,5,6],underneath:[1,3],underscor:[1,2,3],understand:[0,2,3,4,5,6,7],understood:[4,7],unfold:[1,2,3,4,5,7],unicod:[1,3,6],unif:6,uniform:[3,7,8],uniformcontinu:7,uniformcontinuous_iff:7,uniformli:8,union:[1,3,4,5,6,8,9],union_def:3,uniqu:[1,2,3,4,5,7],unit:[5,6,7],univ:[3,7,8,9],univ_set:7,univers:[1,3,5,7,11],unknown:6,unless:[1,2,5],unlik:[3,4],unnecessari:3,unpack:[2,3],unpleas:[6,7],unrel:6,unshad:3,unspecifi:6,unsurprisingli:3,until:[1,4,6,7],up:[0,2,3,4,5,6,7],updat:0,upper:[1,2],us:[0,2,3,4,5,6,7,8,9,11],usabl:6,usag:1,user:[0,6],usual:[1,2,3,4,5,7,9],v:[2,3,5,7],val:5,valid:2,valu:[1,2,3,4,5,6,7,8,9],van:0,varepsilon:[2,7],variabl:[1,2,3,4,5,6,7,8,9],variant:[1,2,7],variat:[1,3,4,5,7,8],varieti:7,variou:[2,3,5,6,9],vastli:2,ve:[6,7],vector:[1,3,6,8],verbos:3,veri:[0,2,4,6,7,9],verifi:2,versa:[1,3],version:[0,1,2,3,4,5,6,7,8,9],vertic:[2,5],vi:5,via:7,vice:[1,3],view:[0,5,6,7],visibl:1,vocabulari:3,volum:9,vs:[0,1,2,3,5],w:[1,6],wa:[1,3],wai:[0,1,2,3,4,5,6,7,9],want:[0,1,2,3,4,5,6,7,8,9],wasn:7,we:[0,1,2,3,4,5,6,7,8,9],weak:6,weaker:[1,2],weav:5,web:[0,1,4],weight:5,weightedaverag:5,weird:[6,7],weirder:8,welcom:[0,1],well:[0,1,2,3,4,5,6,7],were:[2,4,5,7],what:[0,1,2,3,4,5,6,7],whatev:[0,2,4],whatsnew:6,when:[0,1,2,3,4,5,6,7,8],whenev:[1,2,4,5],where:[0,1,2,3,4,5,6,7,8,9],wherea:[0,1,2,3,5,7],wherebi:[5,7],whether:[1,2,3,4,6,7],which:[0,1,2,3,4,5,6,7,8,9],who:[0,7],whole:5,whose:[1,2,4,5,6,7,8],why:[0,2,4,6,7],wieser:0,window:[0,1,2,5],winston:0,wise:5,wish:7,within:[1,2,7],without:[1,2,4,5,6,7,8],withtop:8,wlog:3,won:[2,4,6,7],word:[1,2,3,4,5,7],work:[0,1,2,3,4,5,6,7,8],world:0,worri:[1,3,4,5],worth:[1,2,5],would:[1,2,3,4,5,6,7,8],wouldn:6,wrap:[6,7],write:[0,1,2,4,5,6,7,8,9],written:[1,2,3,4,5,6,7,8],wrong:3,wrote:4,x:[0,1,2,3,4,5,6,7,8,9],x_0:7,x_1:[2,3],x_2:[2,3],x_i:7,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],y_nonneg:5,yball:7,yeq:2,yet:[2,3,4,5,6,7],yield:[1,2,3,4,5,7],ylim:7,ylt:2,you:[0,1,2,3,4,5,6,7,8,9],your:[0,1,2,3,5,6,7],yourself:[2,5],ypo:3,z:[0,1,2,5,6,7,8,9],z_nonneg:5,zermelo:2,zero:[2,3,4,5,6,7,8,9],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_mul:[1,4,5,6],zero_r:5,zero_smul:6,zf:2,zlty:2,zsmul:6,zulip:[0,4]},titles:["1. Introduction","2. Basics","3. Logic","4. Sets and Functions","5. Elementary Number Theory","6. Structures","7. Hierarchies","8. Topology","9. Differential Calculus","10. Integration and Measure Theory","Index","Mathematics in Lean"],titleterms:{"function":[3,7],"schr\u00f6der":3,The:[2,3],about:1,algebra:[1,5],appli:1,asymptot:8,ball:7,basic:[1,6],bernstein:3,build:5,calcul:1,calculu:8,close:7,compact:7,comparison:8,complet:7,conjunct:2,continu:[7,8],converg:[2,7],countabl:7,defin:5,differenti:8,disjunct:2,elementari:[4,8,9],exampl:1,existenti:2,fact:1,filter:7,fundament:7,gaussian:5,get:0,hierarchi:6,ident:1,iff:2,implic:2,index:10,induct:4,infinit:4,integ:5,integr:9,introduct:0,irrat:4,lean:11,lemma:1,linear:8,logic:2,mani:4,map:8,mathemat:11,measur:9,metric:7,more:1,morphism:6,negat:2,norm:8,number:4,object:6,open:7,overview:0,prime:4,prove:1,quantifi:2,recurs:4,root:4,rw:1,separ:7,sequenc:2,set:[3,7],space:[7,8],start:0,structur:[1,5],sub:6,theorem:[1,3],theori:[4,9],topolog:7,uniformli: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_Topology","C09_Differential_Calculus","C10_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_Topology.rst","C09_Differential_Calculus.rst","C10_Integration_and_Measure_Theory.rst","genindex.rst","index.rst"],objects:{},objnames:{},objtypes:{},terms:{"0":[0,1,2,3,4,5,6,7,8,9],"02463336":6,"1":[1,2,3,4,5,6,7,8,9],"10":2,"12":4,"15":2,"17":4,"2":[0,1,2,3,4,5,6,7,8,9],"256":7,"263":6,"27":4,"2c":4,"3":[0,1,2,3,4,5,6,7],"37":2,"4":[0,1,2,4,5,7,8],"4c":4,"5":[1,2,5,7,8],"50":6,"512":7,"6":[2,4,5,6,7,8],"64":7,"7":[2,4],"70":6,"73":6,"8":[2,4,7],"9":8,"\u00b9":[1,3,5,6,7],"\u02e2":7,"\u03b1":[1,2,3,4,5,6,7,8,9],"\u03b2":[1,2,3,5,6,7,9],"\u03b3":[1,2,5,7],"\u03b4":[2,7],"\u03b4po":7,"\u03b5":[2,7,8],"\u03b52po":2,"\u03b5_po":[7,8],"\u03b5k_po":8,"\u03b5po":[2,7],"\u03b9":[7,8,9],"\u03bc":[7,9],"\u03bd":9,"\u03c0":[7,8],"\u03c3":5,"\u03c6":7,"\u1d50":9,"\u1da0":[7,8,9],"\u2080":3,"\u2081":6,"\u2102":[1,5,8],"\u2115":[0,1,2,3,4,5,6,7,8,9],"\u211a":[1,4,7],"\u211d":[1,2,3,5,6,7,8,9],"\u2124":[1,4,5,6],"\ud835\udcdd":[7,8,9],"\ud835\udcdf":7,"\ud835\udce4":7,"\ud835\udd42":8,"\ud835\udd5c":[8,9],"\ud835\udfd9":6,"abstract":[1,2,5,6,7],"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,9],"class":[1,4,5,6,7,8,9],"commgroup\u2083":6,"commmonoid\u2083":6,"commsemigroup\u2083":6,"default":[1,2,3,4,5,6,8],"dia\u2081":6,"diaoneclass\u2081":6,"do":[0,1,2,3,4,5,6,7,8,9],"export":6,"final":[1,2,3,5,7,9],"fr\u00e9chet":8,"function":[1,2,4,5,6,8,9,11],"group\u2081":[5,6],"group\u2081cat":5,"group\u2082":5,"group\u2083":6,"h\u03b5":8,"h\u2080":[1,2,3,4,7],"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,9],"int":[5,6],"inv\u2081":6,"ismonoidhom\u2081":6,"ismonoidhom\u2082":6,"k\u00fclshammer":0,"le\u2081":6,"left_inv_eq_right_inv\u2081":6,"long":[1,2,3,5,6,8],"lt\u2081":6,"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],"nsmul\u2081":6,"one\u2081":6,"one\u2082":6,"orderedcommmonoid\u2081":6,"partialorder\u2081":6,"pos\u2080":2,"preorder\u2081":6,"return":[0,2,3,4,5,7],"ring\u2081":6,"ring\u2083":6,"ringhom\u2081":6,"ringhomclass\u2083":6,"s\u1d9c":[7,9],"s\u2081":6,"s\u2082":6,"schr\u00f6der":11,"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":7,"tendsto\u2082":7,"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,7],"try":[0,1,2,3,4,5,6,7],"while":[0,1,2,6,7],"x\u2080":[7,8],"x\u2081":[2,3,5,7],"x\u2081a":3,"x\u2082":[2,3,5],"x\u2082a":3,"x\u2082eq":3,"x\u2082na":3,"y\u2080":7,"y\u2081":5,"y\u2082":5,"z\u2080":7,"z\u2081":5,"z\u2082":5,"zsmul\u2081":6,A:[1,2,3,4,5,6,7,8],And:[2,4,6,7],As:[0,1,2,3,4,5,6,7,8,9],At:[0,1,2,4,5,6],Be:[1,3],But:[0,1,2,3,4,5,6,7],By:[1,3,5,6],For:[0,1,2,3,4,5,6,7,8,9],If:[0,1,2,3,4,5,6,7],In:[0,1,2,3,4,5,6,7,8,9],It:[0,1,2,3,4,5,6,7,8],Its:[5,6],Not:[1,5,7],Of:[1,2,4,6,7,8,9],On:[1,2,3,5,6,7,9],One:[1,2,3,4,5,6,7],Or:[2,3],Such:[0,1,2,6],That:[0,4,5,6],The:[0,1,4,5,6,7,8,9,11],Their:[7,8],Then:[2,3,5,6,7,9],There:[0,1,2,3,4,6,7,8,9],These:[0,1,3,4,5,8,9],To:[0,1,2,3,4,5,6,7],With:[1,3,4,6,7],_:[0,1,2,3,4,5,6,7,8,9],_add_mod:5,_def:4,_eq:5,_in:7,_inst_1:5,_le:5,_root_:[1,4],a_0:3,a_1:3,a_2:3,a_def:3,a_of_b_of_c:1,ab:[2,5],abandon:4,abbrevi:[1,2,3,5],abel:1,abelian:[1,5,6],abgrpmodul:6,abil:0,abl:[0,1,2,3,4,5,6,8],abn:2,about:[0,2,3,4,5,6,7,8,11],abov:[0,1,2,3,4,5,6,7,9],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,absorpt:1,abstractli:7,absurd:[2,4],abus:5,ac:5,accept:[0,1,2,7],access:[1,3,5,6,7,9],accessor:5,accommod:5,accompani:5,accord:5,achiev:[5,6,7],acknowledg:0,acpo:2,across:6,act:1,activ:0,actual:[2,3,4,6,7],ad:[1,2,3,4,5,6,7],adapt:5,add:[2,4,5,6,7,8],add_assoc:[1,4,5,6],add_comm:[1,4,5,6],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_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,add_sub:1,add_sub_cancel:4,add_x:5,add_zero:[1,5,6],addalt:5,addalt_comm:5,addalt_x:5,addcommgroup:1,addgroup:[1,5],addgrouppoint:5,addit:[1,2,4,5,6,7,8,9],addmonoid:6,addzeroclass:6,adi:5,adject:6,adopt:1,advantag:[2,3,4,5,8],ae:[7,9],aestronglymeasur:9,affect:6,aforement:7,after:[1,2,4,6,7,8],again:[1,2,3,4,5,6,7],against:2,agre:3,ai:3,aim:4,aka:7,aleb:2,alex:0,algebra:[4,6,7,8,9,11],algebrahom:6,algorithm:5,all:[0,1,2,3,4,5,6,7,8,9],allow:[1,2,3,4,5,6,7,8,9],almost:[5,6,7,9],alon:3,along:[1,4,7],alpha:[2,3],alreadi:[0,1,2,3,4,5,6,7],also:[0,1,2,3,4,5,6,7,8,9],altern:[0,2,3,4,5,6,7],although:[0,3,4,5,6,7],alwai:[0,1,2,3,5,6],ambigu:[1,5],among:4,an:[0,1,2,3,4,5,6,7,8,9],analog:[1,2,3,4,5,7,8],analysi:[0,5,8],ancient:4,and_comm:3,anecdot:6,angl:2,ani:[0,1,2,3,4,5,6,7,8,9],ann:5,annoi:[4,6],annot:[1,2,3,4,5,6],anonym:[2,3,4,5],anoth:[0,1,2,3,4,5,6,7],answer:[0,5,7],antireflex:5,antisymm:3,antisymmetr:2,anyhow:2,anyth:[2,5,7],apart:[5,6],api:1,appeal:[3,6],appear:[0,1,2,5,6,7],appli:[2,3,4,5,6,7,8,9,11],applic:[1,2,4,5,9],appreci:4,approach:[4,5,6,7],appropri:[1,2,3,5,6],approxim:1,ar:[0,1,2,3,4,5,6,7,8,9],arbitrari:[1,2,3,4,5],arbitrarili:[2,7],archetyp:5,argu:6,argument:[1,2,3,4,5,6,7],aris:2,arithmet:1,around:[1,3,6,7,9],arrang:5,arrow:[1,2,6,7],artifici:5,ascii:6,ascript:6,asid:3,ask:[2,4,5,6,7],aspect:[0,5],assembl:7,assert:[2,3,6],assign:[2,3,5,6],assist:[0,2,5],associ:[0,1,2,4,5,6,7,9],assum:[0,1,2,3,4,6,7],assumpt:[0,1,2,3,4,5,7,8,9],assur:5,asymmetri:2,attach:7,attain:7,attempt:6,attent:[1,2,4,6,7],attop:[7,9],attop_basi:7,attr:6,attract:2,attribut:6,auto:6,autom:[0,1,5],automat:[0,1,2,3,4,5,6,7,8],aux:[1,2,4,7],auxiliari:[2,7],avail:[0,1,2,4,5,6],averag:5,avoid:[1,2,3,4,5,6,8],awai:[2,5],axiom:[1,2,3,5,6,7,9],axiomat:[1,2,3,5],b:[1,2,3,4,5,6,7,8,9],baanen:5,back:[0,1,2,3,5,6,7],background:0,backslash:[1,3],backward:[2,7],bad:[5,6,7],badinst:6,bair:[7,8],balanc:1,ball:[3,8],banach:[8,9],bar:[0,1,2],bare:6,barrier:6,bartosz:0,base:[0,2,3,4,6,7,8],basi:[5,7],basic:[0,2,4,5,7,9,11],baz:1,bbb:[2,5],bc:5,bci:5,bd:5,becaus:[1,2,3,4,5,6,7,8],becom:[1,4,5,6,7],been:[0,1,2,4,5,6,8],befor:[0,1,2,3,4,5,6],begin:[1,2,3,4,5,6],begun:7,behav:[2,3,6,7],behavior:[3,6,7],behind:3,being:[1,3,5,7,8],belong:[5,6,7],below:[0,2,3,4,5,6,7,8,9],beq:2,berman:0,bernstein:11,besid:6,bespok:5,best:0,beta:[2,3],better:[3,4,5,6,7],between:[0,1,2,3,4,5,6,7,8,9],bewar:6,bex:3,bex_def:3,beyond:[2,6,8],bi:[1,2,5],big:[0,5,7,8],bigcup_:3,bigger:[0,3,8],bigoper:[4,5],biject:[3,5],bilinear:9,binari:[1,2,4,5,6],bind:[1,3],binder:6,bipartit:5,bit:[1,2,4,6,7],black:[4,6],block:[1,4],blur:7,bochner:9,boil:6,bold:2,bolt:1,book:[0,2,7],border:7,borelspac:9,boss:7,both:[1,2,3,4,5,6,7,8],bother:[1,3],bottom:[6,7],bound:[1,2,3,4,5,7,8,9],bounded:8,bounded_of_ex_finset:4,bourbaki:7,box:4,bpo:[2,7],bq:5,brace:1,bracket:[1,2,5,6],branch:[2,3,6],breviti:[1,5],bring:[3,4,7],broader:[4,8],broadest:5,brows:[0,1,4],bryan:0,build:[0,2,4,6,7,11],builder:3,built:[0,2,6],builtin:6,bulb:5,bulwi:0,bundl:[5,6,7,8],button:0,by_cas:[2,3,4],by_contra:[2,4],c:[0,1,2,4,5,6,7,8,9],cach:0,calc:[1,2,3,5,7],calcul:[0,2,4,5,11],calculu:[7,9,11],call:[0,1,2,3,4,5,6,7,8,9],can:[0,1,2,3,4,5,6,7,8,9],candid:5,cannot:[2,3,4,5,6,7],canon:[2,3,4,5],cantor:3,cap:3,capabl:5,capit:5,cardin:3,care:[1,2,3,5],carneiro:0,carri:[0,1,2,3,4,5,6,7,9],carrier:[1,5,6],categor:7,categori:[5,7,8],cauchi:7,cauchyseq:7,cauchyseq_iff:7,cauchyseq_of_le_geometric_two:7,cauchyseq_tendsto_of_complet:7,cdist:7,cdot:5,center:[0,7],central:[0,4],centuri:3,ceq:2,certain:[2,6,7],certifi:0,cha:0,chain:5,challeng:[0,1,2,3,5,8],chanc:2,chang:[0,1,2,4,5,7,9],chapter:[0,1,2,3,4,5,6,7,8],charact:[1,3,6],character:[1,3,4,7,8],chat:0,cheat:[0,1],check:[0,1,2,3,4,5,6,7],checksynthord:6,chen:0,chestnut:2,choic:[1,2,3,5,7],choos:[0,2,3,4,5,6,7],choose_spec:3,chose:6,chosen:[2,5],circ:[3,5],claim:7,clarifi:5,clash:1,classic:[2,3,4],claus:6,clean:[2,7],clear:[1,2,4,5,6],clearer:[1,3,5],clearli:7,clever:1,click:[0,1,3,4,5,6],clock:0,close:[1,2,3,6,8,9],closed_nhds_basi:7,closedbal:7,closer:[2,7],closur:7,cloud:0,clunki:7,cluster:7,clusterpt:7,cmd:[1,2],co:2,cocki:1,code:[0,1,2,3,5,6],codomain:[2,4,7],coe:6,coe_inject:6,coe_natab:5,coe_natabs_norm:5,coeffici:5,coefun:6,coerc:6,coercion:[5,6,7,8],coincid:[4,5,7],coinduc:7,coinduced_compos:7,coinduced_le_iff_le_induc:7,collari:0,collect:[1,2,3,5,7,9],collis:6,colon:2,comap:7,comap_comap:7,combin:[1,2,5,6,7],come:[0,1,2,3,4,5,6,7],comfort:0,comma:1,command:[0,1,2,3,4,5,6],commelin:0,comment:[0,4],commgroup:1,commmonoid:6,common:[1,2,3,4,5,7],commonli:[4,5],commr:[1,2,5],commun:[0,4],commut:[1,2,3,4,5,6,8],comp:7,compact:9,compactspac:7,compani:2,companion:[0,1],compar:[0,5,6,7],comparison:6,compat:[1,7],compl:9,complain:1,complement:[3,7,9],complementari:0,complet:[0,1,2,3,4,6,8],completespac:[7,8,9],complex:[0,1,2,4,5,8,9],complic:[1,2,6],compon:[2,3,5,7,9],compos:[3,5,7],composit:[2,3,5,6,7],compound:[1,2,7],compress:[0,1,7],comput:[0,2,3,4,5,8,9],computation:4,concentr:3,concept:[5,7,8],conceptu:3,concis:[1,5],conclud:[2,8],conclus:[1,2,4],concret:[1,2,4,5,6,7],condens:3,condit:[3,4,6,7,8],confid:3,configur:5,confirm:[1,2,3,4],confus:[3,4,6,7],congr:2,congratul:[1,2,4],congruent:4,conj:5,conj_im:5,conj_r:5,conjug:5,conjunct:[6,11],connect:[1,3,5,7],consid:[1,2,3,4,5,6,7,8,9],consist:[1,3,5,6,7,8],constant:[1,2,9],constitut:1,constraint:[5,7],construct:[0,2,3,4,5,6,7],constructor:[2,3,4,5,6],consult:5,cont:8,contain:[0,2,3,4,5,6,7,8,9],contdiff:8,contdiff_iff_continuous_differenti:8,contdiffat:8,contend:4,content:[0,1,2,4,7],context:[1,2,4,5,6,7,8,9],contextu:5,continu:[0,1,4,5,6,9],continuous_def:7,continuous_dist:7,continuous_fst:7,continuous_id:[6,7],continuous_iff:7,continuous_iff_coinduced_l:7,continuous_linear_map:8,continuous_pow:7,continuous_snd:7,continuousat:[7,9],continuousat_extend:7,continuousat_iff:7,continuouslinearmap:8,continuouson:[7,8],continuum:2,contract:2,contradict:[2,3,4],contradictori:2,contrapos:[2,3,4],contrari:2,contrast:[2,3,5,6,7],contravari:7,contribut:[0,3],control:2,conveni:[1,2,3,5,6,7],convent:[1,5,9],convention:7,converg:[9,11],convergesto:2,convergesto_add:2,convergesto_const:2,convergesto_mul:2,convergesto_mul_const:2,convergesto_uniqu:2,convers:[0,2,4,7],convert:[2,4],convinc:5,convolut:9,copi:[0,3,4,6,7],coprim:4,coprime_mn:4,core:[0,4,5],correct:[0,1],correctli:3,correspond:[0,1,2,3,4,5,6,7,8],could:[0,1,2,4,5,6,7],count_factors_mul_of_po:4,countabl:9,counterexampl:[2,8],counterpart:5,coupl:[1,2,6,7],cours:[1,2,4,6,7,8,9],covari:7,cover:[0,1,3,6,7,8],creat:[0,1,6],creativ:5,criterion:7,crucial:7,crude:4,cryptic:2,cs:2,ct:2,ctrl:[0,1,2,4,5],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,czubin:0,d:[1,2,4,5,8],dai:3,danger:[4,5],data:[1,2,4,5,6,7],databas:[3,4,6,7],datatyp:4,de:0,deal:[1,2,3,4,5,7],dealt:2,decid:[4,7],decidableeq:4,decidablepr:4,decis:4,declar:[0,1,4,5,6],decompos:[0,3],decreas:[1,5],dedekind:3,deduc:[6,7],def:[0,2,3,4,5,6,7],defect:[2,6,7],defin:[1,2,3,4,6,7,8,9,11],definit:[0,1,2,3,4,5,6,7,8,9],definition:[1,4,5,6,7],delet:[1,2,3,4],delic:3,delimit:1,demonstr:[6,7],deni:0,denomin:[2,4,5],denot:[1,3,4,6,7],dens:7,denseinduc:7,densiti:7,depend:[0,2,3,4,5,6,7],deriv:[1,2,4,8,9],deriv_add:8,deriv_eq_zero:8,deriv_zero_of_not_differentiableat:8,descend:6,describ:[0,1,2,3,4,5,6,7],descript:[0,1,2,4,7],deserv:4,design:[0,1,2,3,5,7],desir:[1,3,6,7],destruct:2,destructur:6,det:9,detail:[1,2,3,4,5,6],detect:2,determin:[1,5,7],develop:[0,1,4,9],devic:6,devot:7,di:[2,5],dia:6,dia_assoc:6,dia_inv:6,dia_on:6,diagram:3,diamond:6,dictionari:1,did:[0,2,6,7],dif_neg:3,dif_po:3,diff_eq:3,differ:[0,1,2,3,4,5,6,7,8],differenti:[9,11],differentiableat:8,differentiableon:8,difficult:[2,6],digress:7,dimension:[8,9],direct:[1,2,3,6,7,8],directli:[2,4,5,6,7],discret:5,discuss:[1,2,4,5,6,7,8],dishwash:0,disjoint:[3,9],disjunct:[1,3,11],dispens:4,displai:[0,1,2,6],dispos:2,dist:[1,7],dist_comm:[1,7],dist_eq_zero:7,dist_le_range_sum_dist:7,dist_nonneg:[1,7],dist_self:1,dist_triangl:[1,7],distanc:[1,2,7,8],distinct:[0,2,3,4,5,7],distinguish:[0,5,6,7,8],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],divis:[1,2,4,5,6],divisor:[1,2,4,5],document:[0,1,3,4,6],doe:[0,1,2,3,4,5,6,7,8],doesn:[1,2,7],domain:[1,2,3,4,5,7],domin:9,don:[0,1,2,3,4,5,6,7,9],done:[0,2,3,4,6,7],doorn:0,dot:[1,7],doubl:[2,3],doubt:0,down:[0,3,4,6,7],dozen:3,draw:[1,5,6],drop:2,dsimp:[2,3,4,5],dual:[5,7],dualli:7,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],each:[0,1,2,3,4,5,6,7,8],earlier:1,easi:[0,4,5,6,7],easier:[0,1,3,4,6,7],easiest:[2,4],easili:[1,4,5,6],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,7],effici:[5,7],effort:[1,4],eg:2,eight:7,either:[1,2,3,5,6,7],elabor:7,ele1:2,eleg:5,element:[1,2,3,4,5,6,7,8,9],elementari:[0,3,5,7,11],elim:2,elim_finite_subcov:7,elimin:1,els:[2,3,4],em:[2,3],emb:5,embark:6,emetricspac:7,emod_lt:5,emod_lt_of_po:5,emod_nonneg:5,emphas:6,emphasi:[0,6],empti:[3,4,5,7,9],enabl:[2,3,4,5],enat:4,encapsul:[3,5,8],encod:9,encount:[4,6],encourag:[0,1,2,3,4,5],end:[1,2,3,4,5,6,7,8],endow:6,engin:4,enjoi:[2,3,4,7],ennreal:9,enough:[0,1,2,3,4,6,7],ensur:[6,7],enter:[0,1,2,3,7],enthusiast:0,entir:[1,3,5,7,8],entourag:7,entri:[0,5],enumer:[1,2],epo:2,eq1:4,eq2:4,eq:[3,5],eq_empty_or_nonempti:7,eq_neg_of_add_eq_zero:1,eq_of_dvd_of_prim:4,eq_one_or_self_of_dvd:4,eq_two_or_odd:3,eq_univ:3,eq_univ_of_foral:3,eq_zero_or_eq_zero_of_mul_eq_zero:2,equal:[1,2,3,4,5,6,7,9],equat:[1,2,3,4,5],equilater:5,equip:[1,3,5,6,7,8,9],equiv:5,equival:[1,2,3,4,5,7,8,9],eras:4,eric:0,error:[1,2,3,6],erw:2,especi:[1,2,5,6,7],essenti:[2,3,5,7],establish:[0,1,2,3,4,5],eta:5,etc:7,euclidean:5,euclideandomain:5,eval:0,even:[0,1,2,3,4,5,6,7,8,9],even_iff:3,even_of_even_sqr:4,eventu:[2,3,7],eventually_eventually_nhd:7,eventually_left_invers:8,eventually_of_foral:7,eventually_right_invers:8,eventuallyeq:7,ever:[0,7],everi:[0,1,2,3,4,5,6,7,8,9],everyth:[1,2,6,7],everywher:[2,3,6,7,9],evid:5,evolv:1,ex:[0,2],ex_finset_of_bound:4,exact:[1,2,3,4,5,7],exactli:[1,2,3,5,6,7],exampl:[0,2,3,4,5,6,7,8,9,11],except:[1,2,5],exclam:7,exclud:[2,4],exercis:[0,1,2,3,5,6,7,8],exfalso:2,exhibit:[2,7],exist:[1,2,3,6,7],existenti:[3,11],exists_abs_le_of_convergesto:2,exists_deriv_eq_slop:8,exists_deriv_eq_zero:8,exists_forall_g:7,exists_forall_l:7,exists_infinite_prim:3,exists_one_lt_norm:8,exists_prime_and_dvd:3,exists_prime_factor:4,exists_prime_factor_mod_4_eq_3:4,exot:7,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],expend:6,experi:[0,1,7],explain:[1,2,3,4,5,6,7,9],explan:[0,7],explicit:[1,2,5,6,7],explicitli:[1,2,3,5,6,7,8],explor:[4,7],expon:1,exponenti:4,expos:[2,7],express:[0,1,2,3,4,5,6,7,8,9],ext:[2,3,4,5,6],ext_iff:5,extend:[1,3,4,5,6,7,9],extens:[0,1,6,7,8],extension:[3,5],extra:[1,2,3,5,6,7],extract:[2,7],extrem:[0,6,7],f:[0,1,2,3,4,5,6,7,8,9],f_:7,f_cont:7,f_le:7,f_ne:7,fac:4,fac_po:4,face:[5,6,7],facilit:[2,7],fact:[0,2,3,4,5,6,7,8,9,11],factor:[4,5],factori:4,factorial_po:4,factorization_mul:4,factorization_pow:4,factors_uniqu:4,fail:[1,2,3,4,5,6,7,9],failur:6,fairli:2,fall:3,fals:[1,2,3,4,6],falso:2,famili:[7,8],familiar:[0,1,4,5,7,8],famou:3,far:[2,3,6,7],favor:[1,5],fderiv:8,fear:6,feat:4,featur:[0,2,4],feedback:0,feel:[0,1,2,6,7],fermatlasttheorem:0,fetch:0,few:[1,2,3,4,7],field:[0,1,5,6,8],field_simp:[2,5],figur:[0,1,2,5],file:[0,1,4,5,6,7],fill:[2,3,4,5],filter:[4,8,9,11],filter_upward:7,filteri:7,fin:[5,9],find:[0,1,2,4,5,6,7],finicki:1,finish:[1,2,3,4],finit:[1,3,4,5,7,8,9],finitedimension:[8,9],finset:[4,5,7],fintyp:7,first:[0,1,2,3,4,5,6,7,8,9],firstcountabletopolog:7,fix:[4,6,7],fixm:5,flag:[2,3],flexibl:7,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,9],focus:7,folder:0,follow:[0,1,2,3,4,5,6,7,8,9],foo:[1,3,5],forc:[1,2,3],foreshadow:1,forewarn:0,forget:6,form:[0,1,2,3,4,5,6,7,9],formal:[0,1,2,3,4,5,6,7,8],format:1,former:5,formul:[4,7],formula:9,forth:5,fortiori:7,fortun:3,forward:[1,2,5,7],found:[1,5,8],foundat:[2,3,4,5],four:[2,5],fourth:[1,2],frac:5,fraction:4,fraenkel:2,framework:0,free:[0,1,7],freeli:4,frequent:7,friend:[2,5],from:[0,1,2,3,4,5,6,7,8,9],front:2,frustrat:[0,6],fst:[5,7],fubini:9,full:[1,2,3,4,5,6,7],fulli:[3,7],fun:[0,2,3,4,5,6,7,8,9],functori:7,fundament:[0,4,5,6,9],funlik:6,funni:7,further:[1,7],fx:3,fxeq:3,g:[1,2,3,5,6,7,8,9],g_1:5,g_2:5,g_3:5,g_:7,gabriel:0,gadget:[2,7],gain:6,galoi:[3,5,7],game:[0,6],gaussian:[2,11],gaussianint:5,gaussint:5,gave:7,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],genuin:2,geometr:7,get:[1,2,3,4,6,7,8,11],gin:0,giovanni:0,git:0,github:[0,1],gitpod:0,give:[1,2,3,4,6,7,9],given:[0,1,2,3,4,5,6,7],glb:1,global:7,go:[0,1,2,3,4,6,7],goal:[0,1,2,3,4,5,7],goe:[3,4,5,6,7],good:[1,2,3,4,5,6,7],gorbachev:0,got:6,govern:[1,5],gradual:[6,7],graph:5,grate:[0,5],great:[1,5],greater:[0,1,2,3,4,7],greatest:[1,5,7],greef:0,greek:[1,4],group:[0,1,2,3,5,6,7,8],groupcat:5,grouptheori:5,grow:[0,6],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],h_def:3,h_inj:9,ha:[0,1,2,3,4,5,6,7,8,9],hab:8,habit:6,hac:6,hack:3,had:[1,6],hal:6,half:3,hand:[1,2,3,4,5,6,7],handi:4,handl:[1,3,4,6],happen:[1,6,7],happi:0,hard:[0,1,3,5,6],harder:[2,5],harm:3,has_basi:7,hasbasi:7,hasderivat:[8,9],hasderivat_sin:8,hasfderivat:8,hasfderivatfilt:8,hasfderivwithinat:[8,9],haskel:1,hasmul:5,hasquoti:6,hasstrictfderivat:8,hausdorff:7,have:[0,1,2,3,4,5,6,7,8,9],haven:[0,2,6,7],hb:[2,7],hba:6,hball:7,hbound:9,hc:8,hd:7,hdi:9,headach:4,headi:5,heart:4,heather:5,heaven:5,heavier:6,heavili:[3,7],hello:0,help:[0,1,2,3,4,5,6,7],helper:1,henc:[0,2,3,4,5,6,7,8],here:[0,1,2,3,4,5,6,7,8,9],hesit:4,hf:[3,7,8,9],hfa:2,hfc:8,hff:8,hfi:8,hfx:7,hg:[3,7,8,9],hgb:2,hidden:2,hide:[6,7],hierarchi:[5,11],high:2,higher:6,highlight:[0,2],hint:[0,1,2,9],histor:1,hit:[0,1],hk:[0,8],hle:7,hlim:9,hm:[4,8],hmea:9,hmn:0,hmp:8,hn:[3,4,7,8],hna:2,hnb:2,hne:7,ho:7,hold:[1,2,3,4,5,7,9],home:[4,5],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,9],howev:[1,2,5,6,7,8],hp:7,hpo:7,hq:7,hr:7,hs:[2,4,7,9],hsu:7,ht:2,html:0,http:6,hu:[7,8],huge:6,hum:7,human:1,hunt:6,hunter:0,huo:7,hurdl:6,hurt:2,hux:7,hw:6,hx:[2,3,5,6,8],hxeq:3,hy:[5,6],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],icc:[7,8],ici:7,id:[4,6,7,8],idea:[1,2,3,5,6,7],ident:[3,4,5,6,7,11],identifi:[1,2,4],ie:[6,7],if_neg:3,if_po:3,iff:[1,3,7,8,9,11],ignor:[0,7],ih:4,iinter:9,il:4,illustr:[1,2,3,4,5],im:5,imag:[3,4,6,7],image_subset_iff:3,imagin:1,imaginari:5,immedi:[2,3,5,6],implement:[2,5,6,8],impli:[1,2,3,4,5,7],implic:[1,7,11],implicit:[1,2,5,6,7,8],implicitli:[1,2],importantli:6,imposs:1,impress:0,improv:[3,4],incl:7,includ:[0,1,2,3,4,6,7,8],inclus:[1,3,7],inconsist:1,inconveni:8,incorpor:6,increas:1,increment:[0,1],inde:[1,5,6,7,8],indefinit:4,indent:1,independ:[2,3,5],index:[3,6,7],indic:[1,2,3,5,6],indirect:6,indirectli:1,individu:1,induc:7,induced_compos:7,induct:[7,11],induction_on:4,inequ:[1,2,6,7],inf:[1,6,7],inf_assoc:1,inf_comm:1,inf_le_left:[1,7],inf_le_right:1,inf_sup_left:1,inf_sup_right:1,inf_sup_self:1,infer:[1,2,3,5,6],infer_inst:[8,9],inferenti:0,inferr:6,infimum:[1,6,7,9],infin:[4,7,9],infinit:[3,7,11],infix:[1,6],infixl:6,infixr:6,info:6,inform:[0,1,2,3,5,6,7],infoview:1,infrastructur:0,infti:8,ingredi:[3,5,7,8],inhabit:[3,5,7],inherit:[5,6],inherit_doc:6,inj:4,inject:[2,3,4,6,7],injf:[2,3],injg:2,injon:[3,9],inl:[2,3],inner:3,input:[1,3,7],inr:[2,3],inria:6,inscrut:[2,3],insert:[0,2,4,5,7,8],insid:[0,1,2,3],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],instanti:[2,5,6,7],instcommr:5,instead:[0,1,2,3,4,5,6,7],instruct:[0,1,2,7],intact:0,integ:[1,2,4,6,11],integr:[2,8,11],integral_add:9,integral_eq_sub_of_hasderivat:9,integral_hasstrictderivat_right:9,integral_id:9,integral_image_eq_integral_abs_det_fderiv_smul:9,integral_one_div:9,integral_prod:9,intend:[0,1,2,5],inter_def:3,inter_set:7,interact:[0,5,6,9],interchang:1,interconnect:5,interest:[1,2,3,5,6,7],interestingli:[5,8],interfac:5,interior:[5,8],interior_iinter_subset:8,interior_subset:8,intermedi:[6,7],intern:[2,5],interpret:[0,1,4,5,7],intersect:[1,3,5,6,7,9],interv:[4,7,9],interval_cas:4,intervalintegr:9,intro:[0,1,2,3,4,5,6,7],introduc:[0,1,2,3,4,7,9],introduct:[1,2,7,11],introductori:8,intuit:[3,7],inv:[5,6],inv_dia:6,inv_eq_of_dia:6,inv_eq_of_mul:6,inv_fun:3,inv_fun_eq:3,inv_mul:6,invari:9,invers:[1,3,5,6,8,9],inverse_spec:3,invert:6,invest:5,invfun:[3,5],invfun_eq:3,invis:[5,6],invok:[0,1,7],involv:[1,2,4,5,6,7],inward:2,ioo:[7,8],ipo:4,irrat:11,irration:4,irreduc:[4,5],irreducible_iff_prim:5,irreflex:2,is_addit:5,is_closed_l:8,isaddhaarmeasur:9,isaiah:0,isbigo_iff_isbigowith:8,isbigowith:8,isbigowith_iff:8,isclos:[7,8],isclosed_l:7,iscompact:7,iscompact_icc:7,iscompact_univ:7,isdomain:2,iseqv:6,islinear:5,islittleo_iff_forall_isbigowith:8,islocalmin:8,isn:[0,2,3,4,6],isomorph:[5,8],isopen:7,isopen_compl_iff:7,isopen_empti:7,isopen_iff:7,isopen_iint:7,isopen_iunion:7,isopen_univ:7,isrorc:8,issu:[4,5,6,7],item:7,iter:8,iteratedfderiv:8,its:[0,1,2,3,4,5,6,7,8,9],itself:[0,2,3,5,6,7,8],iunion:9,j:[3,5],job:1,johan:0,join:[0,1,5],journei:7,juggl:6,julian:0,jump:[1,4,5,7],just:[0,1,2,3,4,5,6,7],justif:[1,2],justifi:[0,1,2,7],k:[0,2,4,5,7,8],keep:[1,5,6],kei:[1,4,5,7],keyboard:1,keyword:[1,2,4,5],kind:[0,1,6,7],knew:7,know:[0,1,2,3,4,5,6,7,8],known:[0,1,2,3,4,5,6,7,8],l:[0,1,8,9],label:[1,2],lake:0,lambda:[2,5],lambda_l:5,lambda_nonneg:5,languag:[0,1,2,3],larg:[0,6,7],larger:[1,7],last:[1,2,3,4,5,6,7],later:[0,1,2,4,5,6,7],latter:[5,7],lattic:[1,5,6,7],law:1,layer:[6,7],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:7,le_inf:1,le_inf_iff:7,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:8,le_or_gt:2,le_principal_iff:7,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],leader:1,lean4:1,lean:[0,1,2,3,4,5,6,7,8],learn:[0,1,4,5],least:[1,5,6,7],leav:[0,1,2,3,5,6],lebesgu:9,led:6,left:[0,1,2,3,4,5,6,7,8,9],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,11],less:[1,2,3,4,5,6,7],let:[0,1,2,3,4,5,6,7,8,9],letter:[1,5,8],level:[1,2,6],leverag:7,librari:[0,1,2,3,4,5,7,8],life:[0,2],light:5,like:[0,1,2,3,4,5,6,7],lim_:7,limit:[2,6,7],linarith:[1,2,4,5],line:[0,1,2,3,4,6],linear:[1,2,5,7],linearord:2,linearorderedr:5,liner:0,linf:5,link:[5,6],list:[1,2,3,4,5],littl:[1,2,7,8],live:[0,5],ll:[0,2,4,6,7],local:[1,2,6,7,8],localinvers:8,log:[1,3,9],log_le_log:1,log_lt_log:1,logic:[0,1,3,4,5,11],logician:1,longer:[0,4,5],look:[1,2,3,4,6,7],loop:4,loss:4,lot:[0,3,5,6,7],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],m_iunion:9,mac:[1,2],macbeth:5,machineri:[5,6,7],maco:0,made:[1,2,3,5,7],magic:[2,5,6],mai:[0,1,2,3,5,6,7,8],main:[2,6,7,8],maintain:1,make:[0,1,2,3,4,5,6,7,8],manag:[0,1,4,5,7],mani:[1,2,3,5,6,7,8,9,11],manifest:[1,7],manipul:[2,5,7],manner:[2,5],manual:[0,3,4],map:[1,2,3,5,6,7],map_add:[6,8],map_eq:7,map_inv_of_inv:6,map_le_iff_le_comap:7,map_map:7,map_mono:7,map_mul:6,map_on:6,map_smul:8,map_zero:6,mapsto:[1,5],mario:0,mark:[0,1,2,6,7],marker:2,marriag:5,martin:0,mascellani:0,mass:9,master:[0,1,4],match:[1,2,5],mathbb:[3,4,5],mathcal:[5,8],mathemat:[0,1,2,3,4,5,6,7],mathematician:[4,7],mathematics_in_lean:0,mathieu:0,mathlib:[0,1,2,3,4,5,6,7,8,9],matric:[1,5],matter:[1,2],mauricio:0,max:[1,2,6,7,9],maximum:[2,4,7],mayb:6,mdvdn:4,mean:[1,2,3,4,5,6,7,8,9],meaningless:2,meant:[0,2,6],meanwhil:[1,4],measur:[0,5,7,8,11],measurableset:9,measurablespac:9,measure_eq_iinf:9,measure_iunion_l:9,measuretheori:9,mechan:[1,2,5],mediat:4,meet:[1,2,3,5],mem:3,mem_:4,mem_ball_self:7,mem_closedball_self:7,mem_closure_iff:7,mem_closure_iff_clusterpt:7,mem_closure_iff_nhds_basi:7,mem_closure_iff_seq_limit:7,mem_closure_of_tendsto:7,mem_diff:3,mem_eras:4,mem_filt:4,mem_iff:7,mem_iint:3,mem_image_of_mem:3,mem_insert:4,mem_int:4,mem_inter_iff:3,mem_iunion:3,mem_nhds_iff:7,mem_of_dvd_prod_prim:4,mem_of_tendsto:7,mem_sdiff:4,mem_setof:3,mem_union:[3,4],member:[3,7],membership:[3,4,6],mention:[2,3,5,6,7],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,8,11],metricspac:[1,7,8],mf:2,mg:2,mge2:4,mgt2:4,mid:5,middl:[0,1,2,7],midpoint:5,might:[1,2,3,4,5],mil:0,min:[1,2,7,9],min_le_left:1,min_le_right:1,mind:[1,2,5,6],mindich:0,minfac:4,minimum:7,minor:[6,8],miss:[1,3,4],mission:0,mk:[5,6,7],mkofnhd:7,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,7],modern:5,modifi:6,modu:1,modul:6,modular:1,modulo:[1,4,5],moment:[1,2,5],mono:7,monof:2,monoid:[2,3,4,6],monoidhomclass:6,monoton:[2,6,7],monro:0,monticon:0,moral:[0,5],more:[0,2,3,4,5,6,7,8,11],moreov:[0,1,4,5,7],morphism:[5,8,11],morrison:0,most:[1,2,3,4,5,6,7,9],motiv:2,move:[0,1,2,6,7],mp:[1,2,3,4,7],mpr:[1,2,5,7],much:[0,2,4,6,7,8],mul:[4,5,6,7],mul_add:[0,1,4,6],mul_assoc:[1,2,4,5,6],mul_comm:[1,2,4,5,6],mul_def:5,mul_div_cancel:[2,4],mul_im:5,mul_inv:6,mul_inv_cancel_right:5,mul_inv_rev:1,mul_le_mul:2,mul_left_comm:[0,4],mul_left_inv:[1,5],mul_left_not_lt:5,mul_lt_mul_right:2,mul_mem:6,mul_mod:4,mul_mod_right:4,mul_nonneg:1,mul_on:[1,5,6],mul_po:[1,4],mul_r:5,mul_right_inj:4,mul_right_inv:[1,5],mul_smul:6,mul_sub:1,mul_sum:5,mul_zero:[1,5,6],muloneclass:6,multilinear:8,multipl:[1,2,3,4,5,6,8],multipli:5,mulzeroclass:6,mundan:2,must:[1,5,6,7],my_fil:0,my_lemma2:2,my_lemma3:2,my_lemma4:2,my_lemma:2,my_squar:5,myab:2,mynat:4,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],n_p:7,n_q:7,na:2,naiv:[6,7],name:[1,2,3,4,5,6,7,8],namespac:[1,2,3,4,5,7],nash:0,nat:[0,1,2,3,4,5,7],natab:5,natabs_mul:5,natabs_norm_mod_lt:5,natabs_of_nonneg:5,natur:[0,1,2,3,4,5,6,7,8],nb:2,ne:[4,5],nearbi:[1,4],nearest:5,nebot:7,nebot_of_l:7,necessari:[0,2,4,5],necessarili:[1,9],need:[0,1,2,3,4,5,6,7],neg:[5,6,7,9],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_neg:1,neg_r:5,neg_zero:1,negat:[1,5,11],negsucc:6,neighborhood:7,neither:[3,5,6],neq:4,nest:[1,2],net:1,neutral:6,never:[0,6],newcom:0,next:[0,1,2,3,4,5,6,7,8],nge:2,nhd:7,nhds_basis_bal:7,nhds_basis_closedbal:7,nhds_basis_ioo_po:7,nhds_basis_open:7,nhds_induc:7,nhds_mkofnhd:7,nhds_prod_eq:7,nice:[1,2,4,6,7],nicer:[5,7],nicola:0,nineteenth:3,nna:2,nnc:2,nnez:4,nnf:2,nng:2,nnz:4,non:[1,3,6,7,9],noncomm_r:1,noncomput:[3,5],nondecreas:[2,4],nondistribut:1,nonempti:[3,7],nonempty_interior_of_iunion_of_clos:8,nonexist:2,nonneg:[1,5],nonneg_of_mul_nonneg_left:1,nontrivi:[2,3,4,5,7,8],nontriviallynormedfield:[8,9],nonzero:[2,4,5,9],nor:[3,5],norm:[2,5,7,11],norm_add_l:8,norm_conj:5,norm_eq_zero:[5,8],norm_mod_lt:5,norm_mul:[5,8],norm_nonneg:[5,8],norm_num:[1,2,4,5],norm_po:5,norm_smul:8,norm_y_po:5,normedaddcommgroup:[8,9],normedaddgroup:8,normedfield:8,normedgroup:8,normedspac:[8,9],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],note:[1,2,4,5,6,7,9],noth:[1,2,3,4,5,6],notic:[1,2,3,4,5,7],notin:3,notion:[1,2,3,4,5,7,8,9],noun:6,now:[0,1,2,3,4,5,6,7,8,9],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,11],numer:[1,4,5],nut:1,o:8,obfusc:7,object:[0,1,2,3,4,5,11],observ:[2,4,7],obtain:[1,2,4,5,7,8],obviou:[0,4,5,6],occasion:7,occur:4,occurr:1,odd:[1,2,3,4],of_le_succ:4,of_map:7,off:[2,3,4],offend:6,offer:[0,2,5,7],ofnat:6,ofnat_l:5,ofnat_lt:5,often:[0,1,2,3,4,5,6,7],og:2,old:[2,5,6],oliv:0,omit:5,onc:[1,2,3,4,5,6,7,9],one:[0,1,2,3,4,5,6,7,8,9],one_add_one_eq_two:1,one_def:5,one_dia:6,one_im:5,one_mem:6,one_mul:[1,2,5,6],one_r:5,one_smul:6,oner:1,ones:[0,1,2,3,5,9],onli:[0,1,2,3,4,5,6,7,8,9],onlin:0,op_norm_le_bound:8,op_norm_le_of_shel:8,open:[0,1,2,3,4,5,8,9],oper:[1,2,3,4,5,6,7,8],opportun:7,opposit:[6,7],optim:[6,9],option:[1,2,4,5,6,7],order:[1,2,3,4,5,6,7,8],orderedcanceladdcommmonoid:2,orderpreshom:6,orderpreshomclass:6,orderpresmonoidhom:6,ordinari:[1,2,4,5,7],ordinarili:[4,5],organ:0,organiz:1,orient:5,origin:[0,1,5],other:[1,2,3,4,5,6,7],otherwis:[1,2,3,4,5],our:[0,1,2,3,4,5,6,7,9],ourselv:[4,6],out:[0,1,2,3,4,5,6,7],outer:1,outermost:3,outlin:[1,2,4,7],outparam:6,output:1,outsid:[1,4],over:[0,1,2,3,4,5,6,7,8],overlap:6,overload:3,overview:11,own:[0,1,4,5,6],p4:4,p4eq:4,p:[0,1,2,3,4,5,6,7,9],p_1:4,p_i:[4,7],p_k:4,p_n:4,page:[0,1,4],pai:[1,2,6,7],pair:[1,2,4,5,7],pairwis:9,panel:0,paper:[2,3,5,7,9],paquet:0,paradox:7,paragraph:7,paramet:[5,6],parent:6,parenthes:[1,2,3,4],pariti:[0,4],parity_simp:0,pars:[1,3],part:[1,2,3,4,5,6,7,9],partial:[0,1,2,3,5,6],partialord:[1,2],particular:[1,2,5,6,7],partli:[1,6],pass:[1,5],past:[0,1],path:6,patholog:7,pattern:[1,2,3,5,6],payoff:5,pdf:0,pdvd:4,peel:2,pen:2,peopl:[0,1],perform:[1,2,3],perm:5,permgroup:5,permiss:1,permut:4,person:0,perspicu:2,phenomenon:3,phrase:[0,1,2,4,5],pi:7,pick:[0,6],pictur:[4,5],piec:[1,4,5,6,7],pietro:0,piotrowski:0,pitfal:3,place:[0,1,2,5,7],placehold:2,placement:4,plai:[1,3,4,6,7],plan:[1,6,7],plane:7,plausibl:3,ple:4,pltn:4,pne3:4,point:[0,1,2,3,5,6,7,8,9],pointwis:[5,7,8],polynomi:5,ponen:1,poor:6,pop:0,port:0,posit:[1,3,4,5,7,9],possibl:[1,2,3,4,5,7],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],pragmat:5,pre:2,preal:5,preced:4,precis:[1,3,7,8],precondit:7,pred:4,predecessor:4,predic:[2,3,4,6,7,8],prefer:[0,1,2,3],prefix:[4,6],preimag:[3,7],preliminari:6,prematur:6,preorder:[2,6,7],presenc:6,present:[1,2,4,7],preserv:[4,6,7],preserves_mul:5,press:0,presuppos:0,pretend:6,pretti:[2,6,7],previou:[1,2,3,5,6,7,8,9],previous:6,price:7,primari:6,primarili:[6,7],prime:[1,2,3,5,6,11],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:7,principalidealr:5,principl:[1,2,3,4,6,8],print:[0,3,4,5,9],priori:6,prioriti:5,probabl:[1,5,6,7],problem:[3,4,5,6,7],proce:[4,6],procedur:[4,6],process:3,prod:[4,7,9],prod_:4,prod_empti:4,prod_factor:4,prod_insert:4,prod_map:7,prod_mk:7,prod_po:4,prod_range_succ:4,prod_range_zero:4,produc:[2,8],product:[2,4,5,6,7,9],profici:4,program:[0,1,2],progress:[0,1,5],prohibit:7,project:[0,4,5,7],promis:[6,7],promot:1,proof:[0,1,2,3,4,5,6,7,8],prop:[0,2,3,4,5,6,7,9],propag:6,properti:[1,2,3,4,5,6,7,8,9],proposit:[0,2,3,4,5],protect:5,provabl:[1,3,6,7],prove:[0,2,3,4,5,6,7,8,9,11],provid:[0,1,2,3,4,5,6,7,8,9],proxi:5,ps:4,pseudoemetricspac:7,pseudometricspac:7,psycholog:6,pull:[0,7],pullback:7,pun:2,pure:[1,7],pure_le_nhd:7,purpos:[1,2,3,4,5,6,7],push:[2,4,7],push_neg:[2,3,4],push_pul:7,pushforward:7,put:[0,1,2,3,4,5,6,7],q:[2,4,5,6,7],qk:4,quad:5,quadrat:5,quantifi:[1,3,4,5,7,11],quantiti:7,quest:6,question:[0,4,6,7,9],quick:[4,8],quicker:0,quickli:[3,9],quirk:3,quirki:4,quit:[2,6,7],quot:[5,7],quotient:[4,5,6,7],quotient_mul_add_remainder_eq:5,quotient_zero:5,quotientmonoid:6,r:[1,2,4,5,6,7],r_wellfound:5,radiu:7,raini:3,rais:[1,4],random:6,rang:[0,2,3,4,7],rare:6,rather:[0,1,2,4,5,6,7],ration:[1,2,4,7],rb:7,rcase:[2,3,4,7],re:[4,5],reach:[2,6],read:[0,1,4,5,6,7],readabl:[1,2,3,4,7],reader:[1,7],readi:[4,6,7,8],real:[1,2,3,4,5,6,7,8,9],real_norm_l:8,realli:[1,2,3,4,6,7],reason:[0,1,2,4,5,6,7],rec_on:7,recal:[1,2,4,5,7,9],recaptur:7,recast:7,recent:5,recogn:[1,2,4,5,6,7],recommend:[0,1,3],recon:7,reconcil:2,record:[5,6],recov:7,recurs:[2,3,5,11],redefin:[5,6],reduc:[0,2,3,4,5],reduct:[2,3,5],redund:[1,5,7,9],refer:[0,1,2,4,5,6,7,8],refin:[4,8],refl:[2,3,5,6],refl_tran:5,reflect:2,reflex:[1,2],reformul:7,refus:[6,7],regiment:0,region:3,regist:[5,6],regular:[6,7],regularspac:7,rel:[3,5],relat:[1,2,3,5,6,7,8,9],relatedli:7,relationship:[3,4],relativ:3,relev:[0,1,2,4,5,6,7],reli:[1,2,3,5,7],remain:[0,1,2,3,5,6,7],remaind:[4,5],remainder_lt:5,remark:[5,6],rememb:[1,2,3,4,5,6,7],remov:[4,7],renam:0,render:[2,4],repeat:[1,4,5,6],repeatedli:[2,7],repetit:[1,6],replac:[0,1,2,3,4,6],replai:0,report:1,repositori:[0,1],repres:[0,1,2,3,4,5,6,8],represent:[3,4,5],reproduc:5,reprov:1,requir:[0,1,2,3,4,5,6,7,8,9],resolut:6,resolve_left:3,respect:[1,2,3,4,5,7],respons:[0,1],rest:[2,3,5,7],restat:[2,6],restor:6,restrict:[3,4,7],result:[0,1,2,3,4,5,6,7],retri:6,reus:6,reusabl:6,reveal:1,revers:[1,2,3,5,7],revert:[4,5],review:7,rewrit:[0,1,2,3,4,5,6,7],rewritten:3,rfl:[0,1,2,3,4,5,6,7,8,9],rich:[5,6],rid:2,right:[1,2,3,4,5,6,7,8],right_distrib:[5,6],right_inv:5,rightinvers:3,ring:[0,1,2,3,4,5,6],ringhom:6,rintro:[0,2,3,4,7],rise:[4,6],road:5,robust:[5,6],role:[4,5,7],roll:8,rolland:0,roman:5,root:[5,6,11],roughli:[2,3,4],round:[0,1,5],routin:2,rpo:7,rule:[0,2,4,5,6,7],run:0,rush:0,rw:[0,2,3,4,5,6,7,11],rwa:[3,4,5],s:[0,1,2,3,4,5,6,7,8,9],s_0:[2,3],s_1:2,s_2:2,s_:3,s_n:[2,3],sa:2,sad:7,safe:6,sai:[0,1,2,3,4,5,6,7,9],said:[0,2,4,5],sake:[1,4],salient:7,same:[0,1,2,3,4,5,6,7],satisfi:[1,3,4,5,6,7,8],save:2,saw:[1,5,6,7],sb:2,sb_aux:3,sb_fun:3,sb_inject:3,sb_right_inv:3,sb_set:3,sb_surject:3,sbaux:3,sbfun:3,sbset:3,scalar:[5,6,8],scale:3,scari:5,scheme:5,schroeder_bernstein:3,scienc:6,scientist:2,scope:[1,2,3,5],scott:0,scratch:2,script:1,search:[4,5,6],second:[0,1,2,3,4,5,6,7,9],section:[0,1,2,3,4,5,6,7,8,9],see:[0,1,2,3,4,5,6,7,8,9],seek:5,seem:[1,2,4,6,7,8],seen:[0,1,2,4,5,6,7],segment:[7,9],select:[0,7],self:6,self_of_nhd:7,self_sub:1,self_trans_symm:5,selfmodul:6,semi:6,semicolon:[2,4],semigroup:6,send:9,sens:[0,2,3,4,5,6,7,8],sensibl:7,sent:7,separ:[0,1,2,4,5],sequenc:[3,6,7,8,11],seriou:[4,6,7],serv:[1,3,4,5,9],set:[0,1,2,4,5,6,8,9,11],set_integral_const:9,set_opt:6,setco:6,setlik:6,setminu:3,setoid:6,sets_of_superset:7,setub:2,sever:[6,7,9],shade:3,shame:6,sharp:0,shift:[0,1,6,7],shorten:2,shorter:[1,3,4,7],shot:7,should:[0,1,2,3,4,5,6,7,8],shouldn:7,show:[0,1,2,3,4,5,6,7,8,9],shown:[1,5,8,9],side:[0,1,2,3,4,5,6,7,8],sight:[2,6],sigma:[5,9],sigmafinit:9,sign:7,signatur:6,signific:3,silent:[5,6],silli:6,silva:0,similar:[1,2,3,5,6,7],similarli:[2,3,4,5],simp:[0,2,3,4,5,6,7,8],simpa:[4,8],simpl:[2,4,5,6,8],simpler:6,simplex:5,simpli:[0,1,2,3,4,5,6,7],simplif:[2,3,4],simplifi:[0,2,3,4,5,7,9],sin:[2,8],sinc:[0,1,2,3,4,5,6,7],singl:[0,1,2,3,4,5,6,8],singleton:4,sinter:3,sinter_eq_biint:3,situat:[1,3,6,7],size:5,skeleton:[5,7],sketch:[2,3,4,7],skill:[0,1,2,3,4],slick:2,slight:3,slightli:[1,6,7,8],slow:7,small:[0,2,4,5,7],smaller:[3,4,7],smallest:[4,6,7],smart:4,smul:[5,6],smul_add:6,smul_distrib:5,snd:[5,7],snippet:[2,4,5],so:[0,1,2,3,4,5,6,7,8,9],solut:[0,1,4,6],solv:[0,1,2,3,4,5,6,7],some:[0,1,2,3,4,5,6,7,8],someth:[0,1,2,4,6,7],sometim:[1,2,3,4,5,6,7],somewhat:[1,3,7],somewher:7,soon:[0,2,6,7],sophist:7,sorri:[0,1,2,3,4,5,6,7,8],sort:[1,3,4],sosi:2,sosx:2,sound:[3,5,6],sourc:[2,7],space:[1,2,3,5,6,9,11],speak:[2,5,7],special:[3,4,5,6,7,9],specif:[0,1,3,4,5,6],specifi:[1,2,3,4,5,7,8,9],spell:7,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],squiggli:2,ss:3,ssubt:3,stage:[2,5,6],stai:5,stand:[1,2,5,7,8],standard:[4,5,6,7],standardsimplex:5,standardtwosimplex:5,start:[1,2,3,4,6,7,8,9,11],state:[0,1,2,3,4,6,7,8],statement:[0,1,2,3,4,5,6,7,8,9],stdsimplex:5,steep:0,steinhau:8,step:[0,1,2,3,4,5,6],stick:[1,2,7,8],still:[0,1,2,3,4,5,6,7,9],stipul:8,stop:6,store:5,stori:6,str:5,straightforward:[2,6],strang:[2,4],strategi:[1,2,4],strength:1,strengthen:[1,2,4],stretch:[4,5],strict:[1,2],stricter:8,strictli:[1,2,8],strictmono:7,strictorderedr:1,strike:[1,2],strong:[2,4],strong_induction_on:4,stronger:7,strongli:0,stronglymeasurableatfilt:9,struc:5,structur:[2,4,6,7,8,9,11],stuck:6,studi:[6,7],style:[0,1],sub:[3,7,9,11],sub_add_cancel:[1,5],sub_eq_add_neg:1,sub_self:[1,2],sub_sub:1,subgoal:2,subgroup:6,subject:5,submonoid:6,subobject:6,subproof:1,subr:6,subscript:1,subsequ:[2,4,7],subset:[1,2,3,5,7,8],subset_def:3,subset_iff:4,subspac:[1,6],substant:4,substanti:0,substitut:[0,2],subsum:4,subtl:[5,7],subtleti:6,subtract:[1,4,5],subtyp:[5,6,7],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],suffici:[4,7],suggest:[0,2,4,5,7],suitabl:[0,1,2,5,7],sum:[1,2,4,5,6,7],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,7],sup_assoc:1,sup_comm:1,sup_inf_left:1,sup_inf_right:1,sup_inf_self:1,sup_l:1,superfici:7,superscript:7,suppli:5,support:[0,1,2,3,4,5,6,7],suppos:[1,2,3,4,5,7],suppress:1,supremum:[1,4,6],sure:[0,1,2,3,5,6],surject:[2,3,7],surjf:[2,3],surjg:2,surpris:6,surprisingli:[5,6],swap:5,swapxi:5,sweet:3,symbol:[1,2,5,6],symm:[3,4,5,6,7,8],symmetr:[2,3],symmetri:[3,6],syntact:2,syntax:[0,1,2,4,6],synth:6,synthes:[5,6],synthinst:6,system:[3,4,5,6],t2space:7,t3space:7,t:[0,1,2,3,4,5,6,7,9],t_3:7,t_:7,t_x:7,t_y:7,t_z:7,tab:[1,3,4],tackl:6,tactic:[0,1,2,3,4,5,6,7,8],tag:[2,3,6],take:[1,2,3,4,5,6,7,8,9],taken:[1,2],talk:[4,7,8],tantamount:[1,3],target:[1,6,7,9],task:[0,2,4,5,6,7],tauto:4,tautolog:4,teach:0,tear:6,technic:[1,5,6],techniqu:[2,7],technolog:6,tediou:[1,2,6],tell:[0,2,3,4,5,6],temporarili:[1,2],tempt:6,tend:[1,7],tendsto:[7,9],tendsto_attop:7,tendsto_congr:7,tendsto_iff:7,tendsto_integral_of_dominated_converg:9,tendsto_nhds_uniqu:7,tendsto_pow_attop_nhds_0_of_lt_1:7,tendsto_right_iff:7,tendsto_subseq:7,term:[0,1,2,3,4,5,7],terminolog:5,ters:6,test:4,text:[0,3,5,7],textbook:[0,1,2],th:4,than:[0,1,2,3,4,5,6,7,8],thank:6,thei:[0,1,2,3,4,5,6,7,8],them:[0,1,2,3,4,5,6,7],theme:3,themselv:[0,4,5],theorem:[0,2,4,5,7,8,9,11],theoret:[2,3,7],theori:[0,1,2,3,6,7,8,11],therefor:[1,4,5,7],thereof:0,thi:[0,1,2,3,4,5,6,7,8,9],thing:[0,1,2,3,4,5,6,7],think:[0,1,2,3,4,5,6,7,8],third:[1,2,3,5,7],thorough:0,those:[0,1,2,3,5,6,7,8],though:[2,3,4,5],three:[1,2,4,5,7],through:[0,1,3,4,5,6,7],thu:[1,3,4,5,7],thumb:4,tighter:[1,3],tightli:5,time:[1,4,5,6,7,8,9],timesav:1,tiresom:7,to_addit:6,to_localinvers:8,tofun:[5,6],togeth:[1,2,3,4,5,7],tomuloneclass:6,too:[0,1,3,5,6,7],tool:[0,1,5,6],top:[0,6,7,8],topic:[4,6],topolog:[1,5,6,8,11],topologicalspac:[7,8],toreal:9,total:1,tour:[7,8],trace:6,tradeoff:3,train:[1,6],tran:[2,4,5,6],trans_assoc:5,trans_refl:5,transform:[2,3],transit:[1,2,5,7],translat:[4,6,7],trap:6,treat:[2,3,5,6,7,8],tri:[1,2,4,6],triangl:[1,2,5],trick:[1,2,4,6,8],tricki:[2,3,4,6],trigger:6,tripl:3,trivial:[3,4,7],troubl:[2,3,5],truncat:4,truth:[1,4],tupl:5,turn:[2,3,4,5,6,7,8],tutori:0,twice:[0,1,7],two:[0,1,2,3,4,5,6,7,9],two_l:4,two_le_of_mod_4_eq_3:4,two_mul:1,type:[0,1,2,3,4,5,6,7,8,9],typeclass:6,typic:1,u:[2,3,5,7,9],ubf:2,ubfa:2,ubg:2,ubgb:2,ultim:0,un:3,unbundl:6,unchang:[1,2],uncom:1,uncount:7,uncurri:7,under:[5,6,7],underli:[0,1,5,6],underneath:[1,3],underscor:[1,2,3],understand:[0,2,3,4,5,6,7],understood:[4,7],unfold:[1,2,3,4,5,7],unicod:[1,3,6],unif:6,uniform:[3,7,8],uniformcontinu:7,uniformcontinuous_iff:7,uniformli:8,union:[1,3,4,5,6,8,9],union_def:3,uniqu:[1,2,3,4,5,7],unit:[5,6,7],univ:[3,7,8,9],univ_set:7,univers:[1,3,5,7,11],unknown:6,unless:[1,2,5],unlik:[3,4],unnecessari:3,unpack:[2,3],unpleas:[6,7],unrel:6,unshad:3,unspecifi:6,unsurprisingli:3,until:[1,4,6,7],up:[0,2,3,4,5,6,7],updat:0,upper:[1,2],us:[0,2,3,4,5,6,7,8,9,11],usabl:6,usag:1,user:[0,6],usual:[1,2,3,4,5,7,9],v:[2,3,5,7],val:5,valid:2,valu:[1,2,3,4,5,6,7,8,9],van:0,varepsilon:[2,7],variabl:[1,2,3,4,5,6,7,8,9],variant:[1,2,7],variat:[1,3,4,5,7,8],varieti:7,variou:[2,3,5,6,9],vastli:2,ve:[6,7],vector:[1,3,6,8],verbos:3,veri:[0,2,4,6,7,9],verifi:2,versa:[1,3],version:[0,1,2,3,4,5,6,7,8,9],vertic:[2,5],vi:5,via:7,vice:[1,3],view:[0,5,6,7],visibl:1,vocabulari:3,volum:9,vs:[0,1,2,3,5],w:[1,6],wa:[1,3],wai:[0,1,2,3,4,5,6,7,9],want:[0,1,2,3,4,5,6,7,8,9],wasn:7,we:[0,1,2,3,4,5,6,7,8,9],weak:6,weaker:[1,2],weav:5,web:[0,1,4],weight:5,weightedaverag:5,weird:[6,7],weirder:8,welcom:[0,1],well:[0,1,2,3,4,5,6,7],were:[2,4,5,7],what:[0,1,2,3,4,5,6,7],whatev:[0,2,4],whatsnew:6,when:[0,1,2,3,4,5,6,7,8],whenev:[1,2,4,5],where:[0,1,2,3,4,5,6,7,8,9],wherea:[0,1,2,3,5,7],wherebi:[5,7],whether:[1,2,3,4,6,7],which:[0,1,2,3,4,5,6,7,8,9],who:[0,7],whole:5,whose:[1,2,4,5,6,7,8],why:[0,2,4,6,7],wieser:0,window:[0,1,2,5],winston:0,wise:5,wish:7,within:[1,2,7],without:[1,2,4,5,6,7,8],withtop:8,wlog:3,won:[2,4,6,7],word:[1,2,3,4,5,7],work:[0,1,2,3,4,5,6,7,8],world:0,worri:[1,3,4,5],worth:[1,2,5],would:[1,2,3,4,5,6,7,8],wouldn:6,wrap:[6,7],write:[0,1,2,4,5,6,7,8,9],written:[1,2,3,4,5,6,7,8],wrong:3,wrote:4,x:[0,1,2,3,4,5,6,7,8,9],x_0:7,x_1:[2,3],x_2:[2,3],x_i:7,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],y_nonneg:5,yball:7,yeq:2,yet:[2,3,4,5,6,7],yield:[1,2,3,4,5,7],ylim:7,ylt:2,you:[0,1,2,3,4,5,6,7,8,9],your:[0,1,2,3,5,6,7],yourself:[2,5],ypo:3,z:[0,1,2,5,6,7,8,9],z_nonneg:5,zermelo:2,zero:[2,3,4,5,6,7,8,9],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_mul:[1,4,5,6],zero_r:5,zero_smul:6,zf:2,zlty:2,zsmul:6,zulip:[0,4]},titles:["1. Introduction","2. Basics","3. Logic","4. Sets and Functions","5. Elementary Number Theory","6. Structures","7. Hierarchies","8. Topology","9. Differential Calculus","10. Integration and Measure Theory","Index","Mathematics in Lean"],titleterms:{"function":[3,7],"schr\u00f6der":3,The:[2,3],about:1,algebra:[1,5],appli:1,asymptot:8,ball:7,basic:[1,6],bernstein:3,build:5,calcul:1,calculu:8,close:7,compact:7,comparison:8,complet:7,conjunct:2,continu:[7,8],converg:[2,7],countabl:7,defin:5,differenti:8,disjunct:2,elementari:[4,8,9],exampl:1,existenti:2,fact:1,filter:7,fundament:7,gaussian:5,get:0,hierarchi:6,ident:1,iff:2,implic:2,index:10,induct:4,infinit:4,integ:5,integr:9,introduct:0,irrat:4,lean:11,lemma:1,linear:8,logic:2,mani:4,map:8,mathemat:11,measur:9,metric:7,more:1,morphism:6,negat:2,norm:8,number:4,object:6,open:7,overview:0,prime:4,prove:1,quantifi:2,recurs:4,root:4,rw:1,separ:7,sequenc:2,set:[3,7],space:[7,8],start:0,structur:[1,5],sub:6,theorem:[1,3],theori:[4,9],topolog:7,uniformli:7,univers:2,us:1}})
mathematics_in_lean.pdf