1fade41e - mathematics_in

Authored by: Patrick Massot
Authored at: 2024-08-22 23:04:12 +0200
Committed by: Patrick Massot
Committed at: 2024-08-22 23:04:12 +0200
Object name: 1fade41eebfe761a18596274fdac9192a00e6b07
Parent: 85c2c771

Update jeu. 22 août 2024 23:04:12 CEST

Changes

13 changed files (+22/-22)

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