45b50b91 - mathematics_in

Authored by: Patrick Massot
Authored at: 2024-10-21 10:05:25 +0200
Committed by: Patrick Massot
Committed at: 2024-10-21 10:05:25 +0200
Object name: 45b50b91c7bddb8b518f40eb128b04360e6ee59c
Parent: 36b7d4a6

Update lun. 21 oct. 2024 10:05:25 CEST

Changes

5 changed files (+3/-21)

MIL/C09_Linear_Algebra/S01_Vector_Spaces.lean
- @@ -18,15 +18,6 @@ example (a b : K) (u : V) : (a + b) • u = a • u + b • u :=
  example (a b : K) (u : V) : a • b • u = b • a • u := smul_comm a b u - def mkVectorSpace {K X : Type*} [Field K] [AddCommGroup X] (ρ : K →+* AddMonoid.End X) : Module K X where - smul a x := ρ a x - one_smul x := show ρ 1 x = x by simp - mul_smul a b x := show ρ (a * b) _ = _ by rw [map_mul]; rfl - smul_zero x := map_zero .. - smul_add a x y := map_add .. - add_smul a b x := show ρ (a + b) _ = _ by rw [map_add]; rfl - zero_smul x := show ρ 0 _ = _ by simp - example {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] : Module (Ideal R) (Submodule R M) := inferInstance
html/C06_Structures.html
- @@ -377,8 +377,8 @@ how to sum over it.
 As an exercise, see if you can define the weighted average of two points in the standard \(n\)-simplex. You can use <code class="docutils literal notranslate">Finset.sum_add_distrib</code> - and <code class="docutils literal notranslate">Finset.mul_sum</code> to manipulate the relevant sums. - We have seen that structures can be used to bundle together data + and <code class="docutils literal notranslate">Finset.mul_sum</code> to manipulate the relevant sums. + We have seen that structures can be used to bundle together data and properties. Interestingly, they can also be used to bundle together properties without the data.
html/C09_Linear_Algebra.html
- @@ -154,15 +154,6 @@ multiplication is abbreviated <cite>smul</cite> in lemma names.
 example (a b : K) (u : V) : a • b • u = b • a • u := smul_comm a b u - - def mkVectorSpace {K X : Type*} [Field K] [AddCommGroup X] (ρ : K →+* AddMonoid.End X) : Module K X where - smul a x := ρ a x - one_smul x := show ρ 1 x = x by simp - mul_smul a b x := show ρ (a * b) _ = _ by rw [map_mul]; rfl - smul_zero x := map_zero .. - smul_add a x y := map_add .. - add_smul a b x := show ρ (a + b) _ = _ by rw [map_add]; rfl - zero_smul x := show ρ 0 _ = _ by simp </pre></div> </div> As a quick note for more advanced readers, let us point out that, as suggested by
html/searchindex.js
- @@ -1,1 +1,1 @@
 - Search.setIndex({"alltitles": {"Algebraic Structures": [[5, "algebraic-structures"]], "Algebras and polynomials": [[7, "algebras-and-polynomials"]], "Asymptotic comparisons": [[10, "asymptotic-comparisons"]], "Balls, open sets and closed sets": [[9, "balls-open-sets-and-closed-sets"]], "Bases": [[8, "bases"]], "Basics": [[1, null], [6, "basics"]], "Building the Gaussian Integers": [[5, "building-the-gaussian-integers"]], "Calculating": [[1, "calculating"]], "Compactness": [[9, "compactness"], [9, "id5"]], "Complete lattice structure and internal direct sums": [[8, "complete-lattice-structure-and-internal-direct-sums"]], "Completeness": [[9, "completeness"]], "Concrete groups": [[7, "concrete-groups"]], "Conjunction and Iff": [[2, "conjunction-and-iff"]], "Continuous linear maps": [[10, "continuous-linear-maps"]], "Convergence and continuity": [[9, "convergence-and-continuity"]], "Defining structures": [[5, "defining-structures"]], "Differentiability": [[10, "differentiability"]], "Differential Calculus": [[10, null]], "Differential Calculus in Normed Spaces": [[10, "differential-calculus-in-normed-spaces"]], "Dimension": [[8, "dimension"]], "Disjunction": [[2, "disjunction"]], "Elementary Differential Calculus": [[10, "elementary-differential-calculus"]], "Elementary Integration": [[11, "elementary-integration"]], "Elementary Number Theory": [[4, null]], "Endomorphisms": [[8, "endomorphisms"]], "Filters": [[9, "filters"]], "Functions": [[3, "functions"]], "Fundamentals": [[9, "fundamentals"]], "Getting Started": [[0, "getting-started"]], "Group actions": [[7, "group-actions"]], "Groups and Rings": [[7, null]], "Groups and their morphisms": [[7, "groups-and-their-morphisms"]], "Hierarchies": [[6, null]], "Ideals and quotients": [[7, "ideals-and-quotients"]], "Implication and the Universal Quantifier": [[2, "implication-and-the-universal-quantifier"]], "Index": [[12, null]], "Induction and Recursion": [[4, "induction-and-recursion"]], "Infinitely Many Primes": [[4, "infinitely-many-primes"]], "Integration": [[11, "integration"]], "Integration and Measure Theory": [[11, null]], "Introduction": [[0, null]], "Irrational Roots": [[4, "irrational-roots"]], "Linear algebra": [[8, null]], "Linear maps": [[8, "linear-maps"]], "Logic": [[2, null]], "Mathematics in Lean": [[13, null]], "Matrices": [[8, "matrices"]], "Matrices, bases and dimension": [[8, "matrices-bases-and-dimension"]], "Measure Theory": [[11, "measure-theory"]], "Metric spaces": [[9, "metric-spaces"]], "Monoids and Groups": [[7, "monoids-and-groups"]], "Monoids and their morphisms": [[7, "monoids-and-their-morphisms"]], "More examples using apply and rw": [[1, "more-examples-using-apply-and-rw"]], "Morphisms": [[6, "morphisms"]], "Negation": [[2, "negation"]], "Normed spaces": [[10, "id3"]], "Overview": [[0, "overview"]], "Proving Facts about Algebraic Structures": [[1, "proving-facts-about-algebraic-structures"]], "Proving Identities in Algebraic Structures": [[1, "proving-identities-in-algebraic-structures"]], "Pushing and pulling subspaces": [[8, "pushing-and-pulling-subspaces"]], "Quotient groups": [[7, "quotient-groups"]], "Quotient spaces": [[8, "quotient-spaces"]], "Rings": [[7, "rings"]], "Rings, their units, morphisms and subrings": [[7, "rings-their-units-morphisms-and-subrings"]], "Separation and countability": [[9, "separation-and-countability"]], "Sequences and Convergence": [[2, "sequences-and-convergence"]], "Sets": [[3, "sets"]], "Sets and Functions": [[3, null]], "Structures": [[5, null]], "Sub-objects": [[6, "sub-objects"]], "Subgroups": [[7, "subgroups"]], "Subspace spanned by a set": [[8, "subspace-spanned-by-a-set"]], "Subspaces": [[8, "subspaces"]], "Subspaces and quotients": [[8, "subspaces-and-quotients"]], "Sums and products of vector spaces": [[8, "sums-and-products-of-vector-spaces"]], "The Existential Quantifier": [[2, "the-existential-quantifier"]], "The Schr\u00f6der-Bernstein Theorem": [[3, "the-schroder-bernstein-theorem"]], "Topological spaces": [[9, "topological-spaces"]], "Topology": [[9, null]], "Uniformly continuous functions": [[9, "uniformly-continuous-functions"]], "Using Theorems and Lemmas": [[1, "using-theorems-and-lemmas"]], "Vector spaces": [[8, "vector-spaces"]], "Vector spaces and linear maps": [[8, "vector-spaces-and-linear-maps"]]}, "docnames": ["C01_Introduction", "C02_Basics", "C03_Logic", "C04_Sets_and_Functions", "C05_Elementary_Number_Theory", "C06_Structures", "C07_Hierarchies", "C08_Groups_and_Rings", "C09_Linear_Algebra", "C10_Topology", "C11_Differential_Calculus", "C12_Integration_and_Measure_Theory", "genindex", "index"], "envversion": {"sphinx": 62, "sphinx.domains.c": 3, "sphinx.domains.changeset": 1, "sphinx.domains.citation": 1, "sphinx.domains.cpp": 9, "sphinx.domains.index": 1, "sphinx.domains.javascript": 3, "sphinx.domains.math": 2, "sphinx.domains.python": 4, "sphinx.domains.rst": 2, "sphinx.domains.std": 2}, "filenames": ["C01_Introduction.rst", "C02_Basics.rst", "C03_Logic.rst", "C04_Sets_and_Functions.rst", "C05_Elementary_Number_Theory.rst", "C06_Structures.rst", "C07_Hierarchies.rst", "C08_Groups_and_Rings.rst", "C09_Linear_Algebra.rst", "C10_Topology.rst", "C11_Differential_Calculus.rst", "C12_Integration_and_Measure_Theory.rst", "genindex.rst", "index.rst"], "indexentries": {"abel": [[1, "index-15", false], [7, "index-3", false]], "absolute value": [[1, "index-24", false]], "absurd": [[2, "index-17", false]], "anonymous constructor": [[2, "index-7", false]], "apply": [[1, "index-12", false], [1, "index-17", false]], "assumption": [[2, "index-19", false]], "bounded quantifiers": [[3, "index-3", false]], "by_cases": [[2, "index-23", false]], "by_contra": [[2, "index-14", false]], "by_contra and by_contradiction": [[2, "index-14", false]], "calc": [[1, "index-3", false]], "cases": [[2, "index-8", false]], "change": [[2, "index-2", false]], "check": [[0, "index-0", false]], "command": [[1, "index-9", false]], "commands": [[0, "index-0", false]], "commutative ring": [[1, "index-8", false]], "congr": [[2, "index-25", false]], "constructor": [[2, "index-18", false]], "continuity": [[9, "index-3", false]], "contradiction": [[2, "index-17", false]], "contrapose": [[2, "index-16", false]], "convert": [[2, "index-26", false]], "decide": [[4, "index-0", false]], "definitional equality": [[1, "index-13", false]], "differential calculus": [[10, "index-0", false]], "divisibility": [[1, "index-25", false]], "dsimp": [[2, "index-2", false]], "elementary calculus": [[10, "index-1", false]], "erw": [[2, "index-4", false]], "exact": [[1, "index-12", false], [1, "index-17", false], [1, "index-5", false]], "excluded middle": [[2, "index-22", false]], "exfalso": [[2, "index-17", false]], "exponential": [[1, "index-19", false]], "ext": [[2, "index-24", false]], "extensionality": [[2, "index-24", false]], "field_simp": [[2, "index-11", false]], "filter": [[9, "index-1", false]], "from": [[2, "index-12", false]], "gcd": [[1, "index-26", false]], "goal": [[1, "index-2", false]], "group": [[1, "index-15", false], [7, "index-2", false]], "group (algebraic structure)": [[1, "index-14", false], [7, "index-1", false]], "group (tactic)": [[1, "index-15", false], [7, "index-2", false]], "have": [[1, "index-11", false], [2, "index-12", false]], "implicit argument": [[1, "index-10", false]], "inequalities": [[1, "index-16", false]], "injective function": [[2, "index-5", false]], "integration": [[11, "index-0", false], [11, "index-1", false]], "intro": [[2, "index-0", false]], "lambda abstraction": [[2, "index-1", false]], "lattice": [[1, "index-28", false]], "lcm": [[1, "index-26", false]], "left": [[2, "index-21", false]], "let": [[2, "index-13", false]], "linarith": [[1, "index-18", false]], "linear map": [[8, "index-1", false]], "local context": [[1, "index-2", false]], "logarithm": [[1, "index-19", false]], "matrices": [[8, "index-3", false]], "max": [[1, "index-21", false]], "measure theory": [[11, "index-2", false]], "metric space": [[1, "index-30", false], [9, "index-2", false]], "min": [[1, "index-21", false]], "monoid": [[7, "index-0", false]], "monotone function": [[2, "index-3", false]], "namespace": [[1, "index-9", false]], "noncomm_ring": [[1, "index-15", false]], "norm_num": [[1, "index-20", false]], "normed space": [[10, "index-2", false]], "open": [[1, "index-9", false]], "order relation": [[1, "index-27", false]], "partial order": [[1, "index-27", false]], "proof state": [[1, "index-2", false]], "push_neg": [[2, "index-15", false]], "rcases": [[2, "index-9", false]], "real numbers": [[1, "index-1", false]], "refl and reflexivity": [[1, "index-13", false]], "reflexivity": [[1, "index-13", false]], "repeat": [[1, "index-23", false]], "rewrite": [[1, "index-0", false]], "rfl": [[1, "index-13", false]], "right": [[2, "index-21", false]], "ring": [[1, "index-6", false]], "ring (algebraic structure)": [[1, "index-7", false], [7, "index-4", false]], "ring (tactic)": [[1, "index-6", false]], "rintro": [[2, "index-9", false]], "rw": [[1, "index-0", false], [1, "index-4", false]], "rw and rewrite": [[1, "index-0", false], [1, "index-4", false]], "rwa": [[3, "index-2", false]], "set operations": [[3, "index-0", false]], "show": [[1, "index-22", false]], "simp": [[2, "index-20", false], [3, "index-1", false]], "surjective function": [[2, "index-10", false]], "tactics": [[1, "index-0", false], [1, "index-11", false], [1, "index-12", false], [1, "index-13", false], [1, "index-15", false], [1, "index-17", false], [1, "index-18", false], [1, "index-20", false], [1, "index-22", false], [1, "index-23", false], [1, "index-29", false], [1, "index-3", false], [1, "index-4", false], [1, "index-5", false], [1, "index-6", false], [2, "index-0", false], [2, "index-11", false], [2, "index-12", false], [2, "index-13", false], [2, "index-14", false], [2, "index-15", false], [2, "index-16", false], [2, "index-17", false], [2, "index-18", false], [2, "index-19", false], [2, "index-2", false], [2, "index-20", false], [2, "index-21", false], [2, "index-23", false], [2, "index-24", false], [2, "index-25", false], [2, "index-26", false], [2, "index-4", false], [2, "index-6", false], [2, "index-8", false], [2, "index-9", false], [3, "index-1", false], [3, "index-2", false], [4, "index-0", false], [7, "index-2", false], [7, "index-3", false], [9, "index-3", false]], "this": [[2, "index-12", false]], "topological space": [[9, "index-4", false]], "topology": [[9, "index-0", false]], "trans": [[1, "index-29", false]], "use": [[2, "index-6", false]], "vector space": [[8, "index-0", false]], "vector subspace": [[8, "index-2", false]]}, "objects": {}, "objnames": {}, "objtypes": {}, "terms": {"": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "0": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "02463336": 6, "1": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "10": [2, 8, 9], "11": [8, 10], "12": [4, 8], "15": 2, "17": 4, "2": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "256": 9, "263": 6, "27": 4, "2c": 4, "3": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "37": 2, "4": [0, 1, 2, 4, 5, 7, 8, 9, 10], "4c": 4, "5": [1, 2, 5, 7, 8, 9, 10], "50": 6, "512": 9, "6": [2, 4, 5, 6, 7, 8, 9, 10], "64": 9, "7": [2, 4, 5, 7, 8], "70": 6, "73": 6, "8": [2, 4, 7, 8, 9], "9": 8, "A": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "And": [2, 4, 6, 9], "As": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "At": [0, 1, 2, 4, 5, 6, 8], "Be": [1, 3], "But": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "By": [1, 3, 5, 6, 7, 8], "For": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "If": [0, 1, 2, 3, 4, 5, 6, 8, 9], "In": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "It": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "Its": [5, 6], "Not": [1, 5, 9], "Of": [1, 2, 4, 6, 7, 8, 9, 10, 11], "On": [1, 2, 3, 5, 6, 8, 9, 11], "One": [1, 2, 3, 4, 5, 6, 7, 8, 9], "Or": [2, 3, 8], "Such": [0, 1, 2, 6], "That": [0, 4, 5, 6], "The": [0, 1, 4, 5, 6, 7, 8, 9, 10, 11, 13], "Their": [9, 10], "Then": [2, 3, 5, 6, 7, 8, 9, 11], "There": [0, 1, 2, 3, 4, 6, 7, 8, 9, 10, 11], "These": [0, 1, 3, 4, 5, 7, 10, 11], "To": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "With": [1, 3, 4, 6, 9], "_": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "_add_mod": 5, "_def": 4, "_eq": 5, "_in": 9, "_inst_1": 5, "_le": 5, "_n": 7, "_root_": [1, 3, 4], "a_0": 3, "a_1": 3, "a_2": 3, "a_def": 3, "a_of_b_of_c": 1, "ab": [0, 2, 5, 7], "abandon": 4, "abbrevi": [1, 2, 3, 5, 8], "abel": [1, 7], "abelian": [1, 5, 6, 8], "abgrpmodul": 6, "abil": 0, "abl": [0, 1, 2, 3, 4, 5, 6, 7, 8, 10], "abn": 2, "about": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 13], "abov": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "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, "absorb": 7, "absorb1": 1, "absorb2": 1, "absorpt": 1, "abstract": [1, 2, 5, 6, 7, 8, 9], "abstractli": 9, "absurd": [2, 4], "abus": 5, "ac": 5, "accept": [0, 1, 2, 8, 9], "access": [1, 3, 5, 6, 7, 8, 9, 11], "accessor": 5, "accid": 8, "accommod": [5, 7], "accompani": 5, "accord": [5, 8], "account": 8, "achiev": [5, 6, 9], "acknowledg": 0, "acpo": 2, "across": 6, "act": [1, 7, 8], "action": 8, "activ": 0, "actual": [2, 3, 4, 6, 7, 8, 9], "ad": [1, 2, 3, 4, 5, 6, 8, 9], "adapt": 5, "add": [2, 4, 5, 6, 7, 8, 9, 10], "add_assoc": [1, 4, 5, 6], "add_assoc\u2083": 6, "add_comm": [1, 4, 5, 6, 7], "add_def": 5, "add_im": 5, "add_l": 1, "add_le_add": [1, 2], "add_le_add_left": 1, "add_le_add_right": 1, "add_left_cancel": 1, "add_left_inj": 2, "add_lt_add_left": 1, "add_lt_add_of_le_of_lt": 1, "add_lt_add_of_lt_of_l": 1, "add_lt_add_right": 1, "add_mem": [7, 8], "add_mem_sup": 8, "add_mul": [1, 6], "add_mul_mod_self_left": 4, "add_neg_cancel_right": 1, "add_nonneg": [1, 5], "add_one_le_of_lt": 5, "add_po": 1, "add_pos_of_pos_of_nonneg": 1, "add_r": 5, "add_right_cancel": 1, "add_right_neg": 1, "add_smul": [6, 7, 8], "add_sub": 1, "add_sub_cancel": 4, "add_sub_cancel_right": 1, "add_vadd": 7, "add_x": 5, "add_zero": [1, 5, 6], "addact": 7, "addalt": 5, "addalt_comm": 5, "addalt_x": 5, "addcommgroup": [1, 7, 8], "addcommgroup\u2083": 6, "addcommmonoid": [7, 8], "addcommmonoid\u2083": 6, "addcommsemigroup\u2083": 6, "addequiv": 7, "addgroup": [1, 5, 7], "addgrouppoint": 5, "addgroup\u2081": 5, "addgroup\u2082": 5, "addgroup\u2083": 6, "addit": [1, 2, 4, 5, 6, 7, 8, 9, 10, 11], "addmonoid": [6, 7, 8], "addmonoidhom": 7, "addmonoidhom\u2081": 6, "addmonoid\u2083": 6, "addmonoid\u2084": 6, "addsemigroup\u2083": 6, "addsubgroup": 7, "addzeroclass": 6, "adi": 5, "adjac": 8, "adject": 6, "adjug": 8, "adopt": 1, "advanc": 8, "advantag": [2, 3, 4, 5, 7, 10], "ae": [9, 11], "aestronglymeasur": 11, "aeval": [7, 8], "aeval_self_charpoli": 8, "aeval_x": 8, "affect": 6, "affin": 7, "aforement": 9, "after": [1, 2, 4, 6, 8, 9, 10], "again": [1, 2, 3, 4, 5, 6, 7, 8, 9], "against": 2, "agre": 3, "aid": 8, "aim": [4, 7], "aka": [8, 9], "aleb": 2, "alembert": 7, "alex": 0, "alexandru": 0, "algebra": [4, 6, 9, 10, 11, 13], "algebrahom": 6, "algebramap": [7, 8], "alghom": 7, "algorithm": 5, "alistair": 0, "all": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "allow": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "almost": [5, 6, 7, 8, 9, 11], "alon": 3, "along": [1, 4, 7, 9], "alpha": [2, 3], "alreadi": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "also": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "altern": [0, 1, 2, 3, 4, 5, 6, 9], "although": [0, 3, 4, 5, 6, 7, 8, 9], "alwai": [0, 1, 2, 3, 5, 6, 7, 8], "ambient": 7, "ambigu": [1, 5], "among": 4, "amount": [7, 8], "an": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "analog": [1, 2, 3, 4, 8, 9], "analogi": [2, 5, 9, 10], "analysi": [0, 5, 8, 10], "ancient": 4, "and_comm": 3, "anecdot": 6, "angl": 2, "ani": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "ann": 5, "annoi": [4, 6], "annot": [1, 2, 3, 4, 5, 6], "announc": 8, "anonym": [2, 3, 4, 5, 7], "anoth": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "answer": [0, 5, 9], "antisymm": 3, "antisymmetr": [1, 2], "anyhow": 2, "anyth": [2, 5, 9], "anywai": [4, 7], "apart": [5, 6], "api": 1, "appeal": [3, 6], "appear": [0, 1, 2, 5, 6, 7, 8, 9], "appli": [2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "applic": [1, 2, 5, 7, 11], "apply_fun": 7, "appreci": 4, "approach": [4, 5, 6, 9], "appropri": [1, 2, 3, 5, 6], "approxim": 1, "ar": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "arbitrari": [1, 2, 3, 4, 5, 7, 8], "arbitrarili": [2, 9], "archetyp": [5, 8], "argu": 6, "argument": [1, 2, 3, 4, 5, 6, 7, 8, 9], "aris": 2, "arithmet": 1, "aroot": 7, "aroots_def": 7, "around": [1, 3, 6, 7, 8, 9, 11], "arrai": 8, "arrang": 5, "arrow": [1, 2, 6, 9], "artifici": [5, 8], "ascii": 6, "ascript": [6, 7, 8], "asid": 3, "ask": [2, 4, 5, 6, 7, 9], "aspect": [0, 5, 7], "assembl": [8, 9], "assert": [2, 3, 6, 7], "assign": [2, 3, 5, 6, 7], "assist": [0, 2, 5], "associ": [0, 1, 2, 4, 5, 6, 7, 8, 9, 11], "assum": [0, 1, 2, 3, 4, 6, 7, 8, 9], "assumpt": [0, 1, 2, 3, 4, 5, 7, 8, 9, 10, 11], "assur": 5, "asymmetri": 2, "attach": [8, 9], "attain": 9, "attempt": 6, "attent": [1, 2, 4, 6, 7, 9], "attop": [9, 11], "attop_basi": 9, "attr": 6, "attract": 2, "attribut": 6, "auto": [1, 6], "autom": [0, 1, 5], "automat": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "aux": [1, 2, 4, 9], "aux_card_eq": 7, "auxiliari": [2, 9], "avail": [0, 1, 2, 4, 5, 6, 7, 8], "averag": 5, "avoid": [1, 2, 3, 4, 5, 6, 7, 10], "awai": [2, 5], "awkward": 8, "axiom": [1, 2, 3, 5, 6, 7, 8, 9, 11], "axiomat": [1, 2, 3, 5], "az": 8, "b": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "b_indep": 8, "b_span": 8, "baanen": 5, "back": [0, 1, 2, 5, 6, 7, 8, 9], "background": [0, 7], "backslash": [1, 3], "backward": [2, 9], "bad": [5, 6, 8, 9], "badinst": 6, "bair": [9, 10], "balanc": 1, "ball": [3, 10], "banach": [10, 11], "bar": [0, 1, 2, 8], "bare": [6, 8], "barrier": 6, "bartosz": 0, "base": [0, 2, 3, 4, 6, 7, 9, 10, 13], "basi": [5, 8, 9], "basic": [0, 2, 4, 5, 8, 9, 11, 13], "basisfun": 8, "basissingleon": 8, "baz": 1, "bbb": [2, 5], "bc": 5, "bci": 5, "bd": 5, "becaus": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "becom": [1, 4, 5, 6, 9], "been": [0, 1, 2, 4, 5, 6, 8, 10], "befor": [0, 1, 2, 3, 4, 5, 6, 7, 8], "begin": [1, 2, 3, 4, 5, 6], "begun": 9, "behav": [2, 3, 6, 8, 9], "behavior": [3, 6, 9], "behind": [3, 7], "being": [1, 3, 5, 7, 8, 9, 10], "belong": [5, 6, 9], "below": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "benefit": [7, 8], "benjamin": 0, "beq": 2, "berman": 0, "bernstein": 13, "besid": 6, "bespok": 5, "best": 0, "beta": [2, 3], "better": [3, 4, 5, 6, 9], "between": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "bewar": [6, 8], "bex": 3, "bex_def": 3, "beyond": [2, 6, 10], "bi": [1, 2, 5], "big": [0, 5, 7, 8, 9, 10], "bigcup_": 3, "bigger": [0, 3, 10], "bigoper": [4, 5, 7], "biject": [3, 5, 7, 8], "bijective_iff_injective_and_card": 7, "bilinear": 11, "binari": [1, 2, 4, 5, 6, 8], "binary_product": 8, "bind": [1, 3], "binder": 6, "bipartit": 5, "bit": [1, 2, 4, 6, 7, 8, 9], "black": [4, 6], "block": [1, 4, 7], "blur": 9, "bochner": 11, "bodi": 7, "boil": 6, "bold": 2, "bolt": 1, "book": [0, 2, 8, 9], "boolean": 1, "border": 9, "borelspac": 11, "boss": 9, "both": [1, 2, 3, 4, 5, 6, 7, 9, 10], "bother": [1, 3], "bottom": [6, 7, 8, 9], "bound": [1, 2, 3, 4, 5, 8, 9, 10, 11], "bounded": 10, "bounded_of_ex_finset": 4, "bourbaki": 9, "box": 4, "bpo": [2, 9], "bq": 5, "brace": [1, 8], "bracket": [1, 2, 5, 6, 7], "branch": [2, 3, 6], "break": 6, "breviti": [1, 5], "briefli": 7, "bring": [3, 4, 9], "broader": [4, 10], "broadest": 5, "brown": 0, "brows": [0, 1, 4, 7], "bryan": 0, "build": [0, 2, 4, 6, 7, 8, 9, 13], "builder": 3, "built": [0, 2, 6, 7, 8], "builtin": 6, "bulb": 5, "bulwi": 0, "bundl": [5, 6, 7, 8, 9, 10], "button": 0, "by_cas": [2, 3, 4], "by_contra": [2, 4], "c": [0, 1, 2, 4, 5, 6, 7, 8, 9, 10, 11], "c_mul": 7, "c_neg": 7, "cach": 0, "calc": [1, 2, 3, 5, 7, 9], "calcul": [0, 2, 4, 5, 13], "calculu": [9, 11, 13], "call": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "can": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "candid": 5, "cannot": [2, 3, 4, 5, 6, 7, 8, 9], "canon": [2, 3, 4, 5, 8], "cantor": 3, "cap": 3, "capabl": 5, "capit": 5, "captur": 8, "card": 7, "card_congr": 7, "card_dvd_of_l": 7, "card_eq_one_iff_exist": 7, "card_po": 7, "card_sigma": 7, "cardin": [3, 7, 8], "care": [1, 2, 3, 5, 8], "carneiro": 0, "carri": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "carrier": [1, 5, 6, 7, 8], "case": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "categor": 9, "categori": [5, 8, 9, 10], "cauchi": 9, "cauchyseq": 9, "cauchyseq_iff": 9, "cauchyseq_of_le_geometric_two": 9, "cauchyseq_tendsto_of_complet": 9, "caveat": 7, "caylei": [7, 8], "cayleyisomorph": 7, "cdist": 9, "cdot": 5, "center": [0, 9], "central": [0, 4], "centuri": 3, "ceq": 2, "certain": [2, 6, 9], "certifi": 0, "cha": 0, "chain": 5, "challeng": [0, 1, 2, 3, 5, 10], "chanc": 2, "chang": [0, 1, 2, 4, 5, 9, 11], "chapter": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "char": 0, "charact": [1, 3, 6], "character": [1, 3, 4, 8, 9, 10], "characterist": 8, "charpoli": 8, "chat": 0, "cheat": [0, 1], "check": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "checksynthord": 6, "chen": 0, "chestnut": 2, "chines": 7, "chineseiso": 7, "chinesemap": 7, "chinesemap_inj": 7, "chinesemap_mk": 7, "chinesemap_surj": 7, "choic": [1, 2, 3, 5, 8, 9], "choos": [0, 2, 3, 4, 5, 6, 7, 9], "choose_spec": 3, "chose": 6, "chosen": [2, 5], "circ": [3, 5], "circl": 7, "circleequ": 7, "claim": 9, "clarifi": 5, "clash": 1, "class": [1, 4, 5, 6, 7, 8, 9, 10, 11], "classic": [2, 3, 4, 7, 8], "claus": 6, "clean": [2, 9], "clear": [1, 2, 4, 5, 6], "clearer": [1, 3, 5], "clearli": 9, "clever": 1, "click": [0, 1, 3, 4, 5, 6], "clock": 0, "clontz": 0, "close": [1, 2, 3, 6, 7, 8, 10, 11], "closed_nhds_basi": 9, "closedbal": 9, "closer": [2, 9], "closur": [7, 8, 9], "closure_iscycl": 7, "cloud": 0, "clue": 7, "clunki": 9, "cluster": 9, "clusterpt": 9, "cmd": [1, 2], "co": [2, 7], "cocki": 1, "code": [0, 1, 2, 3, 5, 6, 8], "codomain": [2, 4, 9], "coe": 6, "coe_inject": 6, "coe_natabs_norm": 5, "coeff": 7, "coeffici": [5, 7, 8], "coefun": 6, "coelinearmap": 8, "coerc": [6, 7, 8], "coercion": [5, 6, 7, 8, 9, 10], "coincid": [4, 5, 9], "coinduc": 9, "coinduced_compos": 9, "coinduced_le_iff_le_induc": 9, "col": 8, "collari": 0, "collect": [1, 2, 3, 5, 8, 9, 11], "collis": 6, "colon": [2, 8], "column": 8, "comap": [7, 8, 9], "comap_bot": 8, "comap_comap": 9, "comap_map_eq": 8, "comapmkqreliso": 8, "combin": [1, 2, 5, 6, 7, 8, 9], "come": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "comfort": 0, "comm": 7, "comma": [1, 8], "command": [0, 1, 2, 3, 4, 5, 6, 7, 8], "commelin": 0, "comment": [0, 4], "commgroup": 1, "commgroup\u2083": 6, "commmonoid": 6, "commmonoid\u2083": 6, "common": [1, 2, 3, 4, 5, 7, 8, 9], "commonli": [4, 5], "commr": [1, 2, 5, 7], "commsemigroup\u2083": 6, "commsemir": [7, 8], "commun": [0, 4], "commut": [1, 2, 3, 4, 5, 6, 7, 8, 10], "comp": [7, 8, 9], "comp_id": 8, "compact": 11, "compactspac": 9, "compani": 2, "companion": [0, 1], "compar": [0, 5, 6, 8, 9], "comparison": 6, "compat": [1, 7, 9], "compat_mymap": 7, "compl": 11, "complain": 1, "complement": [3, 8, 9, 11], "complementari": 0, "complet": [0, 1, 2, 3, 4, 6, 7, 10], "completespac": [9, 10, 11], "complex": [0, 1, 2, 4, 5, 7, 8, 10, 11], "complic": [1, 2, 6, 7, 8], "compon": [2, 3, 5, 8, 9, 11], "compos": [3, 5, 7, 9], "composit": [2, 3, 5, 6, 7, 8, 9], "compound": [1, 2, 9], "compress": [0, 1, 9], "comput": [0, 2, 3, 4, 5, 7, 8, 10, 11], "computation": [4, 8], "concentr": 3, "concept": [5, 7, 8, 9, 10], "conceptu": [3, 7], "concis": [1, 5, 7], "conclud": [2, 10], "conclus": [1, 2, 4], "concret": [1, 2, 4, 5, 6, 8, 9], "condens": 3, "condit": [3, 4, 6, 7, 8, 9, 10], "confid": 3, "configur": 5, "confirm": [1, 2, 3, 4], "confus": [3, 4, 6, 7, 9], "congr": 2, "congratul": [1, 2, 4], "congruent": 4, "conj": 5, "conj_im": 5, "conj_r": 5, "conjug": [5, 7], "conjugate_on": 7, "conjunct": [1, 6, 13], "connect": [1, 3, 5, 8, 9], "consequ": 7, "consid": [1, 2, 3, 4, 5, 6, 7, 9, 10, 11], "consider": 8, "consist": [1, 3, 5, 6, 7, 8, 9, 10], "constant": [1, 2, 7, 11], "constantli": 7, "constitut": 1, "constr": 8, "constr_basi": 8, "constraint": [5, 9], "construct": [0, 2, 3, 4, 5, 6, 7, 8, 9], "constructor": [1, 2, 3, 4, 5, 6], "consult": 5, "cont": 10, "contain": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "contdiff": 10, "contdiff_iff_continuous_differenti": 10, "contdiffat": 10, "contend": 4, "content": [0, 1, 2, 4, 9], "context": [1, 2, 4, 5, 6, 7, 8, 9, 10, 11], "contextu": 5, "continu": [0, 1, 4, 5, 6, 8, 11], "continuous_def": 9, "continuous_dist": 9, "continuous_fst": 9, "continuous_id": [6, 9], "continuous_iff": 9, "continuous_iff_coinduced_l": 9, "continuous_linear_map": 10, "continuous_pow": 9, "continuous_snd": 9, "continuousat": [9, 11], "continuousat_extend": 9, "continuousat_iff": 9, "continuouslinearmap": 10, "continuouson": [9, 10], "continuum": 2, "contort": 7, "contract": 2, "contradict": [2, 3, 4], "contradictori": 2, "contrapos": [2, 3, 4], "contrari": 2, "contrast": [2, 3, 5, 6, 9], "contravari": 9, "contribut": [0, 3], "contributor": 8, "control": 2, "conveni": [1, 2, 3, 5, 6, 7, 8, 9], "convent": [1, 5, 7, 11], "convention": 9, "converg": [11, 13], "convergesto": 2, "convergesto_add": 2, "convergesto_const": 2, "convergesto_mul": 2, "convergesto_mul_const": 2, "convergesto_uniqu": 2, "convers": [0, 2, 4, 7, 8, 9], "convert": [2, 4, 7, 8], "convinc": 5, "convolut": 11, "coordin": [7, 8], "copi": [0, 3, 4, 6, 7, 8, 9], "coprim": [4, 7], "coprime_mn": 4, "coprod": 8, "coprod_inl": 8, "coprod_inr": 8, "coproduct": 8, "core": [0, 4, 5], "corner": 7, "corollari": 7, "correct": [0, 1, 7], "correctli": 3, "correspond": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "could": [0, 1, 2, 4, 5, 6, 7, 8, 9], "count": 7, "count_factors_mul_of_po": 4, "countabl": 11, "counter": 8, "counterexampl": [2, 10], "counterpart": 5, "coupl": [1, 2, 6, 8, 9], "cours": [1, 2, 4, 6, 7, 8, 9, 10, 11], "covari": 9, "cover": [0, 1, 3, 6, 7, 8, 9, 10], "cramer": 8, "creat": [0, 1, 4, 6], "creation": 7, "creativ": 5, "criterion": 9, "crucial": [7, 8, 9], "crude": 4, "cryptic": 2, "ct": 2, "ctrl": [0, 1, 2, 4, 5], "cube": 7, "cue": 5, "cup": 3, "curiou": [1, 6], "curli": [1, 2, 8], "current": [1, 2, 5, 6], "curri": 1, "cursor": [0, 1, 2], "curv": 0, "custom": 5, "cut": 4, "cycl": 7, "cyclic": 7, "czubin": 0, "d": [1, 2, 4, 5, 7, 8, 10], "dai": 3, "danger": [4, 5], "data": [1, 2, 4, 5, 6, 8, 9], "databas": [3, 4, 6, 9], "datatyp": 4, "de": 0, "deal": [1, 2, 3, 4, 5, 8, 9], "dealt": 2, "decid": [4, 7, 8, 9], "decidableeq": [4, 8], "decidablepr": 4, "decis": [4, 7], "declar": [0, 1, 4, 5, 6, 7, 8], "decompos": [0, 3], "decreas": [1, 5], "dedekind": 3, "deduc": [6, 7, 9], "def": [0, 2, 3, 4, 5, 6, 7, 8, 9], "default": [1, 2, 3, 4, 5, 6, 7, 10], "defect": [2, 6, 9], "defin": [1, 2, 3, 4, 6, 7, 8, 9, 10, 11, 13], "definit": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "definition": [1, 4, 5, 6, 9], "degre": 7, "degree_mul": 7, "delet": [1, 2, 3], "delic": 3, "delimit": 1, "demonstr": [6, 9], "deni": 0, "denomin": [2, 4, 5], "denot": [1, 3, 4, 6, 7, 8, 9], "dens": 9, "denseinduc": 9, "densiti": 9, "depend": [0, 2, 3, 4, 5, 6, 7, 8, 9], "deriv": [1, 2, 4, 7, 10, 11], "deriv_add": 10, "deriv_eq_zero": 10, "deriv_zero_of_not_differentiableat": 10, "descend": [6, 7], "describ": [0, 1, 2, 3, 4, 5, 6, 8, 9], "descript": [0, 1, 2, 4, 9], "deserv": 4, "design": [0, 1, 2, 3, 5, 7, 8, 9], "desir": [1, 3, 6, 7, 9], "despit": 8, "destruct": 2, "destructur": 6, "det": [8, 11], "det_mul": 8, "det_on": 8, "detail": [1, 2, 3, 4, 5, 6, 7], "detect": 2, "determin": [1, 5, 7, 8, 9], "develop": [0, 1, 4, 7, 11], "devic": 6, "devot": 9, "dfun": 6, "dfunlik": 6, "di": [2, 5], "dia": 6, "dia_assoc": 6, "dia_inv": 6, "dia_on": 6, "diagram": 3, "diamond": 6, "diaoneclass\u2081": 6, "dia\u2081": 6, "dictionari": 1, "did": [0, 2, 6, 9], "dif_neg": 3, "dif_po": 3, "diff_eq": 3, "differ": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "differenti": [11, 13], "differentiableat": 10, "differentiableon": 10, "difficult": [2, 6], "digress": 9, "dimens": 13, "dimension": [8, 10, 11], "direct": [1, 2, 3, 6, 7, 9, 10], "directli": [1, 2, 4, 5, 6, 8, 9], "directsum": 8, "discret": 5, "discuss": [1, 2, 4, 5, 6, 7, 8, 9, 10], "dishwash": 0, "disjoint": [3, 7, 11], "disjunct": [1, 3, 13], "dispens": 4, "displai": [0, 1, 2, 6], "dispos": 2, "dist": [1, 9], "dist_comm": [1, 9], "dist_eq_zero": 9, "dist_le_range_sum_dist": 9, "dist_nonneg": [1, 9], "dist_self": 1, "dist_triangl": [1, 9], "distanc": [1, 2, 9, 10], "distinct": [0, 2, 3, 4, 5, 8, 9], "distinguish": [0, 5, 6, 7, 9, 10], "distract": 6, "distriblattic": 1, "distribut": [1, 4, 5, 6], "div": 5, "div_def": 5, "div_dvd_of_dvd": 4, "div_eq_mul_inv": 5, "div_eq_of_eq_mul_right": 4, "div_lt_self": 4, "div_nonneg": 5, "div_po": 2, "divab": 2, "divac": 2, "divbc": 2, "dive": 0, "divid": [1, 2, 4, 5, 7], "divis": [1, 2, 4, 5, 6, 8], "divisor": [1, 2, 4, 5, 7], "do": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "doc": 0, "document": [0, 1, 3, 4, 6], "doe": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "doesn": [1, 2, 7, 8, 9], "domain": [1, 2, 3, 4, 5, 7, 9], "domin": 11, "don": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "done": [0, 2, 3, 4, 6, 7, 8, 9], "doorn": 0, "dot": [1, 7, 8, 9], "doubl": [2, 3], "doubli": 7, "doubt": 0, "down": [0, 3, 4, 6, 9], "downsid": [7, 8], "dozen": 3, "draw": [1, 5, 6], "drop": 2, "dsimp": [2, 3, 5, 7, 8], "dual": [5, 9], "dualli": 9, "duca": 0, "due": [1, 6], "duplic": 6, "dvd": 1, "dvd_add_iff_left": 4, "dvd_antisymm": 1, "dvd_fac": 4, "dvd_factori": 4, "dvd_gcd": 4, "dvd_gcd_iff": 2, "dvd_iff_exists_eq_mul_left": 4, "dvd_mul": 4, "dvd_mul_left": 1, "dvd_mul_of_dvd_left": 1, "dvd_mul_of_dvd_right": 4, "dvd_mul_right": [2, 4], "dvd_of_dvd_pow": 4, "dvd_prod_of_mem": 4, "dvd_sub": 4, "dvd_tran": 1, "dwell": 3, "e": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "each": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "earli": 8, "earlier": [1, 7, 8], "easi": [0, 4, 5, 6, 7, 8, 9], "easier": [0, 1, 3, 4, 6, 9], "easiest": [2, 4], "easili": [1, 4, 5, 6, 7, 8], "ebner": 0, "eccentr": 8, "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, 9], "effici": [5, 7, 8, 9], "effort": [1, 4], "eg": 2, "eigenspac": 8, "eigenvalu": 8, "eigenvector": 8, "eight": 9, "either": [1, 2, 3, 5, 6, 9], "elabor": [8, 9], "ele1": 2, "eleg": 5, "element": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "elementari": [0, 3, 5, 7, 8, 9, 13], "elim": 2, "elim_finite_subcov": 9, "elimin": 1, "els": [2, 3, 4, 8], "em": [2, 3], "emanuel": 0, "emb": 5, "embark": 6, "embed": 7, "embodi": 7, "emetricspac": 9, "emod_lt": 5, "emod_lt_of_po": 5, "emod_nonneg": 5, "emphas": [6, 7], "emphasi": [0, 6], "empti": [3, 4, 5, 7, 9, 11], "enabl": [2, 3, 4, 5], "enat": 4, "encapsul": [3, 5, 10], "encod": [7, 11], "encount": [4, 6], "encourag": [0, 1, 2, 3, 4, 5], "end": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "endomorph": [7, 13], "endow": [6, 7, 8], "enforc": 7, "engin": 4, "enjoi": [2, 3, 4, 9], "ennreal": 11, "enough": [0, 1, 2, 3, 4, 6, 7, 8, 9], "ensur": [6, 7, 8, 9], "enter": [0, 1, 2, 3, 7, 9], "enthusiast": 0, "entir": [1, 3, 5, 9, 10], "entourag": 9, "entri": [0, 5, 7, 8], "enumer": [1, 2], "epo": 2, "eq": 5, "eq1": 4, "eq2": 4, "eq_bot": 8, "eq_bot_iff": 8, "eq_bot_iff_card": 7, "eq_bot_iff_foral": 7, "eq_empty_or_nonempti": 9, "eq_neg_of_add_eq_zero": 1, "eq_of_dvd_of_prim": 4, "eq_of_mul_eq_mul_right": 7, "eq_one_or_self_of_dvd": 4, "eq_top_iff": 7, "eq_two_or_odd": 3, "eq_univ": 3, "eq_univ_of_foral": 3, "eq_zero_iff_mem": 7, "eq_zero_or_eq_zero_of_mul_eq_zero": 2, "equal": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "equat": [1, 2, 3, 4, 5], "equilater": 5, "equip": [1, 3, 5, 6, 7, 9, 10, 11], "equiv": [5, 7, 8], "equival": [1, 2, 3, 4, 5, 7, 8, 9, 10, 11], "eras": 4, "eric": 0, "error": [1, 2, 3, 6], "erw": 2, "especi": [1, 2, 5, 6, 7, 8, 9], "essenti": [2, 3, 5, 7, 9], "establish": [0, 1, 2, 3, 4, 5], "eta": 5, "etc": [8, 9], "euclidean": 5, "euclideandomain": 5, "eval": [0, 7, 8], "evalu": [7, 8], "eval\u2082": 7, "even": [0, 1, 2, 3, 4, 5, 6, 8, 9, 10, 11], "even_of_even_sqr": 4, "eventu": [2, 3, 9], "eventually_eventually_nhd": 9, "eventually_left_invers": 10, "eventually_right_invers": 10, "eventuallyeq": 9, "ever": [0, 9], "everi": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "everyth": [1, 2, 6, 9], "everywher": [2, 3, 6, 8, 9, 11], "evid": 5, "evolv": 1, "ex": [0, 2], "ex_finset_of_bound": 4, "exact": [1, 2, 3, 4, 5, 7, 8, 9], "exactli": [1, 2, 3, 5, 6, 7, 9], "exampl": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "except": [1, 2, 5, 7], "exclam": 9, "exclud": [2, 4], "exercis": [0, 1, 2, 3, 5, 6, 7, 8, 9, 10], "exfalso": 2, "exhibit": [2, 9], "exist": [1, 2, 3, 6, 7, 8, 9], "existenti": [3, 7, 13], "exists_abs_le_of_convergesto": 2, "exists_deriv_eq_slop": 10, "exists_deriv_eq_zero": 10, "exists_haseigenvector": 8, "exists_infinite_prim": 3, "exists_ismaxon": 9, "exists_isminon": 9, "exists_one_lt_norm": 10, "exists_prime_and_dvd": 3, "exists_prime_factor": 4, "exists_prime_factor_mod_4_eq_3": 4, "exists_subgroup_card_pow_prim": 7, "exot": [7, 9], "exp": [1, 3], "exp_le_exp": 1, "exp_log": 3, "exp_lt_exp": 1, "exp_po": [1, 3], "expand": [1, 2, 3, 4, 5, 6, 8], "expect": [1, 2, 3, 4, 5, 6, 7, 8, 9], "experi": [0, 1, 9], "explain": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "explan": [0, 7, 8, 9], "explicit": [1, 2, 5, 6, 8, 9], "explicitli": [1, 2, 3, 5, 6, 7, 8, 9, 10], "explor": [4, 8, 9], "expon": 1, "exponenti": 4, "export": 6, "expos": [2, 9], "express": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "ext": [2, 3, 4, 5, 6, 7, 8], "ext_iff": 5, "extend": [1, 3, 4, 5, 6, 9, 11], "extens": [0, 1, 6, 9, 10], "extension": [3, 5], "extern": 8, "extra": [1, 2, 3, 5, 6, 7, 9], "extract": [2, 9], "extrem": [0, 6, 9], "f": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "f_": 9, "f_cont": 9, "f_le": 9, "f_ne": 9, "fac": 4, "fac_po": 4, "face": [5, 6, 9], "facilit": [2, 8, 9], "fact": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "factor": [4, 5, 7, 8], "factori": 4, "factorial_po": 4, "factorization_mul": 4, "factorization_pow": 4, "fail": [1, 2, 4, 5, 6, 8, 9, 11], "failur": 6, "fairli": 2, "fals": [1, 2, 3, 4, 6], "falso": 2, "famili": [7, 8, 9, 10], "familiar": [0, 1, 4, 5, 8, 9, 10], "famou": [3, 7], "far": [2, 3, 6, 8, 9], "favor": [1, 5], "fderiv": 10, "fear": 6, "feat": 4, "featur": [0, 2, 4, 7], "feed": 7, "feedback": 0, "feel": [0, 1, 2, 6, 8, 9], "fermatlasttheorem": 0, "fetch": 0, "few": [1, 2, 3, 4, 9], "field": [0, 1, 5, 6, 7, 8, 10], "field_simp": [2, 5], "figur": [0, 1, 2, 5, 8], "file": [0, 1, 4, 5, 6, 7, 9], "fill": [2, 3, 4, 5], "filter": [4, 10, 11, 13], "filter_upward": 9, "filteri": 9, "fin": [5, 7, 8, 11], "fin_cas": 8, "final": [1, 2, 3, 5, 7, 8, 9, 11], "finaliso": 7, "find": [0, 1, 2, 4, 5, 6, 8, 9], "fine": 8, "finicki": 1, "finish": [1, 2, 3, 4, 7], "finit": [1, 3, 4, 5, 7, 8, 9, 10, 11], "finitedimension": [8, 10, 11], "finrank": 8, "finrank_eq_rank": 8, "finrank_fin_fun": 8, "finrank_l": 8, "finrank_pos_iff": 8, "finrank_real_complex": 8, "finrank_self": 8, "finrank_sup_add_finrank_inf_eq": 8, "finset": [4, 5, 7, 8, 9], "finsupp": 8, "fintyp": [7, 8, 9], "fintypebasisindex": 8, "first": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "firstcountabletopologi": 9, "fix": [4, 6, 7, 8, 9], "fixm": 5, "flag": [2, 3], "flavor": 8, "flexibl": 9, "flori": 0, "fn_ub_add": 2, "fneven": 2, "fnhaslb": 2, "fnhasub": 2, "fnlb": 2, "fnodd": 2, "fnub": 2, "fnub_add": 2, "fnuba": 2, "focu": [0, 1, 7, 8, 9, 11], "focus": 9, "folder": 0, "follow": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "font": 7, "foo": [1, 5], "forc": [1, 2, 3, 7, 8], "foreshadow": 1, "forewarn": 0, "forget": 6, "form": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "formal": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "format": 1, "former": 5, "formul": [4, 7, 9], "formula": [7, 11], "forth": 5, "fortiori": 9, "fortun": 3, "forward": [1, 2, 5, 7, 9], "found": [1, 5, 7, 8, 10], "foundat": [2, 3, 4, 5, 7, 8], "four": [2, 5], "fourth": [1, 2], "frac": 5, "fraction": 4, "fraenkel": 2, "framework": [0, 8], "frasa": 0, "free": [0, 1, 7, 8, 9], "freegroup": 7, "freeli": 4, "frequent": 9, "friend": [2, 5], "friendli": 7, "from": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "front": 2, "frustrat": [0, 6], "fr\u00e9chet": 10, "fst": [5, 8, 9], "fubini": 11, "full": [1, 2, 3, 4, 5, 6, 7, 8, 9], "fulli": [3, 7, 8, 9], "fun": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "function": [1, 2, 4, 5, 6, 7, 8, 10, 11, 13], "functori": 9, "fundament": [0, 4, 5, 6, 11], "funni": 9, "further": [1, 9], "furthermor": 7, "g": [1, 2, 3, 5, 6, 7, 8, 9, 10, 11], "g_": 9, "g_1": 5, "g_2": 5, "g_3": 5, "gabriel": 0, "gadget": [2, 9], "gain": 6, "galoi": [3, 5, 8, 9], "galoisinsert": 8, "game": [0, 6], "gauss": 7, "gaussian": [2, 7, 13], "gaussianint": 5, "gaussint": 5, "gave": [7, 9], "gcd": [1, 2, 4], "gcd_zero_left": 1, "gcd_zero_right": 1, "gcongr": 5, "ge": [0, 2, 5], "gener": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "genuin": 2, "geometr": 9, "geometri": 7, "get": [1, 2, 3, 4, 6, 7, 8, 9, 10, 13], "gi": 8, "gin": 0, "giovanni": 0, "git": 0, "github": [0, 1], "gitpod": 0, "give": [1, 2, 3, 4, 6, 7, 8, 9, 11], "given": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "glb": 1, "global": [7, 9], "go": [0, 1, 2, 3, 4, 6, 8, 9], "goal": [0, 1, 2, 3, 4, 5, 8, 9], "goe": [3, 4, 5, 6, 9], "good": [1, 2, 3, 4, 5, 6, 7, 8, 9], "gorbachev": 0, "got": 6, "govern": [1, 5], "gradual": [6, 9], "graph": [5, 8], "grate": [0, 5], "great": [1, 5], "greater": [0, 1, 2, 3, 4, 9], "greatest": [1, 5, 9], "greef": 0, "greek": [1, 4], "group": [0, 1, 2, 3, 4, 5, 6, 8, 9, 10, 13], "groupact": 7, "groupcat": 5, "groupequivquotientprodsubgroup": 7, "grouptheori": 5, "group\u2081": [5, 6], "group\u2081cat": 5, "group\u2082": 5, "group\u2083": 6, "grow": [0, 6, 7], "grp": 5, "guai": 0, "guarante": [0, 3, 5, 8], "guess": [1, 2, 3, 4, 5, 8], "guilherm": 0, "gya": 3, "g\u2080": 7, "g\u2081": 7, "g\u2082": 7, "h": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "h0": 4, "h1": [1, 2, 3, 4, 5], "h2": [1, 2, 3, 5], "h3": 1, "h_def": 3, "h_inj": 11, "ha": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "hab": 10, "habit": [6, 8], "hac": 6, "hack": 3, "had": [1, 6, 8], "hal": 6, "half": [3, 7], "hamilton": 8, "hand": [1, 2, 3, 4, 5, 6, 8, 9], "handi": 4, "handl": [1, 3, 4, 6, 7], "hanson": 0, "happen": [1, 6, 9], "happi": 0, "hard": [0, 1, 3, 5, 6, 7], "harder": [2, 5, 8], "harm": 3, "hasbasi": 9, "hasderivat": [10, 11], "hasderivat_sin": 10, "haseigenvalu": 8, "haseigenvalue_iff_isroot": 8, "haseigenvalue_of_haseigenvector": 8, "haseigenvector": 8, "hasfderivat": 10, "hasfderivatfilt": 10, "hasfderivatfilter_iff_islittleo": 10, "hasfderivwithinat": [10, 11], "hasinvgroup\u2082": 5, "haskel": 1, "hasmulgroup\u2082": 5, "hasonegroup\u2082": 5, "hasquoti": 6, "hasstrictfderivat": 10, "hausdorff": 9, "have": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "haven": [0, 2, 6, 9], "hb": [2, 9], "hba": 6, "hball": 9, "hbound": 11, "hc": 10, "hd": 9, "hdi": 11, "hdvd": 7, "he": 7, "headach": 4, "headi": 5, "heart": [4, 7], "heather": 5, "heaven": 5, "heavier": 6, "heavili": 9, "hello": 0, "help": [0, 1, 2, 3, 4, 5, 6, 8, 9], "helper": 1, "henc": [0, 2, 3, 4, 5, 6, 8, 9, 10], "here": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "hesit": 4, "hf": [3, 7, 9, 10, 11], "hfa": 2, "hfc": 10, "hff": 10, "hfi": 10, "hfx": 9, "hg": [3, 9, 10, 11], "hgb": 2, "hi": 7, "hidden": 2, "hide": [6, 7, 9], "hierarchi": [5, 7, 8, 13], "high": [2, 7], "higher": 6, "highlight": [0, 2], "hij": 8, "hint": [0, 1, 2, 11], "histor": [1, 7], "hit": [0, 1], "hk": [0, 10], "hle": 9, "hlim": 11, "hm": 10, "hmea": 11, "hmn": 0, "hmp": 10, "hn": [3, 4, 9, 10], "hna": 2, "hnb": 2, "hne": 9, "ho": 9, "hold": [1, 2, 3, 4, 5, 7, 8, 9, 11], "home": [4, 5], "homomorph": 7, "hood": [3, 5, 8], "hope": [0, 1, 8], "hopelessli": 6, "hoskinson": 0, "hover": [0, 1, 2, 3, 4, 5], "how": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "howev": [1, 2, 5, 6, 7, 8, 9, 10], "hp": [7, 9], "hpo": 9, "hq": [7, 9], "hr": 9, "hst": 7, "hsu": 9, "ht": 2, "html": 0, "http": 6, "hu": [9, 10], "huge": 6, "huisinga": 0, "hum": 9, "human": 1, "hunt": [6, 8], "hunter": 0, "huo": 9, "hurdl": 6, "hurt": 2, "hux": 9, "hv": 8, "hw": 6, "hx": [2, 3, 5, 6, 7, 8, 10], "hxeq": 3, "hy": [5, 6, 7, 8], "hyp": 1, "hypothes": [1, 2, 3, 4, 5], "hypothesi": [0, 1, 2, 3, 4], "hz": [5, 6], "h\u03b5": 10, "h\u03c6": 8, "h\u2080": [1, 2, 3, 4, 9], "h\u2081": [1, 2, 3, 4], "h\u2082": [1, 3, 4], "h\u2083": [1, 3], "i": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "icc": [9, 10], "ici": 9, "id": [4, 6, 8, 9, 10], "id_comp": 8, "idea": [1, 2, 3, 5, 6, 8, 9], "ideal": 8, "ident": [3, 4, 5, 6, 7, 8, 9, 13], "identif": 8, "identifi": [1, 2, 4, 8], "if_neg": 3, "if_po": 3, "iff": [1, 3, 7, 8, 9, 10, 11, 13], "ignor": [0, 5, 7, 8, 9], "ih": 4, "iinf_insert": 7, "iinter": 11, "il": 4, "illustr": [1, 2, 3, 4, 5, 7], "im": 5, "imag": [3, 4, 6, 7, 8, 9], "image_subset_iff": 3, "imagin": 1, "imaginari": 5, "immedi": [2, 3, 5, 6, 8], "implement": [2, 5, 6, 7, 8, 10], "impli": [1, 2, 3, 4, 5, 8, 9], "implic": [1, 8, 9, 13], "implicit": [1, 2, 5, 6, 7, 8, 9, 10], "implicitli": [1, 2], "import": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "importantli": [6, 7, 8], "imposs": 1, "impress": 0, "improv": [3, 4], "incl": 9, "includ": [0, 1, 2, 3, 4, 6, 7, 8, 9, 10], "inclus": [1, 3, 7, 8, 9], "inconsist": [1, 8], "inconveni": 10, "incorpor": 6, "increas": 1, "increment": [0, 1], "inde": [1, 5, 6, 7, 8, 9, 10], "indefinit": 4, "indent": 1, "independ": [2, 3, 5, 8], "indetermin": 7, "index": [3, 6, 7, 8, 9], "index_eq_card": 7, "index_mul_card": 7, "indic": [1, 2, 3, 5, 6], "indirect": 6, "indirectli": 1, "individu": 1, "induc": 9, "induced_compos": 9, "induct": [7, 8, 9, 13], "induction_on": 4, "inequ": [1, 2, 6, 9], "inf": [1, 6, 9], "inf_assoc": 1, "inf_bot_of_coprim": 7, "inf_comm": [1, 7], "inf_eq_bot": 8, "inf_le_left": [1, 9], "inf_le_right": 1, "inf_sup_left": 1, "inf_sup_right": 1, "inf_sup_self": 1, "infer": [1, 2, 3, 5, 6, 7, 8], "infer_inst": [10, 11], "inferenti": 0, "inferinst": [7, 8], "inferr": 6, "infimum": [1, 6, 7, 8, 9, 11], "infin": [4, 9, 11], "infinit": [3, 8, 9, 13], "infix": [1, 6], "infixl": 6, "infixr": 6, "inform": [0, 1, 2, 3, 5, 6, 8, 9], "infoview": [1, 6], "infrastructur": 0, "infti": 10, "ingredi": [3, 5, 9, 10], "inhabit": [3, 5, 9], "inherit": [5, 6, 7, 8], "inherit_doc": 6, "inj": 4, "inject": [2, 3, 4, 6, 7, 8, 9], "injective_lift_iff": 7, "injf": [2, 3], "injg": 2, "injon": [3, 11], "inl": [2, 3, 8], "inner": 3, "input": [1, 3, 8, 9], "inr": [2, 3, 8], "inria": 6, "inscrut": [2, 3], "insert": [0, 2, 4, 5, 7, 8, 9, 10], "insid": [0, 1, 2, 3, 7], "insight": 2, "insist": [1, 6], "inspect": 1, "inspir": 2, "inst": 6, "inst_1": 6, "instal": [0, 6], "instanc": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "instanti": [2, 5, 6, 9], "instcommr": 5, "instead": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "instruct": [0, 1, 2, 9], "int": [5, 6, 7], "intact": 0, "integ": [1, 2, 4, 6, 7, 13], "integr": [2, 10, 13], "integral_add": 11, "integral_eq_sub_of_hasderivat": 11, "integral_hasstrictderivat_right": 11, "integral_id": 11, "integral_image_eq_integral_abs_det_fderiv_smul": 11, "integral_one_div": 11, "integral_prod": 11, "intend": [0, 1, 2, 5], "inter_def": 3, "inter_set": 9, "interact": [0, 5, 6, 7, 8, 11], "interchang": 1, "interconnect": 5, "interest": [1, 2, 3, 5, 6, 8, 9], "interestingli": [5, 7, 10], "interfac": 5, "interior": [5, 10], "interior_iinter_subset": 10, "interior_subset": 10, "intermedi": [1, 6, 8, 9], "intern": [2, 5, 7], "interpret": [0, 1, 4, 5, 7, 8, 9], "intersect": [1, 3, 5, 6, 7, 8, 9, 11], "interv": [4, 9, 11], "interval_cas": 4, "intervalintegr": 11, "intro": [0, 1, 2, 3, 4, 5, 6, 7, 9], "introduc": [0, 1, 2, 3, 4, 8, 9, 11], "introduct": [1, 2, 7, 9, 13], "introductori": 10, "intuit": [3, 9], "inv": [5, 6], "inv_def": 8, "inv_dia": 6, "inv_eq_of_dia": 6, "inv_eq_of_mul": 6, "inv_mem": 7, "inv_mul": 6, "inv_mul_cancel": [1, 5], "inv_mul_of_invert": 8, "invari": 11, "invers": [1, 3, 5, 6, 7, 8, 10, 11], "inverse_spec": 3, "invert": [6, 7, 8], "invertibleofisunitdet": 8, "invest": 5, "invfun": [3, 5, 8], "invfun_eq": 3, "invisibli": [5, 6], "invok": [0, 1, 9], "involv": [1, 2, 4, 5, 6, 7, 8, 9], "inv\u2081": 6, "inward": 2, "ioo": [9, 10], "ipo": 4, "irrat": 13, "irration": 4, "irreduc": [4, 5], "irreducible_iff_prim": 5, "irreflex": 2, "is_addit": 5, "isaddhaarmeasur": 11, "isaiah": 0, "isalgclos": 7, "isbigo_iff_isbigowith": 10, "isbigowith": 10, "isbigowith_iff": 10, "isclos": [9, 10], "isclosed_l": [9, 10], "iscompact": 9, "iscompact_icc": 9, "iscompact_univ": 9, "iscompl": 8, "iscoprim": [7, 8], "iscoprime_iff_add": 7, "iscoprime_iff_codisjoint": 7, "iscoprime_iff_exist": 7, "iscoprime_iff_sup_eq": 7, "iscoprime_inf": 7, "iscycl": 7, "isdomain": [2, 7], "iseqv": 6, "isintern": 8, "isinternal_submodule_iff_independent_and_isup_eq_top": 8, "islinear": 5, "islittleo_iff_forall_isbigowith": 10, "islocalmin": 10, "ismonoidhom\u2081": 6, "ismonoidhom\u2082": 6, "isn": [0, 2, 3, 4, 6], "isomorph": [5, 7, 8, 10], "isopen": 9, "isopen_compl_iff": 9, "isopen_empti": 9, "isopen_iff": 9, "isopen_iinter_of_finit": 9, "isopen_iunion": 9, "isopen_univ": 9, "iso\u2081": 7, "iso\u2082": 7, "isroot": [7, 8], "isroot_of_haseigenvalu": 8, "issu": [1, 4, 5, 6, 8, 9], "issubgroup": 7, "issubmodul": 8, "isunit": 7, "item": 9, "iter": 10, "iteratedfderiv": 10, "its": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "itself": [0, 2, 3, 5, 6, 7, 8, 9, 10], "iunion": 11, "j": [3, 7, 8], "jimmi": 0, "job": 1, "johan": 0, "john": 0, "join": [0, 1, 5], "jone": 0, "journei": 9, "juggl": 6, "julian": 0, "jump": [1, 4, 5, 9], "just": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "justif": [1, 2], "justifi": [0, 1, 2, 9], "k": [0, 2, 4, 5, 7, 8, 9, 10], "keep": [1, 3, 5, 6, 7], "kei": [1, 4, 5, 7, 8, 9], "keith": 0, "ker": [7, 8], "ker_eq_bot": 8, "ker_eq_bot_iff": 7, "ker_le_ker_comp": 8, "ker_mkq": 8, "ker_pi_quotient_mk": 7, "ker_restrict": 7, "kernel": [7, 8], "keyboard": 1, "keyword": [1, 2, 4, 5], "kim": 0, "kind": [0, 1, 6, 8, 9], "knew": 9, "know": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "known": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "k\u00fclshammer": 0, "l": [0, 1, 8, 10, 11], "label": [1, 2], "lagrang": 7, "lake": 0, "lambda": [2, 5], "lambda_l": 5, "lambda_nonneg": 5, "languag": [0, 1, 2, 3], "larg": [0, 6, 9], "larger": [1, 9], "last": [1, 2, 3, 4, 5, 6, 7, 9], "later": [0, 1, 2, 4, 5, 6, 7, 8, 9], "latter": [5, 7, 9], "lattic": [1, 5, 6, 7, 9], "law": [1, 7], "layer": [6, 9], "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": 9, "le_inf": 1, "le_inf_iff": 9, "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_opnorm": 10, "le_or_gt": 2, "le_principal_iff": 9, "le_refl": [1, 2], "le_sup": 4, "le_sup_left": 1, "le_sup_right": 1, "le_tran": [1, 2], "lead": [1, 2, 4, 5, 6, 7, 8, 9], "leader": 1, "lean": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "lean4": 1, "learn": [0, 1, 4, 5], "least": [1, 5, 6, 8, 9], "leav": [0, 1, 2, 3, 5, 6, 7], "lebesgu": 11, "led": 6, "left": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "left_distrib": [5, 6], "left_inv": [5, 8], "left_inv_eq_right_inv": 6, "left_inv_eq_right_inv\u2081": 6, "left_neg_eq_right_neg": 6, "leftinvers": 3, "leftinverse_invfun": 3, "legal": 1, "lemma": [2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "less": [1, 2, 3, 4, 5, 6, 7, 8, 9], "let": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "letter": [1, 5, 10], "level": [1, 2, 6, 8], "leverag": 9, "le\u2081": 6, "librari": [0, 1, 2, 3, 4, 5, 7, 9, 10], "life": [0, 2], "lift": [7, 8], "liftq": 8, "light": 5, "like": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "lim_": 9, "limit": [2, 6, 9], "linarith": [1, 2, 4, 5], "line": [0, 1, 2, 3, 4, 6, 7, 8], "linear": [1, 2, 5, 7, 9, 13], "linear_combin": 7, "linearcombin": 8, "linearcombination_apply_of_mem_support": 8, "linearcombination_repr": 8, "linearequiv": 8, "linearequivfunonfintyp": 8, "linearindepend": 8, "linearli": 8, "linearmap": 8, "linearord": 2, "linearorderedr": 5, "liner": 0, "linf": 5, "link": [5, 6], "list": [1, 2, 3, 4, 5, 8], "littl": [1, 2, 9, 10], "liu": 0, "live": [0, 5, 8], "ll": [0, 2, 4, 6, 9], "local": [1, 2, 6, 9, 10], "localinvers": 10, "lof": 8, "log": [1, 3, 11], "log_le_log": 1, "log_lt_log": 1, "logic": [0, 1, 3, 4, 5, 7, 8, 13], "logician": 1, "long": [1, 2, 3, 5, 6, 7, 8, 10], "longer": [0, 4, 5], "look": [1, 2, 3, 4, 6, 7, 8, 9], "loop": 4, "loos": 8, "loss": 4, "lot": [0, 1, 3, 5, 6, 7, 8, 9], "loud": 1, "lower": [1, 2, 4], "lowest": 4, "lr": 1, "lsmul": 8, "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, "lt\u2081": 6, "lu": 0, "lub": 1, "m": [0, 1, 2, 4, 6, 7, 8, 9, 10], "m_iunion": 11, "mac": [1, 2], "macbeth": 5, "machin": 8, "machineri": [5, 6, 8, 9], "maco": 0, "made": [1, 2, 3, 5, 8, 9], "magic": [2, 5, 6], "mai": [0, 1, 2, 3, 5, 6, 7, 8, 9, 10], "main": [2, 6, 8, 9, 10], "mainli": 7, "maintain": 1, "make": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "manag": [0, 1, 4, 5, 9], "mani": [1, 2, 3, 5, 6, 7, 8, 9, 10, 11, 13], "manifest": [1, 9], "manipul": [2, 5, 7, 8, 9], "manner": [2, 5], "manual": [0, 3, 4], "map": [1, 2, 3, 5, 6, 7, 9, 13], "map_add": [6, 7, 8, 10], "map_comap_eq": 8, "map_eq": 9, "map_inv": 7, "map_inv_of_inv": 6, "map_le_iff_le_comap": 9, "map_map": 9, "map_mono": 9, "map_mul": [6, 7, 8], "map_on": [6, 7], "map_pow": 7, "map_smul": [8, 10], "map_zero": [6, 7, 8], "mapq": 8, "mapsto": [1, 5], "map\u2082": 6, "marc": 0, "mario": 0, "mark": [0, 1, 2, 6, 9], "marker": 2, "marriag": 5, "martin": 0, "mascellani": 0, "mass": 11, "master": [0, 1, 4], "match": [1, 2, 5], "mathbb": [3, 4, 5, 7], "mathcal": [5, 10], "mathemat": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "mathematician": [4, 9], "mathematics_in_lean": 0, "mathfrak": 7, "mathieu": 0, "mathlib": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "matric": [1, 5, 7, 13], "matrix": 8, "matter": [1, 2], "matthew": 0, "mauricio": 0, "max": [1, 2, 6, 8, 9, 11], "maxim": 7, "maximum": [2, 4, 9], "mayb": 6, "mcdowel": 0, "mdvdn": 4, "mean": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "meaning": 8, "meaningless": 2, "meant": [0, 2, 6, 8], "meanwhil": [1, 4], "measur": [0, 5, 9, 10, 13], "measurableset": 11, "measurablespac": 11, "measure_eq_iinf": 11, "measure_iunion_l": 11, "measuretheori": 11, "mechan": [1, 2, 5], "mediat": 4, "medit": 8, "meet": [1, 2, 3, 5], "mem": 3, "mem_": 4, "mem_ball_self": 9, "mem_bot": [7, 8], "mem_closedball_self": 9, "mem_closure_iff": 9, "mem_closure_iff_clusterpt": 9, "mem_closure_iff_nhds_basi": 9, "mem_closure_iff_seq_limit": 9, "mem_closure_of_tendsto": 9, "mem_comap": [7, 8], "mem_diff": 3, "mem_eras": 4, "mem_filt": 4, "mem_iff": 9, "mem_iint": 3, "mem_iinter\u2082": 3, "mem_image_of_mem": 3, "mem_inf": 8, "mem_insert": 4, "mem_insert_of_mem": 7, "mem_insert_self": 7, "mem_int": 4, "mem_inter_iff": 3, "mem_iunion": 3, "mem_iunion\u2082": 3, "mem_ker": [7, 8], "mem_map": [7, 8], "mem_map_of_mem": 8, "mem_nhds_iff": 9, "mem_of_dvd_prod_prim": 4, "mem_of_tendsto": 9, "mem_preimag": 8, "mem_rang": 7, "mem_sdiff": 4, "mem_setof": 3, "mem_sup": [7, 8], "mem_union": [3, 4], "member": [3, 9], "membership": [3, 4, 6, 7, 8], "mention": [2, 3, 5, 6, 7, 9], "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, 10, 13], "metricspac": [1, 9, 10], "mf": 2, "mg": 2, "mge2": 4, "mgt2": 4, "mid": 5, "middl": [0, 1, 2, 9], "midpoint": 5, "might": [1, 2, 3, 4, 5, 7], "mil": 0, "min": [1, 2, 9, 11], "min_le_left": 1, "min_le_right": 1, "mind": [1, 2, 5, 6, 7], "mindich": 0, "minfac": 4, "minim": 8, "minimum": 9, "minor": [6, 10], "minpoli": 8, "mislead": 7, "miss": [1, 3, 4], "mission": 0, "mk": [5, 6, 7, 8, 9], "mk_appli": 8, "mk_eq_mk_of_basi": 8, "mk_surject": 7, "mkofmuleqon": 7, "mkofnhd": 9, "mkq": 8, "mkvectorspac": 8, "mltn": 4, "mne1": 4, "mnez": 4, "mod": 5, "mod_4_eq_3_or_mod_4_eq_3": 4, "mod_def": 5, "mod_lt": 4, "mode": [1, 2, 5], "model": [3, 8, 9], "modern": [5, 7], "modifi": 6, "modu": 1, "modul": [6, 7, 8], "modular": 1, "module\u2081": 6, "module\u2083": 6, "modulo": [1, 4, 5], "moment": [1, 2, 5], "mono": 9, "monof": 2, "monoid": [2, 3, 4, 6, 8, 13], "monoidhom": 7, "monoidhomclass": 6, "monoidhomclass\u2081": 6, "monoidhomclass\u2082": 6, "monoidhomclass\u2083": 6, "monoidhom\u2081": 6, "monoid\u2081": 6, "monoid\u2082": 6, "monoid\u2083": 6, "monoton": [2, 6, 9], "monro": 0, "monticon": 0, "moral": [0, 5, 7], "more": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 13], "moreov": [0, 1, 4, 5, 9], "morphism": [5, 8, 10, 13], "morrison": 0, "most": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "mostli": 7, "motiv": [2, 8], "move": [0, 1, 2, 6, 8, 9], "mp": [1, 2, 3, 4, 9], "mpr": [1, 2, 5, 9], "much": [0, 2, 4, 6, 7, 8, 9, 10], "mul": [4, 5, 6, 9], "mul_add": [0, 1, 4, 6], "mul_appli": 8, "mul_assoc": [1, 2, 4, 5, 6, 7], "mul_assoc\u2083": 6, "mul_comm": [1, 2, 4, 5, 6, 7], "mul_def": 5, "mul_div_cancel": 4, "mul_div_cancel\u2080": 2, "mul_eq_comp": 8, "mul_im": 5, "mul_inv": [6, 7], "mul_inv_cancel": [1, 5, 7], "mul_inv_cancel_right": 5, "mul_inv_rev": 1, "mul_le_inf": 7, "mul_le_left": 7, "mul_le_mul": 2, "mul_le_right": 7, "mul_left_cancel\u2083": 6, "mul_left_comm": 4, "mul_left_not_lt": 5, "mul_lt_mul_right": 2, "mul_mem": [6, 7], "mul_mod": 4, "mul_mod_mod": 4, "mul_mod_right": 4, "mul_nonneg": 1, "mul_on": [1, 5, 6, 7], "mul_po": [1, 4], "mul_r": 5, "mul_right_cancel\u2083": 6, "mul_right_inj": 4, "mul_smul": [6, 7, 8], "mul_sub": 1, "mul_sum": 5, "mul_zero": [1, 5, 6], "mulact": 7, "mulequiv": 7, "muloneclass": 6, "multilinear": 10, "multipl": [1, 2, 3, 4, 5, 6, 7, 8, 10], "multipli": [5, 8], "multiset": 7, "multivari": 7, "mulvec": 8, "mulzeroclass": 6, "mundan": 2, "must": [1, 5, 6, 8, 9], "mvpolynomi": 7, "my_fil": 0, "my_lemma": 2, "my_lemma2": 2, "my_lemma3": 2, "my_lemma4": 2, "my_squar": 5, "myab": 2, "myelement": 7, "mygroup": 7, "mymap": 7, "mymorph": 7, "mynat": 4, "mynewmorph": 7, "mypoint1": 5, "mypoint2": 5, "mypoint3": 5, "myre": 1, "mysmul": 6, "mysquar": 5, "mysteri": [1, 5, 6], "mz": 4, "m\u02e3": 7, "n": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "n_p": 9, "n_q": 9, "na": 2, "naiv": [6, 9], "name": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "namespac": [1, 2, 3, 4, 5, 7, 8, 9], "nash": 0, "nat": [0, 1, 2, 3, 4, 5, 7, 9], "natab": 5, "natabs_mul": 5, "natabs_norm_mod_lt": 5, "natabs_of_nonneg": 5, "natal": 0, "natcast_natab": 5, "natdegre": 7, "natdegree_comp": 7, "natdegree_mul": 7, "natur": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "nb": 2, "ne": [4, 5], "nearbi": [1, 4], "nearest": 5, "nebot": 9, "nebot_of_l": 9, "necessari": [0, 2, 4, 5, 7, 8], "necessarili": [1, 8, 11], "need": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "neg": [5, 6, 9, 11], "neg_add": 6, "neg_add_cancel": [1, 5], "neg_add_cancel_left": 1, "neg_def": 5, "neg_eq_of_add_eq_zero": 1, "neg_im": 5, "neg_le_abs_self": 2, "neg_mem": 7, "neg_neg": 1, "neg_r": 5, "neg_zero": 1, "negat": [1, 5, 13], "negsucc": 6, "neighborhood": 9, "neither": [3, 5, 6, 8], "neq": 4, "nest": [1, 2], "net": 1, "neutral": [6, 7], "never": [0, 6], "new": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "newcom": 0, "next": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "nge": 2, "nhd": 9, "nhds_basis_bal": 9, "nhds_basis_closedbal": 9, "nhds_basis_ioo_po": 9, "nhds_basis_open": 9, "nhds_induc": 9, "nhds_mkofnhd": 9, "nhds_prod_eq": 9, "nice": [1, 2, 4, 6, 7, 8, 9], "nicer": [5, 7, 9], "nicola": 0, "nineteenth": 3, "nna": 2, "nnc": 2, "nnez": 4, "nnf": 2, "nng": 2, "nnz": 4, "non": [1, 3, 6, 7, 8, 9, 11], "noncomm_r": 1, "noncomput": [3, 5, 7, 8], "nonconstruct": 7, "nondecreas": [2, 4], "nondistribut": 1, "nonempti": [3, 7, 9], "nonempty_interior_of_iunion_of_clos": 10, "nonexist": 2, "nonneg": [1, 5], "nonneg_of_mul_nonneg_left": 1, "nontrivi": [2, 3, 4, 5, 8, 9, 10], "nontriviallynormedfield": [10, 11], "nonzero": [2, 4, 5, 11], "nor": [3, 5, 8], "norm": [2, 5, 9, 13], "norm_add_l": 10, "norm_conj": 5, "norm_eq_zero": [5, 10], "norm_mod_lt": 5, "norm_mul": [5, 10], "norm_nonneg": [5, 10], "norm_num": [1, 2, 4, 5, 8], "norm_po": 5, "norm_smul": 10, "norm_y_po": 5, "normal": 7, "normedaddcommgroup": [10, 11], "normedaddgroup": 10, "normedfield": 10, "normedgroup": 10, "normedspac": [10, 11], "not_even_iff": 3, "not_even_iff_odd": 3, "not_imp_self": 3, "not_le_of_gt": 2, "not_lt_of_g": [2, 4, 5], "not_monotone_iff": 2, "not_norm_mul_left_lt_norm": 5, "not_not": 2, "notat": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "note": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "noth": [1, 2, 3, 4, 5, 6, 7], "notic": [1, 2, 3, 4, 5, 7, 9], "notin": 3, "notion": [1, 2, 3, 4, 5, 7, 8, 9, 10, 11], "noun": 6, "now": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "nozerodivisor": 7, "np": 4, "npow_nz": 4, "npowz": 4, "nsmul": [5, 6], "nsmul_succ": 6, "nsmul_zero": 6, "nsmulrec": 5, "nsmul\u2081": 6, "nsqr_nez": 4, "nt": 2, "nth_rw": 1, "number": [0, 1, 2, 3, 5, 6, 7, 8, 9, 10, 13], "numer": [1, 4, 5], "nut": 1, "n\u2080": 2, "n\u2081": 2, "o": 10, "obfusc": 9, "object": [0, 1, 2, 3, 4, 5, 7, 8, 13], "observ": [2, 4, 9], "obtain": [1, 2, 4, 5, 9, 10], "obviou": [0, 4, 5, 6], "occasion": 9, "occur": 4, "occurr": 1, "odd": [1, 2, 3, 4, 8], "odd_iff": 3, "of_fintype_basi": 8, "of_foral": 9, "of_le_succ": 4, "of_map": 9, "ofbiject": [7, 8], "off": [2, 3, 4], "offend": 6, "offer": [0, 2, 5, 9], "ofnat": 6, "ofnat_l": 5, "ofnat_lt": 5, "ofreal": 7, "often": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "og": 2, "old": [2, 5, 6, 8], "oliv": 0, "omit": 5, "onc": [1, 2, 3, 4, 5, 6, 7, 9, 11], "one": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "one_add_one_eq_two": 1, "one_def": 5, "one_dia": 6, "one_eq_top": 7, "one_fin_two": 8, "one_im": 5, "one_mem": [6, 7], "one_mul": [1, 2, 5, 6], "one_r": 5, "one_smul": [6, 7, 8], "oner": 1, "ones": [0, 1, 2, 3, 5, 8, 11], "one\u2081": 6, "one\u2082": 6, "onli": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "onlin": 0, "onto": [7, 8], "open": [0, 1, 2, 3, 4, 5, 7, 8, 10, 11], "oper": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "opnorm_le_bound": 10, "opnorm_le_of_shel": 10, "opportun": [7, 9], "opposit": [6, 9], "optim": [6, 8, 11], "option": [1, 2, 4, 5, 6, 9], "orbit": 7, "orbitequivquotientstabil": 7, "orbitrel": 7, "order": [1, 2, 3, 4, 5, 6, 8, 9, 10], "orderedcanceladdcommmonoid": 2, "orderedcommmonoid\u2081": 6, "orderpreshom": 6, "orderpreshomclass": 6, "orderpresmonoidhom": 6, "ordinari": [1, 2, 4, 5, 7, 8, 9], "ordinarili": [4, 5], "organ": 0, "organiz": 1, "orient": 5, "origin": [0, 1, 5, 7], "other": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "otherwis": [1, 2, 3, 4, 5, 7], "ott": 0, "our": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "ourselv": [4, 6], "out": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "outer": 1, "outermost": 3, "outlin": [1, 2, 4, 9], "outparam": 6, "output": [1, 7], "outsid": [1, 4, 8], "over": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "overlap": [6, 7], "overload": 3, "overview": 13, "own": [0, 1, 4, 5, 6], "p": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "p4": 4, "p4eq": 4, "p_1": 4, "p_i": [4, 9], "p_k": 4, "p_n": 4, "p_ne_zero": 7, "packag": [7, 8], "page": [0, 1, 4], "pai": [1, 2, 6, 7, 9], "pain": 7, "pair": [1, 2, 4, 5, 7, 9], "pairwis": [8, 11], "pairwisedisjoint": 8, "panel": 0, "paper": [2, 3, 5, 7, 8, 9, 11], "paquet": 0, "paradox": [8, 9], "paragraph": 9, "parallel": 8, "paramet": [5, 6], "parent": 6, "parenthes": [1, 2, 3, 4], "pariti": 0, "parity_simp": 0, "pars": [1, 3, 7], "part": [1, 2, 3, 4, 5, 6, 8, 9, 11], "partial": [0, 1, 2, 3, 5, 6, 7, 8], "partialord": [1, 2], "partialorder\u2081": 6, "particular": [1, 2, 5, 6, 7, 8, 9], "partit": 7, "partli": [1, 6, 7], "pass": [1, 5], "past": [0, 1, 7], "path": 6, "patholog": 9, "pattern": [1, 2, 3, 5, 6], "payoff": 5, "pdf": 0, "pdvd": 4, "pedro": 0, "peel": 2, "pen": [2, 7], "peopl": [0, 1], "perform": [1, 2, 3], "perm": [5, 7], "permgroup": 5, "permiss": 1, "permut": [4, 7], "person": 0, "perspicu": 2, "phenomenon": 3, "phrase": [0, 1, 2, 4, 5, 8], "pi": [7, 8, 9], "pick": [0, 6], "pictur": [4, 5, 7], "piec": [1, 4, 5, 6, 7, 9], "pierpaolo": 0, "pietro": 0, "pim": 0, "pinot": 7, "piotrowski": 0, "place": [0, 1, 2, 5, 8, 9], "placehold": 2, "placement": 4, "plai": [1, 3, 4, 6, 7, 8, 9], "plan": [1, 6, 9], "plane": 9, "plausibl": 3, "ple": 4, "pltn": 4, "pne3": 4, "point": [0, 1, 2, 3, 5, 6, 7, 8, 9, 10, 11], "pointwis": [5, 9, 10], "polynomi": [5, 8], "ponen": 1, "poor": 6, "pop": 0, "port": 0, "posit": [1, 3, 4, 5, 9, 11], "possibl": [1, 2, 3, 4, 5, 7, 9], "possibli": 5, "postfix": 6, "pos\u2080": 2, "potscrubb": 0, "pow_eq": 4, "pow_eq_zero": [2, 4], "pow_succ": 4, "pow_two": [1, 4], "pow_two_le_fac": 4, "pow_two_nonneg": [1, 2], "power": [0, 1, 3, 4, 5, 6, 8], "pp": 4, "pq": 8, "practic": [1, 2, 3, 6, 7, 9], "pragmat": 5, "pre": [2, 8], "preal": 5, "preced": [4, 7], "precis": [1, 3, 7, 8, 9, 10], "precondit": 9, "pred": 4, "predecessor": 4, "predic": [2, 3, 4, 6, 7, 8, 9, 10], "prefer": [0, 1, 2, 3], "prefix": [4, 6, 7], "preimag": [3, 7, 8, 9], "preliminari": 6, "prematur": 6, "preorder": [2, 6, 9], "preorder\u2081": 6, "presenc": 6, "present": [1, 2, 4, 7, 9], "presentedgroup": 7, "preserv": [4, 6, 8, 9], "preserves_mul": 5, "press": [0, 8], "presuppos": 0, "pretend": [6, 8], "pretti": [2, 6, 7, 8, 9], "previou": [1, 2, 3, 5, 6, 7, 9, 10, 11], "previous": 6, "price": 9, "primari": 6, "primarili": [6, 7, 9], "prime": [1, 2, 3, 5, 6, 7, 8, 13], "prime_def_lt": 4, "prime_iff": 3, "prime_of_mem_primefactorslist": 4, "prime_p": 4, "prime_q": 4, "prime_thre": 4, "prime_two": 4, "prime_x": 3, "primefactorslist": 4, "primefactorslist_uniqu": 4, "primes_infinit": 4, "primes_mod_4_eq_3_infinit": 4, "primit": [2, 3], "princip": 9, "principl": [1, 2, 3, 4, 6, 8, 10], "print": [0, 3, 4, 5, 11], "priori": [6, 8], "prioriti": 5, "probabl": [1, 5, 6, 9], "problem": [3, 4, 5, 6, 9], "proce": [4, 6], "procedur": [4, 6], "proceed": 7, "prod": [4, 7, 8, 9, 11], "prod_": 4, "prod_empti": 4, "prod_insert": 4, "prod_map": 9, "prod_mk": 9, "prod_po": 4, "prod_primefactorslist": 4, "prod_range_succ": 4, "prod_range_zero": 4, "prodcongr": 7, "prodequivpi": 7, "prodmap": 8, "produc": [1, 2, 7, 10], "product": [2, 4, 5, 6, 7, 9, 11], "profici": 4, "program": [0, 1, 2], "progress": [0, 1, 5, 7], "prohibit": 9, "proj": 8, "project": [0, 4, 5, 7, 8, 9], "projector": 7, "promin": 7, "promis": [6, 8, 9], "promot": 1, "proof": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "prop": [0, 2, 3, 4, 5, 6, 7, 8, 9, 11], "propag": 6, "properti": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "proposit": [0, 2, 3, 4, 5], "protect": 5, "provabl": [1, 3, 6, 9], "prove": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "proven": [7, 8], "provid": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "proxi": 5, "pseudoemetricspac": 9, "pseudometricspac": 9, "psycholog": 6, "pull": [0, 7, 9], "pullback": [7, 9], "pun": 2, "pure": [1, 9], "pure_le_nhd": 9, "purpos": [1, 2, 3, 4, 5, 6, 8, 9], "push": [2, 4, 7, 9], "push_neg": [2, 3, 4], "push_pul": 9, "pushforward": [7, 9], "put": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "q": [2, 4, 5, 6, 7, 8, 9], "qk": 4, "quad": 5, "quadrat": 5, "quantifi": [1, 3, 4, 5, 7, 9, 13], "quantiti": 9, "quest": 6, "question": [0, 4, 6, 9, 11], "quick": [4, 7, 8, 10], "quicker": 0, "quickli": [3, 7, 11], "quirki": 4, "quit": [2, 6, 9], "quot": [5, 8, 9], "quotequivofeq": 7, "quotient": [4, 5, 6, 9, 13], "quotient_mul_add_remainder_eq": 5, "quotient_zero": 5, "quotientgroup": 7, "quotientinfringequivpiquoti": 7, "quotientkerequivrang": 7, "quotientmap": 7, "quotientmonoid": 6, "quotientmulequivofeq": 7, "quotkerequivrang": 8, "r": [1, 2, 4, 5, 6, 7, 8, 9], "r_wellfound": 5, "radiu": 9, "raini": 3, "rais": [1, 4], "random": 6, "rang": [0, 2, 3, 4, 7, 8, 9], "range_eq_map": 8, "range_eq_top": 8, "range_mkq": 8, "rank": 8, "rare": 6, "rather": [0, 1, 2, 4, 5, 6, 7, 8, 9], "ration": [1, 2, 4, 9], "rb": 9, "rcase": [2, 3, 4, 9], "rclike": 10, "re": [4, 5], "reach": [2, 6], "read": [0, 1, 4, 5, 6, 7, 8, 9], "readabl": [1, 2, 3, 8, 9], "reader": [1, 8, 9], "readi": [4, 6, 7, 8, 9, 10], "real": [1, 2, 3, 4, 5, 6, 8, 9, 10, 11], "real_norm_l": 10, "realli": [1, 2, 3, 4, 6, 7, 8, 9], "reason": [0, 1, 2, 4, 5, 6, 7, 8, 9], "rec_on": 9, "recal": [1, 2, 4, 5, 7, 9, 11], "recaptur": 9, "recast": 9, "recent": 5, "recogn": [1, 2, 4, 5, 6, 9], "recommend": [0, 1, 3], "recon": 9, "reconcil": 2, "record": [5, 6, 8], "recov": 9, "recurs": [2, 3, 5, 13], "redefin": [5, 6], "reduc": [0, 2, 3, 4, 5], "reduct": [2, 3, 5], "redund": [1, 5, 8, 9, 11], "refer": [0, 1, 2, 4, 5, 6, 8, 9, 10], "refin": [4, 10], "refl": [2, 3, 5, 6, 7, 8], "refl_tran": 5, "reflect": 2, "reflex": [1, 2, 5], "reformul": 9, "refus": [6, 9], "regiment": 0, "region": 3, "regist": [5, 6, 7, 8], "regular": [6, 9], "regularspac": 9, "rel": [3, 5, 8], "relat": [1, 2, 3, 5, 6, 7, 8, 9, 10, 11], "relatedli": 9, "relationship": [3, 4], "relativ": 3, "relev": [0, 1, 2, 4, 5, 6, 7, 8, 9], "reli": [1, 2, 5, 9], "remain": [0, 1, 2, 3, 5, 6, 9], "remaind": [4, 5, 7], "remainder_lt": 5, "remark": [5, 6], "rememb": [1, 2, 3, 4, 5, 6, 7, 8, 9], "remov": [4, 9], "renam": 0, "render": [2, 4], "repeat": [1, 4, 5, 6], "repeatedli": [2, 9], "repetit": [1, 6], "replac": [0, 1, 2, 3, 4, 6, 7, 8], "replai": 0, "report": 1, "repositori": [0, 1], "repr": 8, "repres": [0, 1, 2, 3, 4, 5, 6, 10], "represent": [3, 4, 5, 8], "reproduc": 5, "reprov": [1, 7, 8], "requir": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "resolut": 6, "resolve_left": 3, "resourc": 0, "resp": 8, "respect": [1, 2, 3, 4, 5, 7, 8, 9], "respons": [0, 1], "rest": [2, 3, 5, 7, 9], "restat": [2, 6, 7, 8], "restor": 6, "restrict": [3, 4, 7, 9], "result": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "retri": 6, "return": [0, 2, 3, 4, 5, 7, 8, 9], "reus": 6, "reusabl": 6, "reveal": [1, 8], "revers": [1, 2, 3, 5, 9], "revert": [4, 5], "review": [7, 9], "rewrit": [0, 1, 2, 3, 4, 5, 6, 8, 9], "rewritten": 3, "rfl": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "rich": [5, 6], "rid": 2, "right": [1, 2, 3, 4, 5, 6, 8, 9, 10], "right_distrib": [5, 6], "right_inv": [5, 8], "rightinvers": 3, "ring": [0, 1, 2, 3, 4, 5, 6, 8, 13], "ringequiv": 7, "ringhom": [6, 7], "ringhomclass\u2083": 6, "ringhom\u2081": 6, "ring\u2081": 6, "ring\u2083": 6, "rintro": [0, 2, 3, 4, 7, 8, 9], "rise": [4, 6, 7], "road": 5, "robust": [5, 6], "role": [4, 5, 8, 9], "roll": 10, "rolland": 0, "roman": 5, "root": [5, 6, 7, 8, 13], "roots_mul": 7, "roots_x_sub_c": 7, "roughli": [2, 3, 4], "round": [0, 1, 5], "routin": 2, "row": 8, "rpo": 9, "rule": [0, 2, 4, 5, 6, 8, 9], "run": 0, "rush": 0, "russel": 8, "rw": [0, 2, 3, 4, 5, 6, 7, 8, 9, 13], "rwa": [3, 4, 5], "r\u02e3": 7, "s_": 3, "s_0": [2, 3], "s_1": 2, "s_2": 2, "s_n": [2, 3], "sa": 2, "sad": 9, "safe": [6, 7], "safer": 7, "sage": 8, "sai": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "said": [0, 2, 4, 5], "sake": [1, 4], "salient": 9, "same": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "satisfi": [1, 3, 4, 5, 6, 9, 10], "save": 2, "saw": [1, 5, 6, 7, 8, 9], "sb": 2, "sb_fun": 3, "sb_inject": 3, "sb_right_inv": 3, "sb_surject": 3, "sbaux": 3, "sbfun": 3, "sbset": 3, "scalar": [5, 6, 7, 8, 10], "scale": 3, "scari": 5, "scheme": 5, "schroeder_bernstein": 3, "schr\u00f6der": 13, "scienc": 6, "scientist": 2, "scope": [1, 2, 3, 5, 7, 8], "scratch": 2, "script": 1, "search": [4, 5, 6], "second": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "secretli": 8, "section": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "see": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "seek": 5, "seem": [1, 2, 4, 6, 9, 10], "seen": [0, 1, 2, 4, 5, 6, 7, 8, 9], "segment": [9, 11], "select": [0, 9], "self": 6, "self_of_nhd": 9, "self_sub": 1, "self_trans_symm": [5, 7, 8], "selfequivsigmaorbit": 7, "selfmodul": 6, "semi": [6, 7, 8], "semicolon": [2, 4], "semigroup": 6, "semigroup\u2081": 6, "semigroup\u2082": 6, "semigroup\u2083": 6, "semir": [6, 7], "send": [7, 8, 11], "sens": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10], "sensibl": 9, "sent": [7, 9], "separ": [0, 1, 2, 4, 5, 8], "sequenc": [3, 6, 9, 10, 13], "seri": 7, "seriou": [4, 6, 9], "serv": [1, 3, 4, 5, 11], "set": [0, 1, 2, 4, 5, 6, 7, 10, 11, 13], "set_opt": 6, "setco": 6, "setintegral_const": 11, "setlik": 6, "setminu": 3, "setoid": [6, 7], "sets_of_superset": 9, "setub": 2, "setup": [7, 8], "seurin": 0, "sever": [6, 8, 9, 11], "shade": 3, "shame": 6, "sharp": 0, "shift": [0, 1, 6, 9], "short": [0, 1, 2, 3, 4, 5, 8], "shorten": [1, 2, 7], "shorter": [1, 3, 4, 7, 9], "shot": 9, "should": [0, 1, 2, 3, 4, 5, 6, 7, 9, 10], "shouldn": [8, 9], "show": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "shown": [1, 5, 10, 11], "side": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "sight": [2, 6], "sigma": [5, 11], "sigmafinit": 11, "sign": 9, "signatur": 6, "signific": 3, "silent": [5, 6], "silli": 6, "silva": 0, "similar": [1, 2, 3, 5, 6, 7, 8, 9], "similarli": [2, 3, 4, 5, 7, 8], "simp": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10], "simp_rw": 7, "simpa": [4, 7, 10], "simpl": [2, 4, 5, 6, 10], "simpler": [6, 8], "simplex": 5, "simpli": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "simplif": [2, 3, 4], "simplifi": [0, 2, 3, 4, 5, 9, 11], "sin": [2, 10], "sinc": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "singl": [0, 1, 2, 3, 4, 5, 6, 7, 8, 10], "singleton": 4, "sinter": 3, "sinter_eq_biint": 3, "situat": [1, 3, 6, 7, 9], "size": 8, "skeleton": [5, 8, 9], "sketch": [2, 3, 4, 9], "skill": [0, 1, 2, 3, 4], "slick": 2, "slight": 3, "slightli": [1, 6, 7, 8, 9, 10], "slow": 9, "small": [0, 2, 4, 5, 9], "smaller": [3, 4, 9], "smallest": [4, 6, 8, 9], "smart": 4, "smul": [5, 6, 7, 8], "smul_add": [6, 8], "smul_comm": 8, "smul_distrib": 5, "smul_mem": 8, "smul_zero": 8, "smul\u2083": 6, "snd": [5, 8, 9], "snippet": [2, 4, 5, 7, 8], "so": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "solut": [0, 1, 4, 6], "solv": [0, 1, 2, 3, 4, 5, 6, 8, 9], "some": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "somehow": [7, 8], "someth": [0, 1, 2, 4, 6, 8, 9], "sometim": [1, 2, 3, 4, 5, 6, 7, 8, 9], "somewhat": [1, 3, 9], "somewher": 9, "soon": [0, 2, 6, 7, 8, 9], "sophist": 9, "sorri": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "sort": [1, 3, 4], "sosi": 2, "sosx": 2, "sound": [3, 5, 6], "sourc": [2, 9], "space": [1, 2, 3, 5, 6, 7, 11, 13], "span_eq": 8, "span_induct": 8, "span_l": 8, "span_union": 8, "speak": [2, 5, 7, 9], "special": [3, 4, 5, 6, 7, 8, 9, 11], "specif": [0, 1, 3, 4, 5, 6], "specifi": [1, 2, 3, 4, 5, 8, 9, 10, 11], "spell": [8, 9], "split": [1, 2, 3, 4], "spot": 2, "sq_ab": 5, "sq_add_sq_eq_zero": 5, "sq_nonneg": 1, "sqr_eq": 4, "sqrt": [2, 3, 4, 5], "squar": [1, 2, 4, 5, 6, 7, 8], "squiggli": 2, "ss": 3, "ssubt": 3, "stabil": 7, "stabl": 8, "stage": [2, 5, 6], "stai": 5, "stand": [1, 2, 4, 5, 6, 7, 8, 9, 10], "standard": [4, 5, 6, 9], "standardsimplex": 5, "standardtwosimplex": 5, "start": [1, 2, 3, 4, 6, 7, 8, 9, 10, 11, 13], "state": [0, 1, 2, 3, 4, 6, 7, 8, 9, 10], "statement": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "stdsimplex": 5, "steep": 0, "steinhau": 10, "step": [0, 1, 2, 3, 4, 5, 6], "steven": 0, "stick": [1, 2, 9, 10], "still": [0, 1, 2, 3, 4, 5, 6, 8, 9, 11], "stipul": 10, "stop": 6, "store": 5, "stori": [6, 8], "str": 5, "straightforward": [2, 6], "strang": [2, 4, 7, 8], "strategi": [1, 2, 4], "strength": 1, "strengthen": [1, 2, 4], "stretch": [4, 5], "strict": [1, 2], "stricter": 10, "strictli": [1, 2, 10], "strictmono": 9, "strictorderedr": 1, "strike": [1, 2], "strong": [2, 4], "strong_induction_on": 4, "stronger": 9, "strongli": 0, "stronglymeasurableatfilt": 11, "struc": 5, "structur": [2, 4, 6, 7, 9, 10, 11, 13], "stuck": 6, "studi": [6, 9], "style": [0, 1], "sub": [3, 9, 11, 13], "sub_add_cancel": 1, "sub_eq_add_neg": 1, "sub_self": [1, 2], "sub_sub": 1, "subgoal": 2, "subgroup": 6, "subgroupclass\u2081": 6, "subgroupofmulact": 7, "subgroup\u2081": 6, "subject": 5, "submodul": [7, 8], "submodule_independ": 8, "submodule_isup_eq_top": 8, "submonoid": [6, 7], "submonoidclass\u2081": 6, "submonoid\u2081": 6, "submonoid\u2081monoid": 6, "subobject": 6, "subproof": 1, "subr": 6, "subscript": [1, 8], "subsequ": [2, 4, 9], "subset": [1, 2, 3, 5, 9, 10], "subset_def": 3, "subset_iff": 4, "subspac": [1, 6, 13], "substant": 4, "substanti": 0, "substitut": [0, 2], "subsum": 4, "subtl": [5, 7, 8, 9], "subtleti": [6, 7, 8], "subtract": [1, 4, 5], "subtyp": [5, 6, 7, 8, 9], "succ": [4, 6], "succ_add": 4, "succ_le_succ": 4, "succ_mul": 4, "succ_ne_zero": 4, "succ_po": 4, "succe": 6, "success": 6, "successor": [4, 8], "suffic": [1, 2, 3, 7, 9], "suffici": [4, 9], "suggest": [0, 2, 4, 5, 8, 9], "suitabl": [0, 1, 2, 5, 9], "sum": [1, 2, 4, 5, 6, 7, 9], "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_repr": 8, "sum_sqr": 4, "summand": 8, "summat": 4, "sumofsquar": 2, "sumofsquares_mul": 2, "sunion": 3, "sunion_eq_biunion": 3, "sup": [1, 4, 9], "sup_assoc": 1, "sup_comm": 1, "sup_eq_closur": 7, "sup_eq_top": 8, "sup_inf_left": 1, "sup_inf_right": 1, "sup_inf_self": 1, "sup_l": 1, "superfici": 9, "superscript": 9, "supersed": 8, "suppli": 5, "support": [0, 1, 2, 3, 4, 5, 6, 8, 9], "suppos": [1, 2, 3, 4, 5, 9], "suppress": 1, "supremum": [1, 4, 6, 7, 8], "sure": [0, 1, 2, 3, 5, 6, 7, 8], "surject": [2, 3, 7, 8, 9], "surjf": [2, 3], "surjg": 2, "surpris": 6, "surprisingli": [5, 6], "swap": 5, "swapxi": 5, "sweet": 3, "switch": [1, 6], "sylow": 7, "symbol": [1, 2, 5, 6, 7], "symm": [3, 4, 5, 6, 7, 8, 9, 10], "symmetr": [2, 3, 7], "symmetri": [3, 6], "synonym": 7, "syntact": 2, "syntax": [0, 1, 2, 4, 6, 8], "synth": 6, "synthes": [5, 6], "synthesi": 8, "synthinst": 6, "system": [3, 4, 5, 6, 8], "s\u00e1nchez": 0, "s\u02e3": 7, "s\u1d9c": [9, 11], "s\u2081": 6, "s\u2082": 6, "t": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "t2space": 9, "t3space": 9, "t_": 9, "t_3": 9, "t_x": 9, "t_y": 9, "t_z": 9, "tab": [1, 3, 4], "tackl": 6, "tactic": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "tag": [2, 3, 6], "take": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "taken": [1, 2], "takeshi": 0, "talk": [4, 7, 8, 9, 10], "tantamount": [1, 3], "target": [1, 6, 7, 8, 9, 11], "task": [0, 2, 4, 5, 6, 9], "taught": 7, "tauto": 4, "tautologi": 4, "teach": 0, "tear": 6, "technic": [1, 5, 6, 8], "techniqu": [2, 9], "technologi": 6, "tediou": [1, 2, 6], "tell": [0, 2, 3, 4, 5, 6, 7, 8], "temporarili": [1, 2], "tempt": 6, "tend": [1, 9], "tendsto": [9, 11], "tendsto_attop": 9, "tendsto_congr": 9, "tendsto_iff": 9, "tendsto_integral_of_dominated_converg": 11, "tendsto_nhds_uniqu": 9, "tendsto_pow_attop_nhds_zero_of_lt_on": 9, "tendsto_right_iff": 9, "tendsto_subseq": 9, "tendsto\u2081": 9, "tendsto\u2082": 9, "term": [0, 1, 2, 3, 4, 5, 7, 8, 9], "terminologi": [5, 8], "terraf": 0, "ters": 6, "test": 4, "text": [0, 3, 5, 9], "textbook": [0, 1, 2], "th": [4, 8], "than": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "thank": 6, "thei": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "them": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "theme": 3, "themselv": [0, 4, 5], "theorem": [0, 2, 4, 5, 7, 8, 9, 10, 11, 13], "theoret": [2, 3, 8, 9], "theori": [0, 1, 2, 3, 6, 7, 8, 9, 10, 13], "therefor": [1, 4, 5, 8, 9], "thereof": 0, "thi": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "thing": [0, 1, 2, 3, 4, 5, 6, 8, 9], "think": [0, 1, 2, 3, 4, 5, 6, 8, 9, 10], "third": [1, 2, 3, 5, 9], "thoma": 0, "thorough": 0, "those": [0, 1, 2, 3, 5, 6, 7, 8, 9, 10], "though": [2, 3, 4, 5], "three": [1, 2, 4, 5, 7, 9], "through": [0, 1, 3, 4, 5, 6, 7, 8, 9], "thu": [1, 3, 4, 5, 9], "thumb": 4, "tighter": [1, 3], "tightli": 5, "time": [1, 4, 5, 6, 8, 9, 10, 11], "timesav": 1, "tiresom": 9, "to_addit": 6, "to_localinvers": 10, "toaddcommgroup\u2083": 6, "toaddgroup\u2083": 6, "todiaoneclass\u2081": 6, "todia\u2081": 6, "tofun": [5, 6, 8], "togeth": [1, 2, 3, 4, 5, 7, 9], "togroup": 7, "tomatrix": 8, "tomatrix_comp": 8, "tomatrix_id": 8, "tomatrix_mulvec_repr": 8, "tomodul": 8, "tomonoidhom\u2081": 6, "tomuloneclass": 6, "too": [0, 1, 3, 5, 6, 7, 8, 9], "toohei": 0, "tool": [0, 1, 5, 6], "toone\u2081": 6, "top": [0, 6, 7, 8, 9, 10], "topermhom": 7, "topic": [4, 5, 6, 7, 8], "topolog": [5, 6, 10, 13], "topologi": [1, 5, 6, 10, 13], "topologicalspac": [9, 10], "toreal": 11, "tortuou": 8, "tosemigroup\u2081": 6, "tosmul\u2083": 6, "total": 1, "tour": [9, 10], "toward": 7, "trace": [6, 8], "tradeoff": 3, "tradition": 7, "train": [1, 6], "tran": [1, 2, 4, 5, 6, 7, 8], "trans_assoc": 5, "trans_refl": 5, "transform": [2, 3], "transit": [1, 2, 5, 9], "translat": [4, 6, 7, 9], "transpos": 8, "trap": 6, "treat": [2, 3, 5, 6, 7, 9, 10], "treatment": 7, "tri": [1, 2, 4, 6], "triangl": [1, 2, 5], "trick": [1, 2, 4, 6, 10], "tricki": [2, 3, 4, 6, 7], "trigger": [6, 8], "tripl": 3, "trivial": [3, 4, 7, 8, 9], "troubl": [2, 3, 5], "true": [1, 2, 3, 6, 8, 9], "truncat": 4, "trust": 8, "truth": [1, 4], "try": [0, 1, 2, 3, 4, 5, 6, 8, 9], "tucker": 0, "tupl": 5, "turn": [2, 3, 4, 5, 6, 8, 9, 10], "tutori": 0, "twice": [0, 1, 9], "two": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "two_l": 4, "two_le_of_mod_4_eq_3": 4, "two_mul": 1, "ty": 7, "type": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "typeclass": [6, 8], "typic": [1, 7], "u": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "u_2": 8, "u_n": 8, "ubf": 2, "ubfa": 2, "ubg": 2, "ubgb": 2, "ulequiv": 7, "ultim": 0, "un": 3, "unapp": 1, "unbundl": 6, "unchang": [1, 2], "uncom": 1, "uncount": 9, "uncurri": 9, "under": [5, 6, 7, 8, 9], "underli": [0, 1, 5, 6, 7, 8], "underneath": [1, 3], "underscor": [1, 2, 3, 8], "understand": [0, 2, 3, 4, 5, 6, 7, 8, 9], "understood": [4, 9], "unfold": [1, 2, 3, 4, 5, 9], "unfortun": 7, "unicod": [1, 3, 6], "unif": 6, "uniform": [3, 9, 10], "uniformcontinu": 9, "uniformcontinuous_iff": 9, "uniformli": 10, "union": [1, 3, 4, 5, 6, 7, 8, 10, 11], "union_def": 3, "uniqu": [1, 2, 3, 4, 5, 7, 8, 9], "unit": [5, 6, 9], "units_eq_one_or": 7, "univ": [3, 9, 10, 11], "univ_set": 9, "univari": 7, "univers": [1, 3, 5, 7, 8, 9, 13], "unknown": 6, "unless": [1, 2, 5], "unlik": [3, 4], "unnecessari": [3, 7], "unneed": 8, "unpack": [2, 3], "unpleas": [6, 9], "unrel": 6, "unshad": 3, "unspecifi": [6, 8], "unsurprisingli": 3, "until": [1, 4, 6, 9], "up": [0, 2, 3, 4, 5, 6, 7, 9], "updat": 0, "upper": [1, 2], "us": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "usabl": 6, "usag": 1, "useless": 8, "user": [0, 6], "usual": [1, 2, 3, 4, 5, 7, 8, 9, 11], "v": [0, 1, 2, 3, 5, 8, 9], "val": 5, "valid": 2, "valu": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "van": 0, "vandermond": 8, "vanish": [7, 8], "varepsilon": [2, 9], "variabl": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "variant": [1, 2, 7, 9], "variat": [1, 3, 4, 5, 9, 10], "varieti": 9, "variou": [2, 3, 5, 6, 8, 11], "vastli": 2, "ve": [6, 9], "vecmul": 8, "vector": [1, 3, 6, 7, 10, 13], "verbatim": 7, "verbos": 3, "veri": [0, 2, 4, 6, 7, 8, 9, 11], "verifi": 2, "versa": [1, 3], "version": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "vertic": [2, 5, 8], "vi": 5, "via": 9, "vice": [1, 3], "victor": 0, "view": [5, 6, 7, 9], "virtual": 8, "visibl": 1, "vocabulari": [3, 8], "volum": 11, "w": [1, 6, 8], "wa": [1, 3, 7], "wai": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "want": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "wasn": 9, "we": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "weak": 6, "weaker": [1, 2], "weav": 5, "web": [0, 1, 4], "weight": 5, "weightedaverag": 5, "weird": [6, 9], "weirder": 10, "welcom": [0, 1], "well": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "were": [2, 4, 5, 8, 9], "what": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "whatev": [0, 2, 4], "whatsnew": 6, "when": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "whenev": [1, 2, 4, 5, 8], "where": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "wherea": [0, 1, 2, 3, 5, 7, 9], "wherebi": [5, 9], "whether": [2, 3, 4, 6, 9], "which": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "while": [0, 1, 2, 6, 7, 8, 9], "who": [0, 9], "whole": [5, 8], "whose": [1, 2, 4, 5, 6, 7, 8, 9, 10], "why": [0, 2, 4, 6, 7, 8, 9], "wieser": 0, "window": [0, 1, 2, 5], "winston": 0, "wise": [5, 8], "wish": 9, "withbot": 7, "within": [1, 2, 9], "without": [1, 2, 4, 5, 6, 7, 8, 9, 10], "withtop": 10, "wlog": 3, "won": [2, 4, 6, 7, 9], "wonder": 8, "word": [1, 2, 3, 4, 5, 7, 8, 9], "work": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "world": 0, "worri": [1, 3, 4, 5, 7], "worth": [1, 2, 5], "would": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "wouldn": 6, "wrap": [6, 9], "write": [0, 1, 2, 4, 5, 6, 7, 8, 9, 10, 11], "written": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "wrong": 3, "wrote": 4, "x": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "x_0": 9, "x_1": [2, 3], "x_2": [2, 3], "x_i": 9, "x_nonneg": 5, "xa": 3, "xai": 3, "xeq": [2, 3], "xgt": 2, "xlt": 2, "xltz": 2, "xmem": 3, "xnt": 3, "xnu": 3, "xpo": 3, "xstu": 3, "xsu": 3, "xt": 3, "xtu": 3, "xu": 3, "xy": [2, 5], "x\u2080": [9, 10], "x\u2081": [2, 3, 5, 9], "x\u2081a": 3, "x\u2082": [2, 3, 5], "x\u2082a": 3, "x\u2082eq": 3, "x\u2082na": 3, "y": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "y_nonneg": 5, "yannick": 0, "yball": 9, "yeq": 2, "yet": [2, 3, 4, 5, 6, 8, 9], "yield": [1, 2, 3, 4, 5, 9], "ylim": 9, "ylt": 2, "you": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "your": [0, 1, 2, 3, 5, 6, 7, 9], "yourself": [2, 5], "ypo": 3, "y\u2080": 9, "y\u2081": 5, "y\u2082": 5, "z": [0, 1, 2, 5, 6, 7, 8, 9, 10, 11], "z_nonneg": 5, "zermelo": 2, "zero": [2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "zero_add": [1, 4, 5, 6], "zero_def": 5, "zero_dvd_iff": 4, "zero_im": 5, "zero_l": [4, 5], "zero_lt_on": [2, 4], "zero_lt_two": 5, "zero_mem": [7, 8], "zero_mul": [1, 4, 5, 6], "zero_r": 5, "zero_smul": [6, 8], "zeroth": 8, "zf": 2, "zlty": 2, "zmod": 7, "zsmul": [5, 6], "zsmulrec": 5, "zsmul\u2081": 6, "zulip": [0, 4], "z\u2080": 9, "z\u2081": 5, "z\u2082": 5, "\u00b9": [1, 3, 5, 6, 7, 8, 9], "\u02e2": 9, "\u03b1": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "\u03b2": [1, 2, 3, 5, 6, 8, 9, 11], "\u03b3": [1, 2, 5, 9], "\u03b4": [2, 9], "\u03b4po": 9, "\u03b5": [2, 9, 10], "\u03b52po": 2, "\u03b5_po": [9, 10], "\u03b5k_po": 10, "\u03b5po": [2, 9], "\u03b8": 8, "\u03b9": [7, 8, 9, 10, 11], "\u03bc": [9, 11], "\u03bd": 11, "\u03c0": [7, 8, 9, 10], "\u03c1": 8, "\u03c3": [5, 7], "\u03c6": [7, 8, 9], "\u03c8": [7, 8], "\u03c9": 7, "\u1d40": 8, "\u1d50": 11, "\u1d65": [7, 8], "\u1d9c": 7, "\u1da0": [9, 10, 11], "\u2080": [3, 8], "\u2081": 6, "\u2090": 7, "\u2097": 8, "\u2102": [1, 5, 7, 8, 10], "\u2115": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "\u211a": [1, 4, 7, 8, 9], "\u211d": [1, 2, 3, 5, 6, 7, 8, 9, 10, 11], "\u2124": [1, 4, 5, 6, 7, 8], "\u2124\u02e3": 7, "\ud835\udcdd": [9, 10, 11], "\ud835\udcdf": 9, "\ud835\udce4": 9, "\ud835\udd42": 10, "\ud835\udd5c": [10, 11], "\ud835\udfd9": 6}, "titles": ["1. Introduction", "2. Basics", "3. Logic", "4. Sets and Functions", "5. Elementary Number Theory", "6. Structures", "7. Hierarchies", "8. Groups and Rings", "9. Linear algebra", "10. Topology", "11. Differential Calculus", "12. Integration and Measure Theory", "Index", "Mathematics in Lean"], "titleterms": {"The": [2, 3], "about": 1, "action": 7, "algebra": [1, 5, 7, 8], "appli": 1, "asymptot": 10, "ball": 9, "base": 8, "basic": [1, 6], "bernstein": 3, "build": 5, "calcul": 1, "calculu": 10, "close": 9, "compact": 9, "comparison": 10, "complet": [8, 9], "concret": 7, "conjunct": 2, "continu": [9, 10], "converg": [2, 9], "countabl": 9, "defin": 5, "differenti": 10, "dimens": 8, "direct": 8, "disjunct": 2, "elementari": [4, 10, 11], "endomorph": 8, "exampl": 1, "existenti": 2, "fact": 1, "filter": 9, "function": [3, 9], "fundament": 9, "gaussian": 5, "get": 0, "group": 7, "hierarchi": 6, "ideal": 7, "ident": 1, "iff": 2, "implic": 2, "index": 12, "induct": 4, "infinit": 4, "integ": 5, "integr": 11, "intern": 8, "introduct": 0, "irrat": 4, "lattic": 8, "lean": 13, "lemma": 1, "linear": [8, 10], "logic": 2, "mani": 4, "map": [8, 10], "mathemat": 13, "matric": 8, "measur": 11, "metric": 9, "monoid": 7, "more": 1, "morphism": [6, 7], "negat": 2, "norm": 10, "number": 4, "object": 6, "open": 9, "overview": 0, "polynomi": 7, "prime": 4, "product": 8, "prove": 1, "pull": 8, "push": 8, "quantifi": 2, "quotient": [7, 8], "recurs": 4, "ring": 7, "root": 4, "rw": 1, "schr\u00f6der": 3, "separ": 9, "sequenc": 2, "set": [3, 8, 9], "space": [8, 9, 10], "span": 8, "start": 0, "structur": [1, 5, 8], "sub": 6, "subgroup": 7, "subr": 7, "subspac": 8, "sum": 8, "theorem": [1, 3], "theori": [4, 11], "topolog": 9, "topologi": 9, "uniformli": 9, "unit": 7, "univers": 2, "us": 1, "vector": 8}}) + Search.setIndex({"alltitles": {"Algebraic Structures": [[5, "algebraic-structures"]], "Algebras and polynomials": [[7, "algebras-and-polynomials"]], "Asymptotic comparisons": [[10, "asymptotic-comparisons"]], "Balls, open sets and closed sets": [[9, "balls-open-sets-and-closed-sets"]], "Bases": [[8, "bases"]], "Basics": [[1, null], [6, "basics"]], "Building the Gaussian Integers": [[5, "building-the-gaussian-integers"]], "Calculating": [[1, "calculating"]], "Compactness": [[9, "compactness"], [9, "id5"]], "Complete lattice structure and internal direct sums": [[8, "complete-lattice-structure-and-internal-direct-sums"]], "Completeness": [[9, "completeness"]], "Concrete groups": [[7, "concrete-groups"]], "Conjunction and Iff": [[2, "conjunction-and-iff"]], "Continuous linear maps": [[10, "continuous-linear-maps"]], "Convergence and continuity": [[9, "convergence-and-continuity"]], "Defining structures": [[5, "defining-structures"]], "Differentiability": [[10, "differentiability"]], "Differential Calculus": [[10, null]], "Differential Calculus in Normed Spaces": [[10, "differential-calculus-in-normed-spaces"]], "Dimension": [[8, "dimension"]], "Disjunction": [[2, "disjunction"]], "Elementary Differential Calculus": [[10, "elementary-differential-calculus"]], "Elementary Integration": [[11, "elementary-integration"]], "Elementary Number Theory": [[4, null]], "Endomorphisms": [[8, "endomorphisms"]], "Filters": [[9, "filters"]], "Functions": [[3, "functions"]], "Fundamentals": [[9, "fundamentals"]], "Getting Started": [[0, "getting-started"]], "Group actions": [[7, "group-actions"]], "Groups and Rings": [[7, null]], "Groups and their morphisms": [[7, "groups-and-their-morphisms"]], "Hierarchies": [[6, null]], "Ideals and quotients": [[7, "ideals-and-quotients"]], "Implication and the Universal Quantifier": [[2, "implication-and-the-universal-quantifier"]], "Index": [[12, null]], "Induction and Recursion": [[4, "induction-and-recursion"]], "Infinitely Many Primes": [[4, "infinitely-many-primes"]], "Integration": [[11, "integration"]], "Integration and Measure Theory": [[11, null]], "Introduction": [[0, null]], "Irrational Roots": [[4, "irrational-roots"]], "Linear algebra": [[8, null]], "Linear maps": [[8, "linear-maps"]], "Logic": [[2, null]], "Mathematics in Lean": [[13, null]], "Matrices": [[8, "matrices"]], "Matrices, bases and dimension": [[8, "matrices-bases-and-dimension"]], "Measure Theory": [[11, "measure-theory"]], "Metric spaces": [[9, "metric-spaces"]], "Monoids and Groups": [[7, "monoids-and-groups"]], "Monoids and their morphisms": [[7, "monoids-and-their-morphisms"]], "More examples using apply and rw": [[1, "more-examples-using-apply-and-rw"]], "Morphisms": [[6, "morphisms"]], "Negation": [[2, "negation"]], "Normed spaces": [[10, "id3"]], "Overview": [[0, "overview"]], "Proving Facts about Algebraic Structures": [[1, "proving-facts-about-algebraic-structures"]], "Proving Identities in Algebraic Structures": [[1, "proving-identities-in-algebraic-structures"]], "Pushing and pulling subspaces": [[8, "pushing-and-pulling-subspaces"]], "Quotient groups": [[7, "quotient-groups"]], "Quotient spaces": [[8, "quotient-spaces"]], "Rings": [[7, "rings"]], "Rings, their units, morphisms and subrings": [[7, "rings-their-units-morphisms-and-subrings"]], "Separation and countability": [[9, "separation-and-countability"]], "Sequences and Convergence": [[2, "sequences-and-convergence"]], "Sets": [[3, "sets"]], "Sets and Functions": [[3, null]], "Structures": [[5, null]], "Sub-objects": [[6, "sub-objects"]], "Subgroups": [[7, "subgroups"]], "Subspace spanned by a set": [[8, "subspace-spanned-by-a-set"]], "Subspaces": [[8, "subspaces"]], "Subspaces and quotients": [[8, "subspaces-and-quotients"]], "Sums and products of vector spaces": [[8, "sums-and-products-of-vector-spaces"]], "The Existential Quantifier": [[2, "the-existential-quantifier"]], "The Schr\u00f6der-Bernstein Theorem": [[3, "the-schroder-bernstein-theorem"]], "Topological spaces": [[9, "topological-spaces"]], "Topology": [[9, null]], "Uniformly continuous functions": [[9, "uniformly-continuous-functions"]], "Using Theorems and Lemmas": [[1, "using-theorems-and-lemmas"]], "Vector spaces": [[8, "vector-spaces"]], "Vector spaces and linear maps": [[8, "vector-spaces-and-linear-maps"]]}, "docnames": ["C01_Introduction", "C02_Basics", "C03_Logic", "C04_Sets_and_Functions", "C05_Elementary_Number_Theory", "C06_Structures", "C07_Hierarchies", "C08_Groups_and_Rings", "C09_Linear_Algebra", "C10_Topology", "C11_Differential_Calculus", "C12_Integration_and_Measure_Theory", "genindex", "index"], "envversion": {"sphinx": 62, "sphinx.domains.c": 3, "sphinx.domains.changeset": 1, "sphinx.domains.citation": 1, "sphinx.domains.cpp": 9, "sphinx.domains.index": 1, "sphinx.domains.javascript": 3, "sphinx.domains.math": 2, "sphinx.domains.python": 4, "sphinx.domains.rst": 2, "sphinx.domains.std": 2}, "filenames": ["C01_Introduction.rst", "C02_Basics.rst", "C03_Logic.rst", "C04_Sets_and_Functions.rst", "C05_Elementary_Number_Theory.rst", "C06_Structures.rst", "C07_Hierarchies.rst", "C08_Groups_and_Rings.rst", "C09_Linear_Algebra.rst", "C10_Topology.rst", "C11_Differential_Calculus.rst", "C12_Integration_and_Measure_Theory.rst", "genindex.rst", "index.rst"], "indexentries": {"abel": [[1, "index-15", false], [7, "index-3", false]], "absolute value": [[1, "index-24", false]], "absurd": [[2, "index-17", false]], "anonymous constructor": [[2, "index-7", false]], "apply": [[1, "index-12", false], [1, "index-17", false]], "assumption": [[2, "index-19", false]], "bounded quantifiers": [[3, "index-3", false]], "by_cases": [[2, "index-23", false]], "by_contra": [[2, "index-14", false]], "by_contra and by_contradiction": [[2, "index-14", false]], "calc": [[1, "index-3", false]], "cases": [[2, "index-8", false]], "change": [[2, "index-2", false]], "check": [[0, "index-0", false]], "command": [[1, "index-9", false]], "commands": [[0, "index-0", false]], "commutative ring": [[1, "index-8", false]], "congr": [[2, "index-25", false]], "constructor": [[2, "index-18", false]], "continuity": [[9, "index-3", false]], "contradiction": [[2, "index-17", false]], "contrapose": [[2, "index-16", false]], "convert": [[2, "index-26", false]], "decide": [[4, "index-0", false]], "definitional equality": [[1, "index-13", false]], "differential calculus": [[10, "index-0", false]], "divisibility": [[1, "index-25", false]], "dsimp": [[2, "index-2", false]], "elementary calculus": [[10, "index-1", false]], "erw": [[2, "index-4", false]], "exact": [[1, "index-12", false], [1, "index-17", false], [1, "index-5", false]], "excluded middle": [[2, "index-22", false]], "exfalso": [[2, "index-17", false]], "exponential": [[1, "index-19", false]], "ext": [[2, "index-24", false]], "extensionality": [[2, "index-24", false]], "field_simp": [[2, "index-11", false]], "filter": [[9, "index-1", false]], "from": [[2, "index-12", false]], "gcd": [[1, "index-26", false]], "goal": [[1, "index-2", false]], "group": [[1, "index-15", false], [7, "index-2", false]], "group (algebraic structure)": [[1, "index-14", false], [7, "index-1", false]], "group (tactic)": [[1, "index-15", false], [7, "index-2", false]], "have": [[1, "index-11", false], [2, "index-12", false]], "implicit argument": [[1, "index-10", false]], "inequalities": [[1, "index-16", false]], "injective function": [[2, "index-5", false]], "integration": [[11, "index-0", false], [11, "index-1", false]], "intro": [[2, "index-0", false]], "lambda abstraction": [[2, "index-1", false]], "lattice": [[1, "index-28", false]], "lcm": [[1, "index-26", false]], "left": [[2, "index-21", false]], "let": [[2, "index-13", false]], "linarith": [[1, "index-18", false]], "linear map": [[8, "index-1", false]], "local context": [[1, "index-2", false]], "logarithm": [[1, "index-19", false]], "matrices": [[8, "index-3", false]], "max": [[1, "index-21", false]], "measure theory": [[11, "index-2", false]], "metric space": [[1, "index-30", false], [9, "index-2", false]], "min": [[1, "index-21", false]], "monoid": [[7, "index-0", false]], "monotone function": [[2, "index-3", false]], "namespace": [[1, "index-9", false]], "noncomm_ring": [[1, "index-15", false]], "norm_num": [[1, "index-20", false]], "normed space": [[10, "index-2", false]], "open": [[1, "index-9", false]], "order relation": [[1, "index-27", false]], "partial order": [[1, "index-27", false]], "proof state": [[1, "index-2", false]], "push_neg": [[2, "index-15", false]], "rcases": [[2, "index-9", false]], "real numbers": [[1, "index-1", false]], "refl and reflexivity": [[1, "index-13", false]], "reflexivity": [[1, "index-13", false]], "repeat": [[1, "index-23", false]], "rewrite": [[1, "index-0", false]], "rfl": [[1, "index-13", false]], "right": [[2, "index-21", false]], "ring": [[1, "index-6", false]], "ring (algebraic structure)": [[1, "index-7", false], [7, "index-4", false]], "ring (tactic)": [[1, "index-6", false]], "rintro": [[2, "index-9", false]], "rw": [[1, "index-0", false], [1, "index-4", false]], "rw and rewrite": [[1, "index-0", false], [1, "index-4", false]], "rwa": [[3, "index-2", false]], "set operations": [[3, "index-0", false]], "show": [[1, "index-22", false]], "simp": [[2, "index-20", false], [3, "index-1", false]], "surjective function": [[2, "index-10", false]], "tactics": [[1, "index-0", false], [1, "index-11", false], [1, "index-12", false], [1, "index-13", false], [1, "index-15", false], [1, "index-17", false], [1, "index-18", false], [1, "index-20", false], [1, "index-22", false], [1, "index-23", false], [1, "index-29", false], [1, "index-3", false], [1, "index-4", false], [1, "index-5", false], [1, "index-6", false], [2, "index-0", false], [2, "index-11", false], [2, "index-12", false], [2, "index-13", false], [2, "index-14", false], [2, "index-15", false], [2, "index-16", false], [2, "index-17", false], [2, "index-18", false], [2, "index-19", false], [2, "index-2", false], [2, "index-20", false], [2, "index-21", false], [2, "index-23", false], [2, "index-24", false], [2, "index-25", false], [2, "index-26", false], [2, "index-4", false], [2, "index-6", false], [2, "index-8", false], [2, "index-9", false], [3, "index-1", false], [3, "index-2", false], [4, "index-0", false], [7, "index-2", false], [7, "index-3", false], [9, "index-3", false]], "this": [[2, "index-12", false]], "topological space": [[9, "index-4", false]], "topology": [[9, "index-0", false]], "trans": [[1, "index-29", false]], "use": [[2, "index-6", false]], "vector space": [[8, "index-0", false]], "vector subspace": [[8, "index-2", false]]}, "objects": {}, "objnames": {}, "objtypes": {}, "terms": {"": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "0": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "02463336": 6, "1": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "10": [2, 8, 9], "11": [8, 10], "12": [4, 8], "15": 2, "17": 4, "2": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "256": 9, "263": 6, "27": 4, "2c": 4, "3": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "37": 2, "4": [0, 1, 2, 4, 5, 7, 8, 9, 10], "4c": 4, "5": [1, 2, 5, 7, 8, 9, 10], "50": 6, "512": 9, "6": [2, 4, 5, 6, 7, 8, 9, 10], "64": 9, "7": [2, 4, 5, 7, 8], "70": 6, "73": 6, "8": [2, 4, 7, 8, 9], "9": 8, "A": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "And": [2, 4, 6, 9], "As": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "At": [0, 1, 2, 4, 5, 6, 8], "Be": [1, 3], "But": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "By": [1, 3, 5, 6, 7, 8], "For": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "If": [0, 1, 2, 3, 4, 5, 6, 8, 9], "In": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "It": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "Its": [5, 6], "Not": [1, 5, 9], "Of": [1, 2, 4, 6, 7, 8, 9, 10, 11], "On": [1, 2, 3, 5, 6, 8, 9, 11], "One": [1, 2, 3, 4, 5, 6, 7, 8, 9], "Or": [2, 3, 8], "Such": [0, 1, 2, 6], "That": [0, 4, 5, 6], "The": [0, 1, 4, 5, 6, 7, 8, 9, 10, 11, 13], "Their": [9, 10], "Then": [2, 3, 5, 6, 7, 8, 9, 11], "There": [0, 1, 2, 3, 4, 6, 7, 8, 9, 10, 11], "These": [0, 1, 3, 4, 5, 7, 10, 11], "To": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "With": [1, 3, 4, 6, 9], "_": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "_add_mod": 5, "_def": 4, "_eq": 5, "_in": 9, "_inst_1": 5, "_le": 5, "_n": 7, "_root_": [1, 3, 4], "a_0": 3, "a_1": 3, "a_2": 3, "a_def": 3, "a_of_b_of_c": 1, "ab": [0, 2, 5, 7], "abandon": 4, "abbrevi": [1, 2, 3, 5, 8], "abel": [1, 7], "abelian": [1, 5, 6, 8], "abgrpmodul": 6, "abil": 0, "abl": [0, 1, 2, 3, 4, 5, 6, 7, 8, 10], "abn": 2, "about": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 13], "abov": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "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, "absorb": 7, "absorb1": 1, "absorb2": 1, "absorpt": 1, "abstract": [1, 2, 5, 6, 7, 8, 9], "abstractli": 9, "absurd": [2, 4], "abus": 5, "ac": 5, "accept": [0, 1, 2, 8, 9], "access": [1, 3, 5, 6, 7, 8, 9, 11], "accessor": 5, "accid": 8, "accommod": [5, 7], "accompani": 5, "accord": [5, 8], "account": 8, "achiev": [5, 6, 9], "acknowledg": 0, "acpo": 2, "across": 6, "act": [1, 7, 8], "action": 8, "activ": 0, "actual": [2, 3, 4, 6, 7, 8, 9], "ad": [1, 2, 3, 4, 5, 6, 8, 9], "adapt": 5, "add": [2, 4, 5, 6, 7, 8, 9, 10], "add_assoc": [1, 4, 5, 6], "add_assoc\u2083": 6, "add_comm": [1, 4, 5, 6, 7], "add_def": 5, "add_im": 5, "add_l": 1, "add_le_add": [1, 2], "add_le_add_left": 1, "add_le_add_right": 1, "add_left_cancel": 1, "add_left_inj": 2, "add_lt_add_left": 1, "add_lt_add_of_le_of_lt": 1, "add_lt_add_of_lt_of_l": 1, "add_lt_add_right": 1, "add_mem": [7, 8], "add_mem_sup": 8, "add_mul": [1, 6], "add_mul_mod_self_left": 4, "add_neg_cancel_right": 1, "add_nonneg": [1, 5], "add_one_le_of_lt": 5, "add_po": 1, "add_pos_of_pos_of_nonneg": 1, "add_r": 5, "add_right_cancel": 1, "add_right_neg": 1, "add_smul": [6, 7, 8], "add_sub": 1, "add_sub_cancel": 4, "add_sub_cancel_right": 1, "add_vadd": 7, "add_x": 5, "add_zero": [1, 5, 6], "addact": 7, "addalt": 5, "addalt_comm": 5, "addalt_x": 5, "addcommgroup": [1, 7, 8], "addcommgroup\u2083": 6, "addcommmonoid": [7, 8], "addcommmonoid\u2083": 6, "addcommsemigroup\u2083": 6, "addequiv": 7, "addgroup": [1, 5, 7], "addgrouppoint": 5, "addgroup\u2081": 5, "addgroup\u2082": 5, "addgroup\u2083": 6, "addit": [1, 2, 4, 5, 6, 7, 8, 9, 10, 11], "addmonoid": [6, 7], "addmonoidhom": 7, "addmonoidhom\u2081": 6, "addmonoid\u2083": 6, "addmonoid\u2084": 6, "addsemigroup\u2083": 6, "addsubgroup": 7, "addzeroclass": 6, "adi": 5, "adjac": 8, "adject": 6, "adjug": 8, "adopt": 1, "advanc": 8, "advantag": [2, 3, 4, 5, 7, 10], "ae": [9, 11], "aestronglymeasur": 11, "aeval": [7, 8], "aeval_self_charpoli": 8, "aeval_x": 8, "affect": 6, "affin": 7, "aforement": 9, "after": [1, 2, 4, 6, 8, 9, 10], "again": [1, 2, 3, 4, 5, 6, 7, 8, 9], "against": 2, "agre": 3, "aid": 8, "aim": [4, 7], "aka": [8, 9], "aleb": 2, "alembert": 7, "alex": 0, "alexandru": 0, "algebra": [4, 6, 9, 10, 11, 13], "algebrahom": 6, "algebramap": [7, 8], "alghom": 7, "algorithm": 5, "alistair": 0, "all": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "allow": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "almost": [5, 6, 7, 8, 9, 11], "alon": 3, "along": [1, 4, 7, 9], "alpha": [2, 3], "alreadi": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "also": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "altern": [0, 1, 2, 3, 4, 5, 6, 9], "although": [0, 3, 4, 5, 6, 7, 8, 9], "alwai": [0, 1, 2, 3, 5, 6, 7, 8], "ambient": 7, "ambigu": [1, 5], "among": 4, "amount": [7, 8], "an": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "analog": [1, 2, 3, 4, 8, 9], "analogi": [2, 5, 9, 10], "analysi": [0, 5, 8, 10], "ancient": 4, "and_comm": 3, "anecdot": 6, "angl": 2, "ani": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "ann": 5, "annoi": [4, 6], "annot": [1, 2, 3, 4, 5, 6], "announc": 8, "anonym": [2, 3, 4, 5, 7], "anoth": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "answer": [0, 5, 9], "antisymm": 3, "antisymmetr": [1, 2], "anyhow": 2, "anyth": [2, 5, 9], "anywai": [4, 7], "apart": [5, 6], "api": 1, "appeal": [3, 6], "appear": [0, 1, 2, 5, 6, 7, 8, 9], "appli": [2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "applic": [1, 2, 5, 7, 11], "apply_fun": 7, "appreci": 4, "approach": [4, 5, 6, 9], "appropri": [1, 2, 3, 5, 6], "approxim": 1, "ar": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "arbitrari": [1, 2, 3, 4, 5, 7, 8], "arbitrarili": [2, 9], "archetyp": [5, 8], "argu": 6, "argument": [1, 2, 3, 4, 5, 6, 7, 8, 9], "aris": 2, "arithmet": 1, "aroot": 7, "aroots_def": 7, "around": [1, 3, 6, 7, 8, 9, 11], "arrai": 8, "arrang": 5, "arrow": [1, 2, 6, 9], "artifici": [5, 8], "ascii": 6, "ascript": [6, 7, 8], "asid": 3, "ask": [2, 4, 5, 6, 7, 9], "aspect": [0, 5, 7], "assembl": [8, 9], "assert": [2, 3, 6, 7], "assign": [2, 3, 5, 6, 7], "assist": [0, 2, 5], "associ": [0, 1, 2, 4, 5, 6, 7, 8, 9, 11], "assum": [0, 1, 2, 3, 4, 6, 7, 8, 9], "assumpt": [0, 1, 2, 3, 4, 5, 7, 8, 9, 10, 11], "assur": 5, "asymmetri": 2, "attach": [8, 9], "attain": 9, "attempt": 6, "attent": [1, 2, 4, 6, 7, 9], "attop": [9, 11], "attop_basi": 9, "attr": 6, "attract": 2, "attribut": 6, "auto": [1, 6], "autom": [0, 1, 5], "automat": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "aux": [1, 2, 4, 9], "aux_card_eq": 7, "auxiliari": [2, 9], "avail": [0, 1, 2, 4, 5, 6, 7, 8], "averag": 5, "avoid": [1, 2, 3, 4, 5, 6, 7, 10], "awai": [2, 5], "awkward": 8, "axiom": [1, 2, 3, 5, 6, 7, 8, 9, 11], "axiomat": [1, 2, 3, 5], "az": 8, "b": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "b_indep": 8, "b_span": 8, "baanen": 5, "back": [0, 1, 2, 5, 6, 7, 8, 9], "background": [0, 7], "backslash": [1, 3], "backward": [2, 9], "bad": [5, 6, 8, 9], "badinst": 6, "bair": [9, 10], "balanc": 1, "ball": [3, 10], "banach": [10, 11], "bar": [0, 1, 2, 8], "bare": [6, 8], "barrier": 6, "bartosz": 0, "base": [0, 2, 3, 4, 6, 7, 9, 10, 13], "basi": [5, 8, 9], "basic": [0, 2, 4, 5, 8, 9, 11, 13], "basisfun": 8, "basissingleon": 8, "baz": 1, "bbb": [2, 5], "bc": 5, "bci": 5, "bd": 5, "becaus": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "becom": [1, 4, 5, 6, 9], "been": [0, 1, 2, 4, 5, 6, 8, 10], "befor": [0, 1, 2, 3, 4, 5, 6, 7, 8], "begin": [1, 2, 3, 4, 5, 6], "begun": 9, "behav": [2, 3, 6, 8, 9], "behavior": [3, 6, 9], "behind": [3, 7], "being": [1, 3, 5, 7, 8, 9, 10], "belong": [5, 6, 9], "below": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "benefit": [7, 8], "benjamin": 0, "beq": 2, "berman": 0, "bernstein": 13, "besid": 6, "bespok": 5, "best": 0, "beta": [2, 3], "better": [3, 4, 5, 6, 9], "between": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "bewar": [6, 8], "bex": 3, "bex_def": 3, "beyond": [2, 6, 10], "bi": [1, 2, 5], "big": [0, 5, 7, 8, 9, 10], "bigcup_": 3, "bigger": [0, 3, 10], "bigoper": [4, 5, 7], "biject": [3, 5, 7, 8], "bijective_iff_injective_and_card": 7, "bilinear": 11, "binari": [1, 2, 4, 5, 6, 8], "binary_product": 8, "bind": [1, 3], "binder": 6, "bipartit": 5, "bit": [1, 2, 4, 6, 7, 8, 9], "black": [4, 6], "block": [1, 4, 7], "blur": 9, "bochner": 11, "bodi": 7, "boil": 6, "bold": 2, "bolt": 1, "book": [0, 2, 8, 9], "boolean": 1, "border": 9, "borelspac": 11, "boss": 9, "both": [1, 2, 3, 4, 5, 6, 7, 9, 10], "bother": [1, 3], "bottom": [6, 7, 8, 9], "bound": [1, 2, 3, 4, 5, 8, 9, 10, 11], "bounded": 10, "bounded_of_ex_finset": 4, "bourbaki": 9, "box": 4, "bpo": [2, 9], "bq": 5, "brace": [1, 8], "bracket": [1, 2, 5, 6, 7], "branch": [2, 3, 6], "break": 6, "breviti": [1, 5], "briefli": 7, "bring": [3, 4, 9], "broader": [4, 10], "broadest": 5, "brown": 0, "brows": [0, 1, 4, 7], "bryan": 0, "build": [0, 2, 4, 6, 7, 8, 9, 13], "builder": 3, "built": [0, 2, 6, 7, 8], "builtin": 6, "bulb": 5, "bulwi": 0, "bundl": [5, 6, 7, 8, 9, 10], "button": 0, "by_cas": [2, 3, 4], "by_contra": [2, 4], "c": [0, 1, 2, 4, 5, 6, 7, 8, 9, 10, 11], "c_mul": 7, "c_neg": 7, "cach": 0, "calc": [1, 2, 3, 5, 7, 9], "calcul": [0, 2, 4, 5, 13], "calculu": [9, 11, 13], "call": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "can": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "candid": 5, "cannot": [2, 3, 4, 5, 6, 7, 8, 9], "canon": [2, 3, 4, 5, 8], "cantor": 3, "cap": 3, "capabl": 5, "capit": 5, "captur": 8, "card": 7, "card_congr": 7, "card_dvd_of_l": 7, "card_eq_one_iff_exist": 7, "card_po": 7, "card_sigma": 7, "cardin": [3, 7, 8], "care": [1, 2, 3, 5, 8], "carneiro": 0, "carri": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "carrier": [1, 5, 6, 7, 8], "case": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "categor": 9, "categori": [5, 8, 9, 10], "cauchi": 9, "cauchyseq": 9, "cauchyseq_iff": 9, "cauchyseq_of_le_geometric_two": 9, "cauchyseq_tendsto_of_complet": 9, "caveat": 7, "caylei": [7, 8], "cayleyisomorph": 7, "cdist": 9, "cdot": 5, "center": [0, 9], "central": [0, 4], "centuri": 3, "ceq": 2, "certain": [2, 6, 9], "certifi": 0, "cha": 0, "chain": 5, "challeng": [0, 1, 2, 3, 5, 10], "chanc": 2, "chang": [0, 1, 2, 4, 5, 9, 11], "chapter": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "char": 0, "charact": [1, 3, 6], "character": [1, 3, 4, 8, 9, 10], "characterist": 8, "charpoli": 8, "chat": 0, "cheat": [0, 1], "check": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "checksynthord": 6, "chen": 0, "chestnut": 2, "chines": 7, "chineseiso": 7, "chinesemap": 7, "chinesemap_inj": 7, "chinesemap_mk": 7, "chinesemap_surj": 7, "choic": [1, 2, 3, 5, 8, 9], "choos": [0, 2, 3, 4, 5, 6, 7, 9], "choose_spec": 3, "chose": 6, "chosen": [2, 5], "circ": [3, 5], "circl": 7, "circleequ": 7, "claim": 9, "clarifi": 5, "clash": 1, "class": [1, 4, 5, 6, 7, 8, 9, 10, 11], "classic": [2, 3, 4, 7, 8], "claus": 6, "clean": [2, 9], "clear": [1, 2, 4, 5, 6], "clearer": [1, 3, 5], "clearli": 9, "clever": 1, "click": [0, 1, 3, 4, 5, 6], "clock": 0, "clontz": 0, "close": [1, 2, 3, 6, 7, 8, 10, 11], "closed_nhds_basi": 9, "closedbal": 9, "closer": [2, 9], "closur": [7, 8, 9], "closure_iscycl": 7, "cloud": 0, "clue": 7, "clunki": 9, "cluster": 9, "clusterpt": 9, "cmd": [1, 2], "co": [2, 7], "cocki": 1, "code": [0, 1, 2, 3, 5, 6, 8], "codomain": [2, 4, 9], "coe": 6, "coe_inject": 6, "coe_natabs_norm": 5, "coeff": 7, "coeffici": [5, 7, 8], "coefun": 6, "coelinearmap": 8, "coerc": [6, 7, 8], "coercion": [5, 6, 7, 8, 9, 10], "coincid": [4, 5, 9], "coinduc": 9, "coinduced_compos": 9, "coinduced_le_iff_le_induc": 9, "col": 8, "collari": 0, "collect": [1, 2, 3, 5, 8, 9, 11], "collis": 6, "colon": [2, 8], "column": 8, "comap": [7, 8, 9], "comap_bot": 8, "comap_comap": 9, "comap_map_eq": 8, "comapmkqreliso": 8, "combin": [1, 2, 5, 6, 7, 8, 9], "come": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "comfort": 0, "comm": 7, "comma": [1, 8], "command": [0, 1, 2, 3, 4, 5, 6, 7, 8], "commelin": 0, "comment": [0, 4], "commgroup": 1, "commgroup\u2083": 6, "commmonoid": 6, "commmonoid\u2083": 6, "common": [1, 2, 3, 4, 5, 7, 8, 9], "commonli": [4, 5], "commr": [1, 2, 5, 7], "commsemigroup\u2083": 6, "commsemir": [7, 8], "commun": [0, 4], "commut": [1, 2, 3, 4, 5, 6, 7, 8, 10], "comp": [7, 8, 9], "comp_id": 8, "compact": 11, "compactspac": 9, "compani": 2, "companion": [0, 1], "compar": [0, 5, 6, 8, 9], "comparison": 6, "compat": [1, 7, 9], "compat_mymap": 7, "compl": 11, "complain": 1, "complement": [3, 8, 9, 11], "complementari": 0, "complet": [0, 1, 2, 3, 4, 6, 7, 10], "completespac": [9, 10, 11], "complex": [0, 1, 2, 4, 5, 7, 8, 10, 11], "complic": [1, 2, 6, 7, 8], "compon": [2, 3, 5, 8, 9, 11], "compos": [3, 5, 7, 9], "composit": [2, 3, 5, 6, 7, 8, 9], "compound": [1, 2, 9], "compress": [0, 1, 9], "comput": [0, 2, 3, 4, 5, 7, 8, 10, 11], "computation": [4, 8], "concentr": 3, "concept": [5, 7, 8, 9, 10], "conceptu": [3, 7], "concis": [1, 5, 7], "conclud": [2, 10], "conclus": [1, 2, 4], "concret": [1, 2, 4, 5, 6, 8, 9], "condens": 3, "condit": [3, 4, 6, 7, 8, 9, 10], "confid": 3, "configur": 5, "confirm": [1, 2, 3, 4], "confus": [3, 4, 6, 7, 9], "congr": 2, "congratul": [1, 2, 4], "congruent": 4, "conj": 5, "conj_im": 5, "conj_r": 5, "conjug": [5, 7], "conjugate_on": 7, "conjunct": [1, 6, 13], "connect": [1, 3, 5, 8, 9], "consequ": 7, "consid": [1, 2, 3, 4, 5, 6, 7, 9, 10, 11], "consider": 8, "consist": [1, 3, 5, 6, 7, 8, 9, 10], "constant": [1, 2, 7, 11], "constantli": 7, "constitut": 1, "constr": 8, "constr_basi": 8, "constraint": [5, 9], "construct": [0, 2, 3, 4, 5, 6, 7, 8, 9], "constructor": [1, 2, 3, 4, 5, 6], "consult": 5, "cont": 10, "contain": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "contdiff": 10, "contdiff_iff_continuous_differenti": 10, "contdiffat": 10, "contend": 4, "content": [0, 1, 2, 4, 9], "context": [1, 2, 4, 5, 6, 7, 8, 9, 10, 11], "contextu": 5, "continu": [0, 1, 4, 5, 6, 8, 11], "continuous_def": 9, "continuous_dist": 9, "continuous_fst": 9, "continuous_id": [6, 9], "continuous_iff": 9, "continuous_iff_coinduced_l": 9, "continuous_linear_map": 10, "continuous_pow": 9, "continuous_snd": 9, "continuousat": [9, 11], "continuousat_extend": 9, "continuousat_iff": 9, "continuouslinearmap": 10, "continuouson": [9, 10], "continuum": 2, "contort": 7, "contract": 2, "contradict": [2, 3, 4], "contradictori": 2, "contrapos": [2, 3, 4], "contrari": 2, "contrast": [2, 3, 5, 6, 9], "contravari": 9, "contribut": [0, 3], "contributor": 8, "control": 2, "conveni": [1, 2, 3, 5, 6, 7, 8, 9], "convent": [1, 5, 7, 11], "convention": 9, "converg": [11, 13], "convergesto": 2, "convergesto_add": 2, "convergesto_const": 2, "convergesto_mul": 2, "convergesto_mul_const": 2, "convergesto_uniqu": 2, "convers": [0, 2, 4, 7, 8, 9], "convert": [2, 4, 7, 8], "convinc": 5, "convolut": 11, "coordin": [7, 8], "copi": [0, 3, 4, 6, 7, 8, 9], "coprim": [4, 7], "coprime_mn": 4, "coprod": 8, "coprod_inl": 8, "coprod_inr": 8, "coproduct": 8, "core": [0, 4, 5], "corner": 7, "corollari": 7, "correct": [0, 1, 7], "correctli": 3, "correspond": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "could": [0, 1, 2, 4, 5, 6, 7, 8, 9], "count": 7, "count_factors_mul_of_po": 4, "countabl": 11, "counter": 8, "counterexampl": [2, 10], "counterpart": 5, "coupl": [1, 2, 6, 8, 9], "cours": [1, 2, 4, 6, 7, 8, 9, 10, 11], "covari": 9, "cover": [0, 1, 3, 6, 7, 8, 9, 10], "cramer": 8, "creat": [0, 1, 4, 6], "creation": 7, "creativ": 5, "criterion": 9, "crucial": [7, 8, 9], "crude": 4, "cryptic": 2, "ct": 2, "ctrl": [0, 1, 2, 4, 5], "cube": 7, "cue": 5, "cup": 3, "curiou": [1, 6], "curli": [1, 2, 8], "current": [1, 2, 5, 6], "curri": 1, "cursor": [0, 1, 2], "curv": 0, "custom": 5, "cut": 4, "cycl": 7, "cyclic": 7, "czubin": 0, "d": [1, 2, 4, 5, 7, 8, 10], "dai": 3, "danger": [4, 5], "data": [1, 2, 4, 5, 6, 8, 9], "databas": [3, 4, 6, 9], "datatyp": 4, "de": 0, "deal": [1, 2, 3, 4, 5, 8, 9], "dealt": 2, "decid": [4, 7, 8, 9], "decidableeq": [4, 8], "decidablepr": 4, "decis": [4, 7], "declar": [0, 1, 4, 5, 6, 7, 8], "decompos": [0, 3], "decreas": [1, 5], "dedekind": 3, "deduc": [6, 7, 9], "def": [0, 2, 3, 4, 5, 6, 7, 8, 9], "default": [1, 2, 3, 4, 5, 6, 7, 10], "defect": [2, 6, 9], "defin": [1, 2, 3, 4, 6, 7, 8, 9, 10, 11, 13], "definit": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "definition": [1, 4, 5, 6, 9], "degre": 7, "degree_mul": 7, "delet": [1, 2, 3], "delic": 3, "delimit": 1, "demonstr": [6, 9], "deni": 0, "denomin": [2, 4, 5], "denot": [1, 3, 4, 6, 7, 8, 9], "dens": 9, "denseinduc": 9, "densiti": 9, "depend": [0, 2, 3, 4, 5, 6, 7, 8, 9], "deriv": [1, 2, 4, 7, 10, 11], "deriv_add": 10, "deriv_eq_zero": 10, "deriv_zero_of_not_differentiableat": 10, "descend": [6, 7], "describ": [0, 1, 2, 3, 4, 5, 6, 8, 9], "descript": [0, 1, 2, 4, 9], "deserv": 4, "design": [0, 1, 2, 3, 5, 7, 8, 9], "desir": [1, 3, 6, 7, 9], "despit": 8, "destruct": 2, "destructur": 6, "det": [8, 11], "det_mul": 8, "det_on": 8, "detail": [1, 2, 3, 4, 5, 6, 7], "detect": 2, "determin": [1, 5, 7, 8, 9], "develop": [0, 1, 4, 7, 11], "devic": 6, "devot": 9, "dfun": 6, "dfunlik": 6, "di": [2, 5], "dia": 6, "dia_assoc": 6, "dia_inv": 6, "dia_on": 6, "diagram": 3, "diamond": 6, "diaoneclass\u2081": 6, "dia\u2081": 6, "dictionari": 1, "did": [0, 2, 6, 9], "dif_neg": 3, "dif_po": 3, "diff_eq": 3, "differ": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "differenti": [11, 13], "differentiableat": 10, "differentiableon": 10, "difficult": [2, 6], "digress": 9, "dimens": 13, "dimension": [8, 10, 11], "direct": [1, 2, 3, 6, 7, 9, 10], "directli": [1, 2, 4, 5, 6, 8, 9], "directsum": 8, "discret": 5, "discuss": [1, 2, 4, 5, 6, 7, 8, 9, 10], "dishwash": 0, "disjoint": [3, 7, 11], "disjunct": [1, 3, 13], "dispens": 4, "displai": [0, 1, 2, 6], "dispos": 2, "dist": [1, 9], "dist_comm": [1, 9], "dist_eq_zero": 9, "dist_le_range_sum_dist": 9, "dist_nonneg": [1, 9], "dist_self": 1, "dist_triangl": [1, 9], "distanc": [1, 2, 9, 10], "distinct": [0, 2, 3, 4, 5, 8, 9], "distinguish": [0, 5, 6, 7, 9, 10], "distract": 6, "distriblattic": 1, "distribut": [1, 4, 5, 6], "div": 5, "div_def": 5, "div_dvd_of_dvd": 4, "div_eq_mul_inv": 5, "div_eq_of_eq_mul_right": 4, "div_lt_self": 4, "div_nonneg": 5, "div_po": 2, "divab": 2, "divac": 2, "divbc": 2, "dive": 0, "divid": [1, 2, 4, 5, 7], "divis": [1, 2, 4, 5, 6, 8], "divisor": [1, 2, 4, 5, 7], "do": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "doc": 0, "document": [0, 1, 3, 4, 6], "doe": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "doesn": [1, 2, 7, 8, 9], "domain": [1, 2, 3, 4, 5, 7, 9], "domin": 11, "don": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "done": [0, 2, 3, 4, 6, 7, 8, 9], "doorn": 0, "dot": [1, 7, 8, 9], "doubl": [2, 3], "doubli": 7, "doubt": 0, "down": [0, 3, 4, 6, 9], "downsid": [7, 8], "dozen": 3, "draw": [1, 5, 6], "drop": 2, "dsimp": [2, 3, 5, 7, 8], "dual": [5, 9], "dualli": 9, "duca": 0, "due": [1, 6], "duplic": 6, "dvd": 1, "dvd_add_iff_left": 4, "dvd_antisymm": 1, "dvd_fac": 4, "dvd_factori": 4, "dvd_gcd": 4, "dvd_gcd_iff": 2, "dvd_iff_exists_eq_mul_left": 4, "dvd_mul": 4, "dvd_mul_left": 1, "dvd_mul_of_dvd_left": 1, "dvd_mul_of_dvd_right": 4, "dvd_mul_right": [2, 4], "dvd_of_dvd_pow": 4, "dvd_prod_of_mem": 4, "dvd_sub": 4, "dvd_tran": 1, "dwell": 3, "e": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "each": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "earli": 8, "earlier": [1, 7, 8], "easi": [0, 4, 5, 6, 7, 8, 9], "easier": [0, 1, 3, 4, 6, 9], "easiest": [2, 4], "easili": [1, 4, 5, 6, 7, 8], "ebner": 0, "eccentr": 8, "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, 9], "effici": [5, 7, 8, 9], "effort": [1, 4], "eg": 2, "eigenspac": 8, "eigenvalu": 8, "eigenvector": 8, "eight": 9, "either": [1, 2, 3, 5, 6, 9], "elabor": [8, 9], "ele1": 2, "eleg": 5, "element": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "elementari": [0, 3, 5, 7, 8, 9, 13], "elim": 2, "elim_finite_subcov": 9, "elimin": 1, "els": [2, 3, 4, 8], "em": [2, 3], "emanuel": 0, "emb": 5, "embark": 6, "embed": 7, "embodi": 7, "emetricspac": 9, "emod_lt": 5, "emod_lt_of_po": 5, "emod_nonneg": 5, "emphas": [6, 7], "emphasi": [0, 6], "empti": [3, 4, 5, 7, 9, 11], "enabl": [2, 3, 4, 5], "enat": 4, "encapsul": [3, 5, 10], "encod": [7, 11], "encount": [4, 6], "encourag": [0, 1, 2, 3, 4, 5], "end": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "endomorph": [7, 13], "endow": [6, 7, 8], "enforc": 7, "engin": 4, "enjoi": [2, 3, 4, 9], "ennreal": 11, "enough": [0, 1, 2, 3, 4, 6, 7, 8, 9], "ensur": [6, 7, 8, 9], "enter": [0, 1, 2, 3, 7, 9], "enthusiast": 0, "entir": [1, 3, 5, 9, 10], "entourag": 9, "entri": [0, 5, 7, 8], "enumer": [1, 2], "epo": 2, "eq": 5, "eq1": 4, "eq2": 4, "eq_bot": 8, "eq_bot_iff": 8, "eq_bot_iff_card": 7, "eq_bot_iff_foral": 7, "eq_empty_or_nonempti": 9, "eq_neg_of_add_eq_zero": 1, "eq_of_dvd_of_prim": 4, "eq_of_mul_eq_mul_right": 7, "eq_one_or_self_of_dvd": 4, "eq_top_iff": 7, "eq_two_or_odd": 3, "eq_univ": 3, "eq_univ_of_foral": 3, "eq_zero_iff_mem": 7, "eq_zero_or_eq_zero_of_mul_eq_zero": 2, "equal": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "equat": [1, 2, 3, 4, 5], "equilater": 5, "equip": [1, 3, 5, 6, 7, 9, 10, 11], "equiv": [5, 7, 8], "equival": [1, 2, 3, 4, 5, 7, 8, 9, 10, 11], "eras": 4, "eric": 0, "error": [1, 2, 3, 6], "erw": 2, "especi": [1, 2, 5, 6, 7, 8, 9], "essenti": [2, 3, 5, 7, 9], "establish": [0, 1, 2, 3, 4, 5], "eta": 5, "etc": [8, 9], "euclidean": 5, "euclideandomain": 5, "eval": [0, 7, 8], "evalu": [7, 8], "eval\u2082": 7, "even": [0, 1, 2, 3, 4, 5, 6, 8, 9, 10, 11], "even_of_even_sqr": 4, "eventu": [2, 3, 9], "eventually_eventually_nhd": 9, "eventually_left_invers": 10, "eventually_right_invers": 10, "eventuallyeq": 9, "ever": [0, 9], "everi": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "everyth": [1, 2, 6, 9], "everywher": [2, 3, 6, 8, 9, 11], "evid": 5, "evolv": 1, "ex": [0, 2], "ex_finset_of_bound": 4, "exact": [1, 2, 3, 4, 5, 7, 8, 9], "exactli": [1, 2, 3, 5, 6, 7, 9], "exampl": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "except": [1, 2, 5, 7], "exclam": 9, "exclud": [2, 4], "exercis": [0, 1, 2, 3, 5, 6, 7, 8, 9, 10], "exfalso": 2, "exhibit": [2, 9], "exist": [1, 2, 3, 6, 7, 8, 9], "existenti": [3, 7, 13], "exists_abs_le_of_convergesto": 2, "exists_deriv_eq_slop": 10, "exists_deriv_eq_zero": 10, "exists_haseigenvector": 8, "exists_infinite_prim": 3, "exists_ismaxon": 9, "exists_isminon": 9, "exists_one_lt_norm": 10, "exists_prime_and_dvd": 3, "exists_prime_factor": 4, "exists_prime_factor_mod_4_eq_3": 4, "exists_subgroup_card_pow_prim": 7, "exot": [7, 9], "exp": [1, 3], "exp_le_exp": 1, "exp_log": 3, "exp_lt_exp": 1, "exp_po": [1, 3], "expand": [1, 2, 3, 4, 5, 6, 8], "expect": [1, 2, 3, 4, 5, 6, 7, 8, 9], "experi": [0, 1, 9], "explain": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "explan": [0, 7, 8, 9], "explicit": [1, 2, 5, 6, 8, 9], "explicitli": [1, 2, 3, 5, 6, 7, 8, 9, 10], "explor": [4, 8, 9], "expon": 1, "exponenti": 4, "export": 6, "expos": [2, 9], "express": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "ext": [2, 3, 4, 5, 6, 7, 8], "ext_iff": 5, "extend": [1, 3, 4, 5, 6, 9, 11], "extens": [0, 1, 6, 9, 10], "extension": [3, 5], "extern": 8, "extra": [1, 2, 3, 5, 6, 7, 9], "extract": [2, 9], "extrem": [0, 6, 9], "f": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "f_": 9, "f_cont": 9, "f_le": 9, "f_ne": 9, "fac": 4, "fac_po": 4, "face": [5, 6, 9], "facilit": [2, 8, 9], "fact": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "factor": [4, 5, 7, 8], "factori": 4, "factorial_po": 4, "factorization_mul": 4, "factorization_pow": 4, "fail": [1, 2, 4, 5, 6, 8, 9, 11], "failur": 6, "fairli": 2, "fals": [1, 2, 3, 4, 6], "falso": 2, "famili": [7, 8, 9, 10], "familiar": [0, 1, 4, 5, 8, 9, 10], "famou": [3, 7], "far": [2, 3, 6, 8, 9], "favor": [1, 5], "fderiv": 10, "fear": 6, "feat": 4, "featur": [0, 2, 4, 7], "feed": 7, "feedback": 0, "feel": [0, 1, 2, 6, 8, 9], "fermatlasttheorem": 0, "fetch": 0, "few": [1, 2, 3, 4, 9], "field": [0, 1, 5, 6, 7, 8, 10], "field_simp": [2, 5], "figur": [0, 1, 2, 5, 8], "file": [0, 1, 4, 5, 6, 7, 9], "fill": [2, 3, 4, 5], "filter": [4, 10, 11, 13], "filter_upward": 9, "filteri": 9, "fin": [5, 7, 8, 11], "fin_cas": 8, "final": [1, 2, 3, 5, 7, 8, 9, 11], "finaliso": 7, "find": [0, 1, 2, 4, 5, 6, 8, 9], "fine": 8, "finicki": 1, "finish": [1, 2, 3, 4, 7], "finit": [1, 3, 4, 5, 7, 8, 9, 10, 11], "finitedimension": [8, 10, 11], "finrank": 8, "finrank_eq_rank": 8, "finrank_fin_fun": 8, "finrank_l": 8, "finrank_pos_iff": 8, "finrank_real_complex": 8, "finrank_self": 8, "finrank_sup_add_finrank_inf_eq": 8, "finset": [4, 5, 7, 8, 9], "finsupp": 8, "fintyp": [7, 8, 9], "fintypebasisindex": 8, "first": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "firstcountabletopologi": 9, "fix": [4, 6, 7, 8, 9], "fixm": 5, "flag": [2, 3], "flavor": 8, "flexibl": 9, "flori": 0, "fn_ub_add": 2, "fneven": 2, "fnhaslb": 2, "fnhasub": 2, "fnlb": 2, "fnodd": 2, "fnub": 2, "fnub_add": 2, "fnuba": 2, "focu": [0, 1, 7, 8, 9, 11], "focus": 9, "folder": 0, "follow": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "font": 7, "foo": [1, 5], "forc": [1, 2, 3, 7, 8], "foreshadow": 1, "forewarn": 0, "forget": 6, "form": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "formal": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "format": 1, "former": 5, "formul": [4, 7, 9], "formula": [7, 11], "forth": 5, "fortiori": 9, "fortun": 3, "forward": [1, 2, 5, 7, 9], "found": [1, 5, 7, 8, 10], "foundat": [2, 3, 4, 5, 7, 8], "four": [2, 5], "fourth": [1, 2], "frac": 5, "fraction": 4, "fraenkel": 2, "framework": [0, 8], "frasa": 0, "free": [0, 1, 7, 8, 9], "freegroup": 7, "freeli": 4, "frequent": 9, "friend": [2, 5], "friendli": 7, "from": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "front": 2, "frustrat": [0, 6], "fr\u00e9chet": 10, "fst": [5, 8, 9], "fubini": 11, "full": [1, 2, 3, 4, 5, 6, 7, 8, 9], "fulli": [3, 7, 8, 9], "fun": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "function": [1, 2, 4, 5, 6, 7, 8, 10, 11, 13], "functori": 9, "fundament": [0, 4, 5, 6, 11], "funni": 9, "further": [1, 9], "furthermor": 7, "g": [1, 2, 3, 5, 6, 7, 8, 9, 10, 11], "g_": 9, "g_1": 5, "g_2": 5, "g_3": 5, "gabriel": 0, "gadget": [2, 9], "gain": 6, "galoi": [3, 5, 8, 9], "galoisinsert": 8, "game": [0, 6], "gauss": 7, "gaussian": [2, 7, 13], "gaussianint": 5, "gaussint": 5, "gave": [7, 9], "gcd": [1, 2, 4], "gcd_zero_left": 1, "gcd_zero_right": 1, "gcongr": 5, "ge": [0, 2, 5], "gener": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "genuin": 2, "geometr": 9, "geometri": 7, "get": [1, 2, 3, 4, 6, 7, 8, 9, 10, 13], "gi": 8, "gin": 0, "giovanni": 0, "git": 0, "github": [0, 1], "gitpod": 0, "give": [1, 2, 3, 4, 6, 7, 8, 9, 11], "given": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "glb": 1, "global": [7, 9], "go": [0, 1, 2, 3, 4, 6, 8, 9], "goal": [0, 1, 2, 3, 4, 5, 8, 9], "goe": [3, 4, 5, 6, 9], "good": [1, 2, 3, 4, 5, 6, 7, 8, 9], "gorbachev": 0, "got": 6, "govern": [1, 5], "gradual": [6, 9], "graph": [5, 8], "grate": [0, 5], "great": [1, 5], "greater": [0, 1, 2, 3, 4, 9], "greatest": [1, 5, 9], "greef": 0, "greek": [1, 4], "group": [0, 1, 2, 3, 4, 5, 6, 8, 9, 10, 13], "groupact": 7, "groupcat": 5, "groupequivquotientprodsubgroup": 7, "grouptheori": 5, "group\u2081": [5, 6], "group\u2081cat": 5, "group\u2082": 5, "group\u2083": 6, "grow": [0, 6, 7], "grp": 5, "guai": 0, "guarante": [0, 3, 5, 8], "guess": [1, 2, 3, 4, 5, 8], "guilherm": 0, "gya": 3, "g\u2080": 7, "g\u2081": 7, "g\u2082": 7, "h": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "h0": 4, "h1": [1, 2, 3, 4, 5], "h2": [1, 2, 3, 5], "h3": 1, "h_def": 3, "h_inj": 11, "ha": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "hab": 10, "habit": [6, 8], "hac": 6, "hack": 3, "had": [1, 6, 8], "hal": 6, "half": [3, 7], "hamilton": 8, "hand": [1, 2, 3, 4, 5, 6, 8, 9], "handi": 4, "handl": [1, 3, 4, 6, 7], "hanson": 0, "happen": [1, 6, 9], "happi": 0, "hard": [0, 1, 3, 5, 6, 7], "harder": [2, 5, 8], "harm": 3, "hasbasi": 9, "hasderivat": [10, 11], "hasderivat_sin": 10, "haseigenvalu": 8, "haseigenvalue_iff_isroot": 8, "haseigenvalue_of_haseigenvector": 8, "haseigenvector": 8, "hasfderivat": 10, "hasfderivatfilt": 10, "hasfderivatfilter_iff_islittleo": 10, "hasfderivwithinat": [10, 11], "hasinvgroup\u2082": 5, "haskel": 1, "hasmulgroup\u2082": 5, "hasonegroup\u2082": 5, "hasquoti": 6, "hasstrictfderivat": 10, "hausdorff": 9, "have": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "haven": [0, 2, 6, 9], "hb": [2, 9], "hba": 6, "hball": 9, "hbound": 11, "hc": 10, "hd": 9, "hdi": 11, "hdvd": 7, "he": 7, "headach": 4, "headi": 5, "heart": [4, 7], "heather": 5, "heaven": 5, "heavier": 6, "heavili": 9, "hello": 0, "help": [0, 1, 2, 3, 4, 5, 6, 8, 9], "helper": 1, "henc": [0, 2, 3, 4, 5, 6, 8, 9, 10], "here": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "hesit": 4, "hf": [3, 7, 9, 10, 11], "hfa": 2, "hfc": 10, "hff": 10, "hfi": 10, "hfx": 9, "hg": [3, 9, 10, 11], "hgb": 2, "hi": 7, "hidden": 2, "hide": [6, 7, 9], "hierarchi": [5, 7, 8, 13], "high": [2, 7], "higher": 6, "highlight": [0, 2], "hij": 8, "hint": [0, 1, 2, 11], "histor": [1, 7], "hit": [0, 1], "hk": [0, 10], "hle": 9, "hlim": 11, "hm": 10, "hmea": 11, "hmn": 0, "hmp": 10, "hn": [3, 4, 9, 10], "hna": 2, "hnb": 2, "hne": 9, "ho": 9, "hold": [1, 2, 3, 4, 5, 7, 8, 9, 11], "home": [4, 5], "homomorph": 7, "hood": [3, 5, 8], "hope": [0, 1, 8], "hopelessli": 6, "hoskinson": 0, "hover": [0, 1, 2, 3, 4, 5], "how": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "howev": [1, 2, 5, 6, 7, 8, 9, 10], "hp": [7, 9], "hpo": 9, "hq": [7, 9], "hr": 9, "hst": 7, "hsu": 9, "ht": 2, "html": 0, "http": 6, "hu": [9, 10], "huge": 6, "huisinga": 0, "hum": 9, "human": 1, "hunt": [6, 8], "hunter": 0, "huo": 9, "hurdl": 6, "hurt": 2, "hux": 9, "hv": 8, "hw": 6, "hx": [2, 3, 5, 6, 7, 8, 10], "hxeq": 3, "hy": [5, 6, 7, 8], "hyp": 1, "hypothes": [1, 2, 3, 4, 5], "hypothesi": [0, 1, 2, 3, 4], "hz": [5, 6], "h\u03b5": 10, "h\u03c6": 8, "h\u2080": [1, 2, 3, 4, 9], "h\u2081": [1, 2, 3, 4], "h\u2082": [1, 3, 4], "h\u2083": [1, 3], "i": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "icc": [9, 10], "ici": 9, "id": [4, 6, 8, 9, 10], "id_comp": 8, "idea": [1, 2, 3, 5, 6, 8, 9], "ideal": 8, "ident": [3, 4, 5, 6, 7, 8, 9, 13], "identif": 8, "identifi": [1, 2, 4, 8], "if_neg": 3, "if_po": 3, "iff": [1, 3, 7, 8, 9, 10, 11, 13], "ignor": [0, 5, 7, 8, 9], "ih": 4, "iinf_insert": 7, "iinter": 11, "il": 4, "illustr": [1, 2, 3, 4, 5, 7], "im": 5, "imag": [3, 4, 6, 7, 8, 9], "image_subset_iff": 3, "imagin": 1, "imaginari": 5, "immedi": [2, 3, 5, 6, 8], "implement": [2, 5, 6, 7, 8, 10], "impli": [1, 2, 3, 4, 5, 8, 9], "implic": [1, 8, 9, 13], "implicit": [1, 2, 5, 6, 7, 8, 9, 10], "implicitli": [1, 2], "import": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "importantli": [6, 7, 8], "imposs": 1, "impress": 0, "improv": [3, 4], "incl": 9, "includ": [0, 1, 2, 3, 4, 6, 7, 8, 9, 10], "inclus": [1, 3, 7, 8, 9], "inconsist": [1, 8], "inconveni": 10, "incorpor": 6, "increas": 1, "increment": [0, 1], "inde": [1, 5, 6, 7, 8, 9, 10], "indefinit": 4, "indent": 1, "independ": [2, 3, 5, 8], "indetermin": 7, "index": [3, 6, 7, 8, 9], "index_eq_card": 7, "index_mul_card": 7, "indic": [1, 2, 3, 5, 6], "indirect": 6, "indirectli": 1, "individu": 1, "induc": 9, "induced_compos": 9, "induct": [7, 8, 9, 13], "induction_on": 4, "inequ": [1, 2, 6, 9], "inf": [1, 6, 9], "inf_assoc": 1, "inf_bot_of_coprim": 7, "inf_comm": [1, 7], "inf_eq_bot": 8, "inf_le_left": [1, 9], "inf_le_right": 1, "inf_sup_left": 1, "inf_sup_right": 1, "inf_sup_self": 1, "infer": [1, 2, 3, 5, 6, 7, 8], "infer_inst": [10, 11], "inferenti": 0, "inferinst": [7, 8], "inferr": 6, "infimum": [1, 6, 7, 8, 9, 11], "infin": [4, 9, 11], "infinit": [3, 8, 9, 13], "infix": [1, 6], "infixl": 6, "infixr": 6, "inform": [0, 1, 2, 3, 5, 6, 8, 9], "infoview": [1, 6], "infrastructur": 0, "infti": 10, "ingredi": [3, 5, 9, 10], "inhabit": [3, 5, 9], "inherit": [5, 6, 7, 8], "inherit_doc": 6, "inj": 4, "inject": [2, 3, 4, 6, 7, 8, 9], "injective_lift_iff": 7, "injf": [2, 3], "injg": 2, "injon": [3, 11], "inl": [2, 3, 8], "inner": 3, "input": [1, 3, 8, 9], "inr": [2, 3, 8], "inria": 6, "inscrut": [2, 3], "insert": [0, 2, 4, 5, 7, 8, 9, 10], "insid": [0, 1, 2, 3, 7], "insight": 2, "insist": [1, 6], "inspect": 1, "inspir": 2, "inst": 6, "inst_1": 6, "instal": [0, 6], "instanc": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "instanti": [2, 5, 6, 9], "instcommr": 5, "instead": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "instruct": [0, 1, 2, 9], "int": [5, 6, 7], "intact": 0, "integ": [1, 2, 4, 6, 7, 13], "integr": [2, 10, 13], "integral_add": 11, "integral_eq_sub_of_hasderivat": 11, "integral_hasstrictderivat_right": 11, "integral_id": 11, "integral_image_eq_integral_abs_det_fderiv_smul": 11, "integral_one_div": 11, "integral_prod": 11, "intend": [0, 1, 2, 5], "inter_def": 3, "inter_set": 9, "interact": [0, 5, 6, 7, 8, 11], "interchang": 1, "interconnect": 5, "interest": [1, 2, 3, 5, 6, 8, 9], "interestingli": [5, 7, 10], "interfac": 5, "interior": [5, 10], "interior_iinter_subset": 10, "interior_subset": 10, "intermedi": [1, 6, 8, 9], "intern": [2, 5, 7], "interpret": [0, 1, 4, 5, 7, 8, 9], "intersect": [1, 3, 5, 6, 7, 8, 9, 11], "interv": [4, 9, 11], "interval_cas": 4, "intervalintegr": 11, "intro": [0, 1, 2, 3, 4, 5, 6, 7, 9], "introduc": [0, 1, 2, 3, 4, 8, 9, 11], "introduct": [1, 2, 7, 9, 13], "introductori": 10, "intuit": [3, 9], "inv": [5, 6], "inv_def": 8, "inv_dia": 6, "inv_eq_of_dia": 6, "inv_eq_of_mul": 6, "inv_mem": 7, "inv_mul": 6, "inv_mul_cancel": [1, 5], "inv_mul_of_invert": 8, "invari": 11, "invers": [1, 3, 5, 6, 7, 8, 10, 11], "inverse_spec": 3, "invert": [6, 7, 8], "invertibleofisunitdet": 8, "invest": 5, "invfun": [3, 5, 8], "invfun_eq": 3, "invisibli": [5, 6], "invok": [0, 1, 9], "involv": [1, 2, 4, 5, 6, 7, 8, 9], "inv\u2081": 6, "inward": 2, "ioo": [9, 10], "ipo": 4, "irrat": 13, "irration": 4, "irreduc": [4, 5], "irreducible_iff_prim": 5, "irreflex": 2, "is_addit": 5, "isaddhaarmeasur": 11, "isaiah": 0, "isalgclos": 7, "isbigo_iff_isbigowith": 10, "isbigowith": 10, "isbigowith_iff": 10, "isclos": [9, 10], "isclosed_l": [9, 10], "iscompact": 9, "iscompact_icc": 9, "iscompact_univ": 9, "iscompl": 8, "iscoprim": [7, 8], "iscoprime_iff_add": 7, "iscoprime_iff_codisjoint": 7, "iscoprime_iff_exist": 7, "iscoprime_iff_sup_eq": 7, "iscoprime_inf": 7, "iscycl": 7, "isdomain": [2, 7], "iseqv": 6, "isintern": 8, "isinternal_submodule_iff_independent_and_isup_eq_top": 8, "islinear": 5, "islittleo_iff_forall_isbigowith": 10, "islocalmin": 10, "ismonoidhom\u2081": 6, "ismonoidhom\u2082": 6, "isn": [0, 2, 3, 4, 6], "isomorph": [5, 7, 8, 10], "isopen": 9, "isopen_compl_iff": 9, "isopen_empti": 9, "isopen_iff": 9, "isopen_iinter_of_finit": 9, "isopen_iunion": 9, "isopen_univ": 9, "iso\u2081": 7, "iso\u2082": 7, "isroot": [7, 8], "isroot_of_haseigenvalu": 8, "issu": [1, 4, 5, 6, 8, 9], "issubgroup": 7, "issubmodul": 8, "isunit": 7, "item": 9, "iter": 10, "iteratedfderiv": 10, "its": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "itself": [0, 2, 3, 5, 6, 7, 8, 9, 10], "iunion": 11, "j": [3, 7, 8], "jimmi": 0, "job": 1, "johan": 0, "john": 0, "join": [0, 1, 5], "jone": 0, "journei": 9, "juggl": 6, "julian": 0, "jump": [1, 4, 5, 9], "just": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "justif": [1, 2], "justifi": [0, 1, 2, 9], "k": [0, 2, 4, 5, 7, 8, 9, 10], "keep": [1, 3, 5, 6, 7], "kei": [1, 4, 5, 7, 8, 9], "keith": 0, "ker": [7, 8], "ker_eq_bot": 8, "ker_eq_bot_iff": 7, "ker_le_ker_comp": 8, "ker_mkq": 8, "ker_pi_quotient_mk": 7, "ker_restrict": 7, "kernel": [7, 8], "keyboard": 1, "keyword": [1, 2, 4, 5], "kim": 0, "kind": [0, 1, 6, 8, 9], "knew": 9, "know": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "known": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "k\u00fclshammer": 0, "l": [0, 1, 8, 10, 11], "label": [1, 2], "lagrang": 7, "lake": 0, "lambda": [2, 5], "lambda_l": 5, "lambda_nonneg": 5, "languag": [0, 1, 2, 3], "larg": [0, 6, 9], "larger": [1, 9], "last": [1, 2, 3, 4, 5, 6, 7, 9], "later": [0, 1, 2, 4, 5, 6, 7, 8, 9], "latter": [5, 7, 9], "lattic": [1, 5, 6, 7, 9], "law": [1, 7], "layer": [6, 9], "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": 9, "le_inf": 1, "le_inf_iff": 9, "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_opnorm": 10, "le_or_gt": 2, "le_principal_iff": 9, "le_refl": [1, 2], "le_sup": 4, "le_sup_left": 1, "le_sup_right": 1, "le_tran": [1, 2], "lead": [1, 2, 4, 5, 6, 7, 8, 9], "leader": 1, "lean": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "lean4": 1, "learn": [0, 1, 4, 5], "least": [1, 5, 6, 8, 9], "leav": [0, 1, 2, 3, 5, 6, 7], "lebesgu": 11, "led": 6, "left": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "left_distrib": [5, 6], "left_inv": [5, 8], "left_inv_eq_right_inv": 6, "left_inv_eq_right_inv\u2081": 6, "left_neg_eq_right_neg": 6, "leftinvers": 3, "leftinverse_invfun": 3, "legal": 1, "lemma": [2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "less": [1, 2, 3, 4, 5, 6, 7, 8, 9], "let": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "letter": [1, 5, 10], "level": [1, 2, 6, 8], "leverag": 9, "le\u2081": 6, "librari": [0, 1, 2, 3, 4, 5, 7, 9, 10], "life": [0, 2], "lift": [7, 8], "liftq": 8, "light": 5, "like": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "lim_": 9, "limit": [2, 6, 9], "linarith": [1, 2, 4, 5], "line": [0, 1, 2, 3, 4, 6, 7, 8], "linear": [1, 2, 5, 7, 9, 13], "linear_combin": 7, "linearcombin": 8, "linearcombination_apply_of_mem_support": 8, "linearcombination_repr": 8, "linearequiv": 8, "linearequivfunonfintyp": 8, "linearindepend": 8, "linearli": 8, "linearmap": 8, "linearord": 2, "linearorderedr": 5, "liner": 0, "linf": 5, "link": [5, 6], "list": [1, 2, 3, 4, 5, 8], "littl": [1, 2, 9, 10], "liu": 0, "live": [0, 5, 8], "ll": [0, 2, 4, 6, 9], "local": [1, 2, 6, 9, 10], "localinvers": 10, "lof": 8, "log": [1, 3, 11], "log_le_log": 1, "log_lt_log": 1, "logic": [0, 1, 3, 4, 5, 7, 8, 13], "logician": 1, "long": [1, 2, 3, 5, 6, 7, 8, 10], "longer": [0, 4, 5], "look": [1, 2, 3, 4, 6, 7, 8, 9], "loop": 4, "loos": 8, "loss": 4, "lot": [0, 1, 3, 5, 6, 7, 8, 9], "loud": 1, "lower": [1, 2, 4], "lowest": 4, "lr": 1, "lsmul": 8, "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, "lt\u2081": 6, "lu": 0, "lub": 1, "m": [0, 1, 2, 4, 6, 7, 8, 9, 10], "m_iunion": 11, "mac": [1, 2], "macbeth": 5, "machin": 8, "machineri": [5, 6, 8, 9], "maco": 0, "made": [1, 2, 3, 5, 8, 9], "magic": [2, 5, 6], "mai": [0, 1, 2, 3, 5, 6, 7, 8, 9, 10], "main": [2, 6, 8, 9, 10], "mainli": 7, "maintain": 1, "make": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "manag": [0, 1, 4, 5, 9], "mani": [1, 2, 3, 5, 6, 7, 8, 9, 10, 11, 13], "manifest": [1, 9], "manipul": [2, 5, 7, 8, 9], "manner": [2, 5], "manual": [0, 3, 4], "map": [1, 2, 3, 5, 6, 7, 9, 13], "map_add": [6, 7, 8, 10], "map_comap_eq": 8, "map_eq": 9, "map_inv": 7, "map_inv_of_inv": 6, "map_le_iff_le_comap": 9, "map_map": 9, "map_mono": 9, "map_mul": [6, 7, 8], "map_on": [6, 7], "map_pow": 7, "map_smul": [8, 10], "map_zero": [6, 7], "mapq": 8, "mapsto": [1, 5], "map\u2082": 6, "marc": 0, "mario": 0, "mark": [0, 1, 2, 6, 9], "marker": 2, "marriag": 5, "martin": 0, "mascellani": 0, "mass": 11, "master": [0, 1, 4], "match": [1, 2, 5], "mathbb": [3, 4, 5, 7], "mathcal": [5, 10], "mathemat": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "mathematician": [4, 9], "mathematics_in_lean": 0, "mathfrak": 7, "mathieu": 0, "mathlib": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "matric": [1, 5, 7, 13], "matrix": 8, "matter": [1, 2], "matthew": 0, "mauricio": 0, "max": [1, 2, 6, 8, 9, 11], "maxim": 7, "maximum": [2, 4, 9], "mayb": 6, "mcdowel": 0, "mdvdn": 4, "mean": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "meaning": 8, "meaningless": 2, "meant": [0, 2, 6, 8], "meanwhil": [1, 4], "measur": [0, 5, 9, 10, 13], "measurableset": 11, "measurablespac": 11, "measure_eq_iinf": 11, "measure_iunion_l": 11, "measuretheori": 11, "mechan": [1, 2, 5], "mediat": 4, "medit": 8, "meet": [1, 2, 3, 5], "mem": 3, "mem_": 4, "mem_ball_self": 9, "mem_bot": [7, 8], "mem_closedball_self": 9, "mem_closure_iff": 9, "mem_closure_iff_clusterpt": 9, "mem_closure_iff_nhds_basi": 9, "mem_closure_iff_seq_limit": 9, "mem_closure_of_tendsto": 9, "mem_comap": [7, 8], "mem_diff": 3, "mem_eras": 4, "mem_filt": 4, "mem_iff": 9, "mem_iint": 3, "mem_iinter\u2082": 3, "mem_image_of_mem": 3, "mem_inf": 8, "mem_insert": 4, "mem_insert_of_mem": 7, "mem_insert_self": 7, "mem_int": 4, "mem_inter_iff": 3, "mem_iunion": 3, "mem_iunion\u2082": 3, "mem_ker": [7, 8], "mem_map": [7, 8], "mem_map_of_mem": 8, "mem_nhds_iff": 9, "mem_of_dvd_prod_prim": 4, "mem_of_tendsto": 9, "mem_preimag": 8, "mem_rang": 7, "mem_sdiff": 4, "mem_setof": 3, "mem_sup": [7, 8], "mem_union": [3, 4], "member": [3, 9], "membership": [3, 4, 6, 7, 8], "mention": [2, 3, 5, 6, 7, 9], "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, 10, 13], "metricspac": [1, 9, 10], "mf": 2, "mg": 2, "mge2": 4, "mgt2": 4, "mid": 5, "middl": [0, 1, 2, 9], "midpoint": 5, "might": [1, 2, 3, 4, 5, 7], "mil": 0, "min": [1, 2, 9, 11], "min_le_left": 1, "min_le_right": 1, "mind": [1, 2, 5, 6, 7], "mindich": 0, "minfac": 4, "minim": 8, "minimum": 9, "minor": [6, 10], "minpoli": 8, "mislead": 7, "miss": [1, 3, 4], "mission": 0, "mk": [5, 6, 7, 8, 9], "mk_appli": 8, "mk_eq_mk_of_basi": 8, "mk_surject": 7, "mkofmuleqon": 7, "mkofnhd": 9, "mkq": 8, "mltn": 4, "mne1": 4, "mnez": 4, "mod": 5, "mod_4_eq_3_or_mod_4_eq_3": 4, "mod_def": 5, "mod_lt": 4, "mode": [1, 2, 5], "model": [3, 8, 9], "modern": [5, 7], "modifi": 6, "modu": 1, "modul": [6, 7, 8], "modular": 1, "module\u2081": 6, "module\u2083": 6, "modulo": [1, 4, 5], "moment": [1, 2, 5], "mono": 9, "monof": 2, "monoid": [2, 3, 4, 6, 8, 13], "monoidhom": 7, "monoidhomclass": 6, "monoidhomclass\u2081": 6, "monoidhomclass\u2082": 6, "monoidhomclass\u2083": 6, "monoidhom\u2081": 6, "monoid\u2081": 6, "monoid\u2082": 6, "monoid\u2083": 6, "monoton": [2, 6, 9], "monro": 0, "monticon": 0, "moral": [0, 5, 7], "more": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 13], "moreov": [0, 1, 4, 5, 9], "morphism": [5, 8, 10, 13], "morrison": 0, "most": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "mostli": 7, "motiv": [2, 8], "move": [0, 1, 2, 6, 8, 9], "mp": [1, 2, 3, 4, 9], "mpr": [1, 2, 5, 9], "much": [0, 2, 4, 6, 7, 8, 9, 10], "mul": [4, 5, 6, 9], "mul_add": [0, 1, 4, 6], "mul_appli": 8, "mul_assoc": [1, 2, 4, 5, 6, 7], "mul_assoc\u2083": 6, "mul_comm": [1, 2, 4, 5, 6, 7], "mul_def": 5, "mul_div_cancel": 4, "mul_div_cancel\u2080": 2, "mul_eq_comp": 8, "mul_im": 5, "mul_inv": [6, 7], "mul_inv_cancel": [1, 5, 7], "mul_inv_cancel_right": 5, "mul_inv_rev": 1, "mul_le_inf": 7, "mul_le_left": 7, "mul_le_mul": 2, "mul_le_right": 7, "mul_left_cancel\u2083": 6, "mul_left_comm": 4, "mul_left_not_lt": 5, "mul_lt_mul_right": 2, "mul_mem": [6, 7], "mul_mod": 4, "mul_mod_mod": 4, "mul_mod_right": 4, "mul_nonneg": 1, "mul_on": [1, 5, 6, 7], "mul_po": [1, 4], "mul_r": 5, "mul_right_cancel\u2083": 6, "mul_right_inj": 4, "mul_smul": [6, 7], "mul_sub": 1, "mul_sum": 5, "mul_zero": [1, 5, 6], "mulact": 7, "mulequiv": 7, "muloneclass": 6, "multilinear": 10, "multipl": [1, 2, 3, 4, 5, 6, 7, 8, 10], "multipli": [5, 8], "multiset": 7, "multivari": 7, "mulvec": 8, "mulzeroclass": 6, "mundan": 2, "must": [1, 5, 6, 8, 9], "mvpolynomi": 7, "my_fil": 0, "my_lemma": 2, "my_lemma2": 2, "my_lemma3": 2, "my_lemma4": 2, "my_squar": 5, "myab": 2, "myelement": 7, "mygroup": 7, "mymap": 7, "mymorph": 7, "mynat": 4, "mynewmorph": 7, "mypoint1": 5, "mypoint2": 5, "mypoint3": 5, "myre": 1, "mysmul": 6, "mysquar": 5, "mysteri": [1, 5, 6], "mz": 4, "m\u02e3": 7, "n": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "n_p": 9, "n_q": 9, "na": 2, "naiv": [6, 9], "name": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "namespac": [1, 2, 3, 4, 5, 7, 8, 9], "nash": 0, "nat": [0, 1, 2, 3, 4, 5, 7, 9], "natab": 5, "natabs_mul": 5, "natabs_norm_mod_lt": 5, "natabs_of_nonneg": 5, "natal": 0, "natcast_natab": 5, "natdegre": 7, "natdegree_comp": 7, "natdegree_mul": 7, "natur": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "nb": 2, "ne": [4, 5], "nearbi": [1, 4], "nearest": 5, "nebot": 9, "nebot_of_l": 9, "necessari": [0, 2, 4, 5, 7, 8], "necessarili": [1, 8, 11], "need": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "neg": [5, 6, 9, 11], "neg_add": 6, "neg_add_cancel": [1, 5], "neg_add_cancel_left": 1, "neg_def": 5, "neg_eq_of_add_eq_zero": 1, "neg_im": 5, "neg_le_abs_self": 2, "neg_mem": 7, "neg_neg": 1, "neg_r": 5, "neg_zero": 1, "negat": [1, 5, 13], "negsucc": 6, "neighborhood": 9, "neither": [3, 5, 6, 8], "neq": 4, "nest": [1, 2], "net": 1, "neutral": [6, 7], "never": [0, 6], "new": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "newcom": 0, "next": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "nge": 2, "nhd": 9, "nhds_basis_bal": 9, "nhds_basis_closedbal": 9, "nhds_basis_ioo_po": 9, "nhds_basis_open": 9, "nhds_induc": 9, "nhds_mkofnhd": 9, "nhds_prod_eq": 9, "nice": [1, 2, 4, 6, 7, 8, 9], "nicer": [5, 7, 9], "nicola": 0, "nineteenth": 3, "nna": 2, "nnc": 2, "nnez": 4, "nnf": 2, "nng": 2, "nnz": 4, "non": [1, 3, 6, 7, 8, 9, 11], "noncomm_r": 1, "noncomput": [3, 5, 7, 8], "nonconstruct": 7, "nondecreas": [2, 4], "nondistribut": 1, "nonempti": [3, 7, 9], "nonempty_interior_of_iunion_of_clos": 10, "nonexist": 2, "nonneg": [1, 5], "nonneg_of_mul_nonneg_left": 1, "nontrivi": [2, 3, 4, 5, 8, 9, 10], "nontriviallynormedfield": [10, 11], "nonzero": [2, 4, 5, 11], "nor": [3, 5, 8], "norm": [2, 5, 9, 13], "norm_add_l": 10, "norm_conj": 5, "norm_eq_zero": [5, 10], "norm_mod_lt": 5, "norm_mul": [5, 10], "norm_nonneg": [5, 10], "norm_num": [1, 2, 4, 5, 8], "norm_po": 5, "norm_smul": 10, "norm_y_po": 5, "normal": 7, "normedaddcommgroup": [10, 11], "normedaddgroup": 10, "normedfield": 10, "normedgroup": 10, "normedspac": [10, 11], "not_even_iff": 3, "not_even_iff_odd": 3, "not_imp_self": 3, "not_le_of_gt": 2, "not_lt_of_g": [2, 4, 5], "not_monotone_iff": 2, "not_norm_mul_left_lt_norm": 5, "not_not": 2, "notat": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "note": [1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "noth": [1, 2, 3, 4, 5, 6, 7], "notic": [1, 2, 3, 4, 5, 7, 9], "notin": 3, "notion": [1, 2, 3, 4, 5, 7, 8, 9, 10, 11], "noun": 6, "now": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "nozerodivisor": 7, "np": 4, "npow_nz": 4, "npowz": 4, "nsmul": [5, 6], "nsmul_succ": 6, "nsmul_zero": 6, "nsmulrec": 5, "nsmul\u2081": 6, "nsqr_nez": 4, "nt": 2, "nth_rw": 1, "number": [0, 1, 2, 3, 5, 6, 7, 8, 9, 10, 13], "numer": [1, 4, 5], "nut": 1, "n\u2080": 2, "n\u2081": 2, "o": 10, "obfusc": 9, "object": [0, 1, 2, 3, 4, 5, 7, 8, 13], "observ": [2, 4, 9], "obtain": [1, 2, 4, 5, 9, 10], "obviou": [0, 4, 5, 6], "occasion": 9, "occur": 4, "occurr": 1, "odd": [1, 2, 3, 4, 8], "odd_iff": 3, "of_fintype_basi": 8, "of_foral": 9, "of_le_succ": 4, "of_map": 9, "ofbiject": [7, 8], "off": [2, 3, 4], "offend": 6, "offer": [0, 2, 5, 9], "ofnat": 6, "ofnat_l": 5, "ofnat_lt": 5, "ofreal": 7, "often": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "og": 2, "old": [2, 5, 6, 8], "oliv": 0, "omit": 5, "onc": [1, 2, 3, 4, 5, 6, 7, 9, 11], "one": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "one_add_one_eq_two": 1, "one_def": 5, "one_dia": 6, "one_eq_top": 7, "one_fin_two": 8, "one_im": 5, "one_mem": [6, 7], "one_mul": [1, 2, 5, 6], "one_r": 5, "one_smul": [6, 7], "oner": 1, "ones": [0, 1, 2, 3, 5, 8, 11], "one\u2081": 6, "one\u2082": 6, "onli": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "onlin": 0, "onto": [7, 8], "open": [0, 1, 2, 3, 4, 5, 7, 8, 10, 11], "oper": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "opnorm_le_bound": 10, "opnorm_le_of_shel": 10, "opportun": [7, 9], "opposit": [6, 9], "optim": [6, 8, 11], "option": [1, 2, 4, 5, 6, 9], "orbit": 7, "orbitequivquotientstabil": 7, "orbitrel": 7, "order": [1, 2, 3, 4, 5, 6, 8, 9, 10], "orderedcanceladdcommmonoid": 2, "orderedcommmonoid\u2081": 6, "orderpreshom": 6, "orderpreshomclass": 6, "orderpresmonoidhom": 6, "ordinari": [1, 2, 4, 5, 7, 8, 9], "ordinarili": [4, 5], "organ": 0, "organiz": 1, "orient": 5, "origin": [0, 1, 5, 7], "other": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "otherwis": [1, 2, 3, 4, 5, 7], "ott": 0, "our": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "ourselv": [4, 6], "out": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "outer": 1, "outermost": 3, "outlin": [1, 2, 4, 9], "outparam": 6, "output": [1, 7], "outsid": [1, 4, 8], "over": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "overlap": [6, 7], "overload": 3, "overview": 13, "own": [0, 1, 4, 5, 6], "p": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "p4": 4, "p4eq": 4, "p_1": 4, "p_i": [4, 9], "p_k": 4, "p_n": 4, "p_ne_zero": 7, "packag": [7, 8], "page": [0, 1, 4], "pai": [1, 2, 6, 7, 9], "pain": 7, "pair": [1, 2, 4, 5, 7, 9], "pairwis": [8, 11], "pairwisedisjoint": 8, "panel": 0, "paper": [2, 3, 5, 7, 8, 9, 11], "paquet": 0, "paradox": [8, 9], "paragraph": 9, "parallel": 8, "paramet": [5, 6], "parent": 6, "parenthes": [1, 2, 3, 4], "pariti": 0, "parity_simp": 0, "pars": [1, 3, 7], "part": [1, 2, 3, 4, 5, 6, 8, 9, 11], "partial": [0, 1, 2, 3, 5, 6, 7, 8], "partialord": [1, 2], "partialorder\u2081": 6, "particular": [1, 2, 5, 6, 7, 8, 9], "partit": 7, "partli": [1, 6, 7], "pass": [1, 5], "past": [0, 1, 7], "path": 6, "patholog": 9, "pattern": [1, 2, 3, 5, 6], "payoff": 5, "pdf": 0, "pdvd": 4, "pedro": 0, "peel": 2, "pen": [2, 7], "peopl": [0, 1], "perform": [1, 2, 3], "perm": [5, 7], "permgroup": 5, "permiss": 1, "permut": [4, 7], "person": 0, "perspicu": 2, "phenomenon": 3, "phrase": [0, 1, 2, 4, 5, 8], "pi": [7, 8, 9], "pick": [0, 6], "pictur": [4, 5, 7], "piec": [1, 4, 5, 6, 7, 9], "pierpaolo": 0, "pietro": 0, "pim": 0, "pinot": 7, "piotrowski": 0, "place": [0, 1, 2, 5, 8, 9], "placehold": 2, "placement": 4, "plai": [1, 3, 4, 6, 7, 8, 9], "plan": [1, 6, 9], "plane": 9, "plausibl": 3, "ple": 4, "pltn": 4, "pne3": 4, "point": [0, 1, 2, 3, 5, 6, 7, 8, 9, 10, 11], "pointwis": [5, 9, 10], "polynomi": [5, 8], "ponen": 1, "poor": 6, "pop": 0, "port": 0, "posit": [1, 3, 4, 5, 9, 11], "possibl": [1, 2, 3, 4, 5, 7, 9], "possibli": 5, "postfix": 6, "pos\u2080": 2, "potscrubb": 0, "pow_eq": 4, "pow_eq_zero": [2, 4], "pow_succ": 4, "pow_two": [1, 4], "pow_two_le_fac": 4, "pow_two_nonneg": [1, 2], "power": [0, 1, 3, 4, 5, 6, 8], "pp": 4, "pq": 8, "practic": [1, 2, 3, 6, 7, 9], "pragmat": 5, "pre": [2, 8], "preal": 5, "preced": [4, 7], "precis": [1, 3, 7, 8, 9, 10], "precondit": 9, "pred": 4, "predecessor": 4, "predic": [2, 3, 4, 6, 7, 8, 9, 10], "prefer": [0, 1, 2, 3], "prefix": [4, 6, 7], "preimag": [3, 7, 8, 9], "preliminari": 6, "prematur": 6, "preorder": [2, 6, 9], "preorder\u2081": 6, "presenc": 6, "present": [1, 2, 4, 7, 9], "presentedgroup": 7, "preserv": [4, 6, 8, 9], "preserves_mul": 5, "press": [0, 8], "presuppos": 0, "pretend": [6, 8], "pretti": [2, 6, 7, 8, 9], "previou": [1, 2, 3, 5, 6, 7, 9, 10, 11], "previous": 6, "price": 9, "primari": 6, "primarili": [6, 7, 9], "prime": [1, 2, 3, 5, 6, 7, 8, 13], "prime_def_lt": 4, "prime_iff": 3, "prime_of_mem_primefactorslist": 4, "prime_p": 4, "prime_q": 4, "prime_thre": 4, "prime_two": 4, "prime_x": 3, "primefactorslist": 4, "primefactorslist_uniqu": 4, "primes_infinit": 4, "primes_mod_4_eq_3_infinit": 4, "primit": [2, 3], "princip": 9, "principl": [1, 2, 3, 4, 6, 8, 10], "print": [0, 3, 4, 5, 11], "priori": [6, 8], "prioriti": 5, "probabl": [1, 5, 6, 9], "problem": [3, 4, 5, 6, 9], "proce": [4, 6], "procedur": [4, 6], "proceed": 7, "prod": [4, 7, 8, 9, 11], "prod_": 4, "prod_empti": 4, "prod_insert": 4, "prod_map": 9, "prod_mk": 9, "prod_po": 4, "prod_primefactorslist": 4, "prod_range_succ": 4, "prod_range_zero": 4, "prodcongr": 7, "prodequivpi": 7, "prodmap": 8, "produc": [1, 2, 7, 10], "product": [2, 4, 5, 6, 7, 9, 11], "profici": 4, "program": [0, 1, 2], "progress": [0, 1, 5, 7], "prohibit": 9, "proj": 8, "project": [0, 4, 5, 7, 8, 9], "projector": 7, "promin": 7, "promis": [6, 8, 9], "promot": 1, "proof": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "prop": [0, 2, 3, 4, 5, 6, 7, 8, 9, 11], "propag": 6, "properti": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "proposit": [0, 2, 3, 4, 5], "protect": 5, "provabl": [1, 3, 6, 9], "prove": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "proven": [7, 8], "provid": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "proxi": 5, "pseudoemetricspac": 9, "pseudometricspac": 9, "psycholog": 6, "pull": [0, 7, 9], "pullback": [7, 9], "pun": 2, "pure": [1, 9], "pure_le_nhd": 9, "purpos": [1, 2, 3, 4, 5, 6, 8, 9], "push": [2, 4, 7, 9], "push_neg": [2, 3, 4], "push_pul": 9, "pushforward": [7, 9], "put": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "q": [2, 4, 5, 6, 7, 8, 9], "qk": 4, "quad": 5, "quadrat": 5, "quantifi": [1, 3, 4, 5, 7, 9, 13], "quantiti": 9, "quest": 6, "question": [0, 4, 6, 9, 11], "quick": [4, 7, 8, 10], "quicker": 0, "quickli": [3, 7, 11], "quirki": 4, "quit": [2, 6, 9], "quot": [5, 8, 9], "quotequivofeq": 7, "quotient": [4, 5, 6, 9, 13], "quotient_mul_add_remainder_eq": 5, "quotient_zero": 5, "quotientgroup": 7, "quotientinfringequivpiquoti": 7, "quotientkerequivrang": 7, "quotientmap": 7, "quotientmonoid": 6, "quotientmulequivofeq": 7, "quotkerequivrang": 8, "r": [1, 2, 4, 5, 6, 7, 8, 9], "r_wellfound": 5, "radiu": 9, "raini": 3, "rais": [1, 4], "random": 6, "rang": [0, 2, 3, 4, 7, 8, 9], "range_eq_map": 8, "range_eq_top": 8, "range_mkq": 8, "rank": 8, "rare": 6, "rather": [0, 1, 2, 4, 5, 6, 7, 8, 9], "ration": [1, 2, 4, 9], "rb": 9, "rcase": [2, 3, 4, 9], "rclike": 10, "re": [4, 5], "reach": [2, 6], "read": [0, 1, 4, 5, 6, 7, 8, 9], "readabl": [1, 2, 3, 8, 9], "reader": [1, 8, 9], "readi": [4, 6, 7, 8, 9, 10], "real": [1, 2, 3, 4, 5, 6, 8, 9, 10, 11], "real_norm_l": 10, "realli": [1, 2, 3, 4, 6, 7, 8, 9], "reason": [0, 1, 2, 4, 5, 6, 7, 8, 9], "rec_on": 9, "recal": [1, 2, 4, 5, 7, 9, 11], "recaptur": 9, "recast": 9, "recent": 5, "recogn": [1, 2, 4, 5, 6, 9], "recommend": [0, 1, 3], "recon": 9, "reconcil": 2, "record": [5, 6, 8], "recov": 9, "recurs": [2, 3, 5, 13], "redefin": [5, 6], "reduc": [0, 2, 3, 4, 5], "reduct": [2, 3, 5], "redund": [1, 5, 8, 9, 11], "refer": [0, 1, 2, 4, 5, 6, 8, 9, 10], "refin": [4, 10], "refl": [2, 3, 5, 6, 7, 8], "refl_tran": 5, "reflect": 2, "reflex": [1, 2, 5], "reformul": 9, "refus": [6, 9], "regiment": 0, "region": 3, "regist": [5, 6, 7, 8], "regular": [6, 9], "regularspac": 9, "rel": [3, 5, 8], "relat": [1, 2, 3, 5, 6, 7, 8, 9, 10, 11], "relatedli": 9, "relationship": [3, 4], "relativ": 3, "relev": [0, 1, 2, 4, 5, 6, 7, 8, 9], "reli": [1, 2, 5, 9], "remain": [0, 1, 2, 3, 5, 6, 9], "remaind": [4, 5, 7], "remainder_lt": 5, "remark": [5, 6], "rememb": [1, 2, 3, 4, 5, 6, 7, 8, 9], "remov": [4, 9], "renam": 0, "render": [2, 4], "repeat": [1, 4, 5, 6], "repeatedli": [2, 9], "repetit": [1, 6], "replac": [0, 1, 2, 3, 4, 6, 7, 8], "replai": 0, "report": 1, "repositori": [0, 1], "repr": 8, "repres": [0, 1, 2, 3, 4, 5, 6, 10], "represent": [3, 4, 5, 8], "reproduc": 5, "reprov": [1, 7, 8], "requir": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "resolut": 6, "resolve_left": 3, "resourc": 0, "resp": 8, "respect": [1, 2, 3, 4, 5, 7, 8, 9], "respons": [0, 1], "rest": [2, 3, 5, 7, 9], "restat": [2, 6, 7, 8], "restor": 6, "restrict": [3, 4, 7, 9], "result": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "retri": 6, "return": [0, 2, 3, 4, 5, 7, 8, 9], "reus": 6, "reusabl": 6, "reveal": [1, 8], "revers": [1, 2, 3, 5, 9], "revert": [4, 5], "review": [7, 9], "rewrit": [0, 1, 2, 3, 4, 5, 6, 8, 9], "rewritten": 3, "rfl": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "rich": [5, 6], "rid": 2, "right": [1, 2, 3, 4, 5, 6, 8, 9, 10], "right_distrib": [5, 6], "right_inv": [5, 8], "rightinvers": 3, "ring": [0, 1, 2, 3, 4, 5, 6, 8, 13], "ringequiv": 7, "ringhom": [6, 7], "ringhomclass\u2083": 6, "ringhom\u2081": 6, "ring\u2081": 6, "ring\u2083": 6, "rintro": [0, 2, 3, 4, 7, 8, 9], "rise": [4, 6, 7], "road": 5, "robust": [5, 6], "role": [4, 5, 8, 9], "roll": 10, "rolland": 0, "roman": 5, "root": [5, 6, 7, 8, 13], "roots_mul": 7, "roots_x_sub_c": 7, "roughli": [2, 3, 4], "round": [0, 1, 5], "routin": 2, "row": 8, "rpo": 9, "rule": [0, 2, 4, 5, 6, 8, 9], "run": 0, "rush": 0, "russel": 8, "rw": [0, 2, 3, 4, 5, 6, 7, 8, 9, 13], "rwa": [3, 4, 5], "r\u02e3": 7, "s_": 3, "s_0": [2, 3], "s_1": 2, "s_2": 2, "s_n": [2, 3], "sa": 2, "sad": 9, "safe": [6, 7], "safer": 7, "sage": 8, "sai": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "said": [0, 2, 4, 5], "sake": [1, 4], "salient": 9, "same": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "satisfi": [1, 3, 4, 5, 6, 9, 10], "save": 2, "saw": [1, 5, 6, 7, 8, 9], "sb": 2, "sb_fun": 3, "sb_inject": 3, "sb_right_inv": 3, "sb_surject": 3, "sbaux": 3, "sbfun": 3, "sbset": 3, "scalar": [5, 6, 7, 8, 10], "scale": 3, "scari": 5, "scheme": 5, "schroeder_bernstein": 3, "schr\u00f6der": 13, "scienc": 6, "scientist": 2, "scope": [1, 2, 3, 5, 7, 8], "scratch": 2, "script": 1, "search": [4, 5, 6], "second": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "secretli": 8, "section": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "see": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "seek": 5, "seem": [1, 2, 4, 6, 9, 10], "seen": [0, 1, 2, 4, 5, 6, 7, 8, 9], "segment": [9, 11], "select": [0, 9], "self": 6, "self_of_nhd": 9, "self_sub": 1, "self_trans_symm": [5, 7, 8], "selfequivsigmaorbit": 7, "selfmodul": 6, "semi": [6, 7, 8], "semicolon": [2, 4], "semigroup": 6, "semigroup\u2081": 6, "semigroup\u2082": 6, "semigroup\u2083": 6, "semir": [6, 7], "send": [7, 8, 11], "sens": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10], "sensibl": 9, "sent": [7, 9], "separ": [0, 1, 2, 4, 5, 8], "sequenc": [3, 6, 9, 10, 13], "seri": 7, "seriou": [4, 6, 9], "serv": [1, 3, 4, 5, 11], "set": [0, 1, 2, 4, 5, 6, 7, 10, 11, 13], "set_opt": 6, "setco": 6, "setintegral_const": 11, "setlik": 6, "setminu": 3, "setoid": [6, 7], "sets_of_superset": 9, "setub": 2, "setup": [7, 8], "seurin": 0, "sever": [6, 8, 9, 11], "shade": 3, "shame": 6, "sharp": 0, "shift": [0, 1, 6, 9], "short": [0, 1, 2, 3, 4, 5, 8], "shorten": [1, 2, 7], "shorter": [1, 3, 4, 7, 9], "shot": 9, "should": [0, 1, 2, 3, 4, 5, 6, 7, 9, 10], "shouldn": [8, 9], "show": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "shown": [1, 5, 10, 11], "side": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "sight": [2, 6], "sigma": [5, 11], "sigmafinit": 11, "sign": 9, "signatur": 6, "signific": 3, "silent": [5, 6], "silli": 6, "silva": 0, "similar": [1, 2, 3, 5, 6, 7, 8, 9], "similarli": [2, 3, 4, 5, 7, 8], "simp": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10], "simp_rw": 7, "simpa": [4, 7, 10], "simpl": [2, 4, 5, 6, 10], "simpler": [6, 8], "simplex": 5, "simpli": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "simplif": [2, 3, 4], "simplifi": [0, 2, 3, 4, 5, 9, 11], "sin": [2, 10], "sinc": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "singl": [0, 1, 2, 3, 4, 5, 6, 7, 8, 10], "singleton": 4, "sinter": 3, "sinter_eq_biint": 3, "situat": [1, 3, 6, 7, 9], "size": 8, "skeleton": [5, 8, 9], "sketch": [2, 3, 4, 9], "skill": [0, 1, 2, 3, 4], "slick": 2, "slight": 3, "slightli": [1, 6, 7, 8, 9, 10], "slow": 9, "small": [0, 2, 4, 5, 9], "smaller": [3, 4, 9], "smallest": [4, 6, 8, 9], "smart": 4, "smul": [5, 6, 7, 8], "smul_add": [6, 8], "smul_comm": 8, "smul_distrib": 5, "smul_mem": 8, "smul\u2083": 6, "snd": [5, 8, 9], "snippet": [2, 4, 5, 7, 8], "so": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "solut": [0, 1, 4, 6], "solv": [0, 1, 2, 3, 4, 5, 6, 8, 9], "some": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "somehow": [7, 8], "someth": [0, 1, 2, 4, 6, 8, 9], "sometim": [1, 2, 3, 4, 5, 6, 7, 8, 9], "somewhat": [1, 3, 9], "somewher": 9, "soon": [0, 2, 6, 7, 8, 9], "sophist": 9, "sorri": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "sort": [1, 3, 4], "sosi": 2, "sosx": 2, "sound": [3, 5, 6], "sourc": [2, 9], "space": [1, 2, 3, 5, 6, 7, 11, 13], "span_eq": 8, "span_induct": 8, "span_l": 8, "span_union": 8, "speak": [2, 5, 7, 9], "special": [3, 4, 5, 6, 7, 8, 9, 11], "specif": [0, 1, 3, 4, 5, 6], "specifi": [1, 2, 3, 4, 5, 8, 9, 10, 11], "spell": [8, 9], "split": [1, 2, 3, 4], "spot": 2, "sq_ab": 5, "sq_add_sq_eq_zero": 5, "sq_nonneg": 1, "sqr_eq": 4, "sqrt": [2, 3, 4, 5], "squar": [1, 2, 4, 5, 6, 7, 8], "squiggli": 2, "ss": 3, "ssubt": 3, "stabil": 7, "stabl": 8, "stage": [2, 5, 6], "stai": 5, "stand": [1, 2, 4, 5, 6, 7, 8, 9, 10], "standard": [4, 5, 6, 9], "standardsimplex": 5, "standardtwosimplex": 5, "start": [1, 2, 3, 4, 6, 7, 8, 9, 10, 11, 13], "state": [0, 1, 2, 3, 4, 6, 7, 8, 9, 10], "statement": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "stdsimplex": 5, "steep": 0, "steinhau": 10, "step": [0, 1, 2, 3, 4, 5, 6], "steven": 0, "stick": [1, 2, 9, 10], "still": [0, 1, 2, 3, 4, 5, 6, 8, 9, 11], "stipul": 10, "stop": 6, "store": 5, "stori": [6, 8], "str": 5, "straightforward": [2, 6], "strang": [2, 4, 7, 8], "strategi": [1, 2, 4], "strength": 1, "strengthen": [1, 2, 4], "stretch": [4, 5], "strict": [1, 2], "stricter": 10, "strictli": [1, 2, 10], "strictmono": 9, "strictorderedr": 1, "strike": [1, 2], "strong": [2, 4], "strong_induction_on": 4, "stronger": 9, "strongli": 0, "stronglymeasurableatfilt": 11, "struc": 5, "structur": [2, 4, 6, 7, 9, 10, 11, 13], "stuck": 6, "studi": [6, 9], "style": [0, 1], "sub": [3, 9, 11, 13], "sub_add_cancel": 1, "sub_eq_add_neg": 1, "sub_self": [1, 2], "sub_sub": 1, "subgoal": 2, "subgroup": 6, "subgroupclass\u2081": 6, "subgroupofmulact": 7, "subgroup\u2081": 6, "subject": 5, "submodul": [7, 8], "submodule_independ": 8, "submodule_isup_eq_top": 8, "submonoid": [6, 7], "submonoidclass\u2081": 6, "submonoid\u2081": 6, "submonoid\u2081monoid": 6, "subobject": 6, "subproof": 1, "subr": 6, "subscript": [1, 8], "subsequ": [2, 4, 9], "subset": [1, 2, 3, 5, 9, 10], "subset_def": 3, "subset_iff": 4, "subspac": [1, 6, 13], "substant": 4, "substanti": 0, "substitut": [0, 2], "subsum": 4, "subtl": [5, 7, 8, 9], "subtleti": [6, 7, 8], "subtract": [1, 4, 5], "subtyp": [5, 6, 7, 8, 9], "succ": [4, 6], "succ_add": 4, "succ_le_succ": 4, "succ_mul": 4, "succ_ne_zero": 4, "succ_po": 4, "succe": 6, "success": 6, "successor": [4, 8], "suffic": [1, 2, 3, 7, 9], "suffici": [4, 9], "suggest": [0, 2, 4, 5, 8, 9], "suitabl": [0, 1, 2, 5, 9], "sum": [1, 2, 4, 5, 6, 7, 9], "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_repr": 8, "sum_sqr": 4, "summand": 8, "summat": 4, "sumofsquar": 2, "sumofsquares_mul": 2, "sunion": 3, "sunion_eq_biunion": 3, "sup": [1, 4, 9], "sup_assoc": 1, "sup_comm": 1, "sup_eq_closur": 7, "sup_eq_top": 8, "sup_inf_left": 1, "sup_inf_right": 1, "sup_inf_self": 1, "sup_l": 1, "superfici": 9, "superscript": 9, "supersed": 8, "suppli": 5, "support": [0, 1, 2, 3, 4, 5, 6, 8, 9], "suppos": [1, 2, 3, 4, 5, 9], "suppress": 1, "supremum": [1, 4, 6, 7, 8], "sure": [0, 1, 2, 3, 5, 6, 7, 8], "surject": [2, 3, 7, 8, 9], "surjf": [2, 3], "surjg": 2, "surpris": 6, "surprisingli": [5, 6], "swap": 5, "swapxi": 5, "sweet": 3, "switch": [1, 6], "sylow": 7, "symbol": [1, 2, 5, 6, 7], "symm": [3, 4, 5, 6, 7, 8, 9, 10], "symmetr": [2, 3, 7], "symmetri": [3, 6], "synonym": 7, "syntact": 2, "syntax": [0, 1, 2, 4, 6, 8], "synth": 6, "synthes": [5, 6], "synthesi": 8, "synthinst": 6, "system": [3, 4, 5, 6, 8], "s\u00e1nchez": 0, "s\u02e3": 7, "s\u1d9c": [9, 11], "s\u2081": 6, "s\u2082": 6, "t": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "t2space": 9, "t3space": 9, "t_": 9, "t_3": 9, "t_x": 9, "t_y": 9, "t_z": 9, "tab": [1, 3, 4], "tackl": 6, "tactic": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "tag": [2, 3, 6], "take": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "taken": [1, 2], "takeshi": 0, "talk": [4, 7, 8, 9, 10], "tantamount": [1, 3], "target": [1, 6, 7, 8, 9, 11], "task": [0, 2, 4, 5, 6, 9], "taught": 7, "tauto": 4, "tautologi": 4, "teach": 0, "tear": 6, "technic": [1, 5, 6, 8], "techniqu": [2, 9], "technologi": 6, "tediou": [1, 2, 6], "tell": [0, 2, 3, 4, 5, 6, 7, 8], "temporarili": [1, 2], "tempt": 6, "tend": [1, 9], "tendsto": [9, 11], "tendsto_attop": 9, "tendsto_congr": 9, "tendsto_iff": 9, "tendsto_integral_of_dominated_converg": 11, "tendsto_nhds_uniqu": 9, "tendsto_pow_attop_nhds_zero_of_lt_on": 9, "tendsto_right_iff": 9, "tendsto_subseq": 9, "tendsto\u2081": 9, "tendsto\u2082": 9, "term": [0, 1, 2, 3, 4, 5, 7, 8, 9], "terminologi": [5, 8], "terraf": 0, "ters": 6, "test": 4, "text": [0, 3, 5, 9], "textbook": [0, 1, 2], "th": [4, 8], "than": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "thank": 6, "thei": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "them": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "theme": 3, "themselv": [0, 4, 5], "theorem": [0, 2, 4, 5, 7, 8, 9, 10, 11, 13], "theoret": [2, 3, 8, 9], "theori": [0, 1, 2, 3, 6, 7, 8, 9, 10, 13], "therefor": [1, 4, 5, 8, 9], "thereof": 0, "thi": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "thing": [0, 1, 2, 3, 4, 5, 6, 8, 9], "think": [0, 1, 2, 3, 4, 5, 6, 8, 9, 10], "third": [1, 2, 3, 5, 9], "thoma": 0, "thorough": 0, "those": [0, 1, 2, 3, 5, 6, 7, 8, 9, 10], "though": [2, 3, 4, 5], "three": [1, 2, 4, 5, 7, 9], "through": [0, 1, 3, 4, 5, 6, 7, 8, 9], "thu": [1, 3, 4, 5, 9], "thumb": 4, "tighter": [1, 3], "tightli": 5, "time": [1, 4, 5, 6, 8, 9, 10, 11], "timesav": 1, "tiresom": 9, "to_addit": 6, "to_localinvers": 10, "toaddcommgroup\u2083": 6, "toaddgroup\u2083": 6, "todiaoneclass\u2081": 6, "todia\u2081": 6, "tofun": [5, 6, 8], "togeth": [1, 2, 3, 4, 5, 7, 9], "togroup": 7, "tomatrix": 8, "tomatrix_comp": 8, "tomatrix_id": 8, "tomatrix_mulvec_repr": 8, "tomodul": 8, "tomonoidhom\u2081": 6, "tomuloneclass": 6, "too": [0, 1, 3, 5, 6, 7, 8, 9], "toohei": 0, "tool": [0, 1, 5, 6], "toone\u2081": 6, "top": [0, 6, 7, 8, 9, 10], "topermhom": 7, "topic": [4, 5, 6, 7, 8], "topolog": [5, 6, 10, 13], "topologi": [1, 5, 6, 10, 13], "topologicalspac": [9, 10], "toreal": 11, "tortuou": 8, "tosemigroup\u2081": 6, "tosmul\u2083": 6, "total": 1, "tour": [9, 10], "toward": 7, "trace": [6, 8], "tradeoff": 3, "tradition": 7, "train": [1, 6], "tran": [1, 2, 4, 5, 6, 7, 8], "trans_assoc": 5, "trans_refl": 5, "transform": [2, 3], "transit": [1, 2, 5, 9], "translat": [4, 6, 7, 9], "transpos": 8, "trap": 6, "treat": [2, 3, 5, 6, 7, 9, 10], "treatment": 7, "tri": [1, 2, 4, 6], "triangl": [1, 2, 5], "trick": [1, 2, 4, 6, 10], "tricki": [2, 3, 4, 6, 7], "trigger": [6, 8], "tripl": 3, "trivial": [3, 4, 7, 8, 9], "troubl": [2, 3, 5], "true": [1, 2, 3, 6, 8, 9], "truncat": 4, "trust": 8, "truth": [1, 4], "try": [0, 1, 2, 3, 4, 5, 6, 8, 9], "tucker": 0, "tupl": 5, "turn": [2, 3, 4, 5, 6, 8, 9, 10], "tutori": 0, "twice": [0, 1, 9], "two": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "two_l": 4, "two_le_of_mod_4_eq_3": 4, "two_mul": 1, "ty": 7, "type": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "typeclass": [6, 8], "typic": [1, 7], "u": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "u_2": 8, "u_n": 8, "ubf": 2, "ubfa": 2, "ubg": 2, "ubgb": 2, "ulequiv": 7, "ultim": 0, "un": 3, "unapp": 1, "unbundl": 6, "unchang": [1, 2], "uncom": 1, "uncount": 9, "uncurri": 9, "under": [5, 6, 7, 8, 9], "underli": [0, 1, 5, 6, 7, 8], "underneath": [1, 3], "underscor": [1, 2, 3, 8], "understand": [0, 2, 3, 4, 5, 6, 7, 8, 9], "understood": [4, 9], "unfold": [1, 2, 3, 4, 5, 9], "unfortun": 7, "unicod": [1, 3, 6], "unif": 6, "uniform": [3, 9, 10], "uniformcontinu": 9, "uniformcontinuous_iff": 9, "uniformli": 10, "union": [1, 3, 4, 5, 6, 7, 8, 10, 11], "union_def": 3, "uniqu": [1, 2, 3, 4, 5, 7, 8, 9], "unit": [5, 6, 9], "units_eq_one_or": 7, "univ": [3, 9, 10, 11], "univ_set": 9, "univari": 7, "univers": [1, 3, 5, 7, 8, 9, 13], "unknown": 6, "unless": [1, 2, 5], "unlik": [3, 4], "unnecessari": [3, 7], "unneed": 8, "unpack": [2, 3], "unpleas": [6, 9], "unrel": 6, "unshad": 3, "unspecifi": [6, 8], "unsurprisingli": 3, "until": [1, 4, 6, 9], "up": [0, 2, 3, 4, 5, 6, 7, 9], "updat": 0, "upper": [1, 2], "us": [0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 13], "usabl": 6, "usag": 1, "useless": 8, "user": [0, 6], "usual": [1, 2, 3, 4, 5, 7, 8, 9, 11], "v": [0, 1, 2, 3, 5, 8, 9], "val": 5, "valid": 2, "valu": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "van": 0, "vandermond": 8, "vanish": [7, 8], "varepsilon": [2, 9], "variabl": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "variant": [1, 2, 7, 9], "variat": [1, 3, 4, 5, 9, 10], "varieti": 9, "variou": [2, 3, 5, 6, 8, 11], "vastli": 2, "ve": [6, 9], "vecmul": 8, "vector": [1, 3, 6, 7, 10, 13], "verbatim": 7, "verbos": 3, "veri": [0, 2, 4, 6, 7, 8, 9, 11], "verifi": 2, "versa": [1, 3], "version": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "vertic": [2, 5, 8], "vi": 5, "via": 9, "vice": [1, 3], "victor": 0, "view": [5, 6, 7, 9], "virtual": 8, "visibl": 1, "vocabulari": [3, 8], "volum": 11, "w": [1, 6, 8], "wa": [1, 3, 7], "wai": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 11], "want": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "wasn": 9, "we": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "weak": 6, "weaker": [1, 2], "weav": 5, "web": [0, 1, 4], "weight": 5, "weightedaverag": 5, "weird": [6, 9], "weirder": 10, "welcom": [0, 1], "well": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "were": [2, 4, 5, 8, 9], "what": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9], "whatev": [0, 2, 4], "whatsnew": 6, "when": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "whenev": [1, 2, 4, 5, 8], "where": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "wherea": [0, 1, 2, 3, 5, 7, 9], "wherebi": [5, 9], "whether": [2, 3, 4, 6, 9], "which": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "while": [0, 1, 2, 6, 7, 8, 9], "who": [0, 9], "whole": [5, 8], "whose": [1, 2, 4, 5, 6, 7, 8, 9, 10], "why": [0, 2, 4, 6, 7, 8, 9], "wieser": 0, "window": [0, 1, 2, 5], "winston": 0, "wise": [5, 8], "wish": 9, "withbot": 7, "within": [1, 2, 9], "without": [1, 2, 4, 5, 6, 7, 8, 9, 10], "withtop": 10, "wlog": 3, "won": [2, 4, 6, 7, 9], "wonder": 8, "word": [1, 2, 3, 4, 5, 7, 8, 9], "work": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "world": 0, "worri": [1, 3, 4, 5, 7], "worth": [1, 2, 5], "would": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "wouldn": 6, "wrap": [6, 9], "write": [0, 1, 2, 4, 5, 6, 7, 8, 9, 10, 11], "written": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10], "wrong": 3, "wrote": 4, "x": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "x_0": 9, "x_1": [2, 3], "x_2": [2, 3], "x_i": 9, "x_nonneg": 5, "xa": 3, "xai": 3, "xeq": [2, 3], "xgt": 2, "xlt": 2, "xltz": 2, "xmem": 3, "xnt": 3, "xnu": 3, "xpo": 3, "xstu": 3, "xsu": 3, "xt": 3, "xtu": 3, "xu": 3, "xy": [2, 5], "x\u2080": [9, 10], "x\u2081": [2, 3, 5, 9], "x\u2081a": 3, "x\u2082": [2, 3, 5], "x\u2082a": 3, "x\u2082eq": 3, "x\u2082na": 3, "y": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "y_nonneg": 5, "yannick": 0, "yball": 9, "yeq": 2, "yet": [2, 3, 4, 5, 6, 8, 9], "yield": [1, 2, 3, 4, 5, 9], "ylim": 9, "ylt": 2, "you": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "your": [0, 1, 2, 3, 5, 6, 7, 9], "yourself": [2, 5], "ypo": 3, "y\u2080": 9, "y\u2081": 5, "y\u2082": 5, "z": [0, 1, 2, 5, 6, 7, 8, 9, 10, 11], "z_nonneg": 5, "zermelo": 2, "zero": [2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "zero_add": [1, 4, 5, 6], "zero_def": 5, "zero_dvd_iff": 4, "zero_im": 5, "zero_l": [4, 5], "zero_lt_on": [2, 4], "zero_lt_two": 5, "zero_mem": [7, 8], "zero_mul": [1, 4, 5, 6], "zero_r": 5, "zero_smul": 6, "zeroth": 8, "zf": 2, "zlty": 2, "zmod": 7, "zsmul": [5, 6], "zsmulrec": 5, "zsmul\u2081": 6, "zulip": [0, 4], "z\u2080": 9, "z\u2081": 5, "z\u2082": 5, "\u00b9": [1, 3, 5, 6, 7, 8, 9], "\u02e2": 9, "\u03b1": [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "\u03b2": [1, 2, 3, 5, 6, 8, 9, 11], "\u03b3": [1, 2, 5, 9], "\u03b4": [2, 9], "\u03b4po": 9, "\u03b5": [2, 9, 10], "\u03b52po": 2, "\u03b5_po": [9, 10], "\u03b5k_po": 10, "\u03b5po": [2, 9], "\u03b8": 8, "\u03b9": [7, 8, 9, 10, 11], "\u03bc": [9, 11], "\u03bd": 11, "\u03c0": [7, 8, 9, 10], "\u03c3": [5, 7], "\u03c6": [7, 8, 9], "\u03c8": [7, 8], "\u03c9": 7, "\u1d40": 8, "\u1d50": 11, "\u1d65": [7, 8], "\u1d9c": 7, "\u1da0": [9, 10, 11], "\u2080": [3, 8], "\u2081": 6, "\u2090": 7, "\u2097": 8, "\u2102": [1, 5, 7, 8, 10], "\u2115": [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11], "\u211a": [1, 4, 7, 8, 9], "\u211d": [1, 2, 3, 5, 6, 7, 8, 9, 10, 11], "\u2124": [1, 4, 5, 6, 7, 8], "\u2124\u02e3": 7, "\ud835\udcdd": [9, 10, 11], "\ud835\udcdf": 9, "\ud835\udce4": 9, "\ud835\udd42": 10, "\ud835\udd5c": [10, 11], "\ud835\udfd9": 6}, "titles": ["1. Introduction", "2. Basics", "3. Logic", "4. Sets and Functions", "5. Elementary Number Theory", "6. Structures", "7. Hierarchies", "8. Groups and Rings", "9. Linear algebra", "10. Topology", "11. Differential Calculus", "12. Integration and Measure Theory", "Index", "Mathematics in Lean"], "titleterms": {"The": [2, 3], "about": 1, "action": 7, "algebra": [1, 5, 7, 8], "appli": 1, "asymptot": 10, "ball": 9, "base": 8, "basic": [1, 6], "bernstein": 3, "build": 5, "calcul": 1, "calculu": 10, "close": 9, "compact": 9, "comparison": 10, "complet": [8, 9], "concret": 7, "conjunct": 2, "continu": [9, 10], "converg": [2, 9], "countabl": 9, "defin": 5, "differenti": 10, "dimens": 8, "direct": 8, "disjunct": 2, "elementari": [4, 10, 11], "endomorph": 8, "exampl": 1, "existenti": 2, "fact": 1, "filter": 9, "function": [3, 9], "fundament": 9, "gaussian": 5, "get": 0, "group": 7, "hierarchi": 6, "ideal": 7, "ident": 1, "iff": 2, "implic": 2, "index": 12, "induct": 4, "infinit": 4, "integ": 5, "integr": 11, "intern": 8, "introduct": 0, "irrat": 4, "lattic": 8, "lean": 13, "lemma": 1, "linear": [8, 10], "logic": 2, "mani": 4, "map": [8, 10], "mathemat": 13, "matric": 8, "measur": 11, "metric": 9, "monoid": 7, "more": 1, "morphism": [6, 7], "negat": 2, "norm": 10, "number": 4, "object": 6, "open": 9, "overview": 0, "polynomi": 7, "prime": 4, "product": 8, "prove": 1, "pull": 8, "push": 8, "quantifi": 2, "quotient": [7, 8], "recurs": 4, "ring": 7, "root": 4, "rw": 1, "schr\u00f6der": 3, "separ": 9, "sequenc": 2, "set": [3, 8, 9], "space": [8, 9, 10], "span": 8, "start": 0, "structur": [1, 5, 8], "sub": 6, "subgroup": 7, "subr": 7, "subspac": 8, "sum": 8, "theorem": [1, 3], "theori": [4, 11], "topolog": 9, "topologi": 9, "uniformli": 9, "unit": 7, "univers": 2, "us": 1, "vector": 8}})
mathematics_in_lean.pdf