f3109b5d - mathematics_in

Authored by: Jeremy Avigad
Authored at: 2023-05-29 22:06:46 -0400
Committed by: Jeremy Avigad
Committed at: 2023-05-29 22:06:46 -0400
Object name: f3109b5dd43173b92285c7e2ab6350d5e45b23da
Parent: f78b56ef

Update Mon 29 May 2023 10:06:46 PM EDT

Changes

29 changed files (+265/-190)

html/C01_Introduction.html
- @@ -230,7 +230,8 @@ if <code class="docutils literal notranslate">n</code>
 </pre></div> </div> The proof term can be compressed to a single line: - <div class="highlight-lean notranslate"><div class="highlight"><pre>example : ∀ m n : Nat, Even n → Even (m * n) := fun m n ⟨k, hk⟩ => ⟨m * k, by rw [hk, mul_add]⟩ + <div class="highlight-lean notranslate"><div class="highlight"><pre>example : ∀ m n : Nat, Even n → Even (m * n) := + fun m n ⟨k, hk⟩ => ⟨m * k, by rw [hk, mul_add]⟩ </pre></div> </div> The following is, instead, a tactic-style proof of the same theorem:
html/C02_Basics.html
- @@ -1156,15 +1156,11 @@ are analogous to <code class="docutils literal notranslate">mi
 Since every number divides <code class="docutils literal notranslate">0</code>, <code class="docutils literal notranslate">0</code> is really the greatest element with respect to divisibility: <div class="highlight-lean notranslate"><div class="highlight"><pre>variable (m n : ℕ) - open Nat #check (gcd_zero_right n : gcd n 0 = n) - #check (gcd_zero_left n : gcd 0 n = n) - #check (lcm_zero_right n : lcm n 0 = 0) - #check (lcm_zero_left n : lcm 0 n = 0) </pre></div> </div>
html/C03_Logic.html
- @@ -165,7 +165,8 @@ you are left with new goals that require you to prove
 each of the hypotheses. To prove a statement like this, use the <code class="docutils literal notranslate">intro</code> tactic. Take a look at what it does in this example: - <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem my_lemma3 : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε := by + <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem my_lemma3 : + ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε := by intro x y ε epos ele1 xlt ylt sorry </pre></div>
- @@ -185,7 +186,8 @@ as we did in the last section.
 In a moment, we will see why it is sometimes necessary to introduce variables and hypotheses after the proof begins. To help you prove the lemma, we will start you off: - <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem my_lemma4 : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε := by + <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem my_lemma4 : + ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε := by intro x y ε epos ele1 xlt ylt calc abs (x * y) = abs x * abs y := sorry
- @@ -1538,7 +1540,8 @@ the sequence <code class="docutils literal notranslate">fun</s
 of <code class="docutils literal notranslate">a + b</code>. The following example begins to implement this strategy. See if you can finish it off. - <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem convergesTo_add {s t : ℕ → ℝ} {a b : ℝ} (cs : ConvergesTo s a) (ct : ConvergesTo t b) : + <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem convergesTo_add {s t : ℕ → ℝ} {a b : ℝ} + (cs : ConvergesTo s a) (ct : ConvergesTo t b) : ConvergesTo (fun n => s n + t n) (a + b) := by intro ε εpos dsimp
- @@ -1615,7 +1618,8 @@ and finish the proof.
 If you have made it this far, congratulations! We are now within striking distance of our theorem. The following proof finishes it off. - <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem convergesTo_mul {s t : ℕ → ℝ} {a b : ℝ} (cs : ConvergesTo s a) (ct : ConvergesTo t b) : + <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem convergesTo_mul {s t : ℕ → ℝ} {a b : ℝ} + (cs : ConvergesTo s a) (ct : ConvergesTo t b) : ConvergesTo (fun n => s n * t n) (a * b) := by have h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0 := by apply aux cs
- @@ -1632,7 +1636,8 @@ try filling out the following sketch of a proof that limits
 are unique. (If you are feeling bold, you can delete the proof sketch and try proving it from scratch.) - <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem convergesTo_unique {s : ℕ → ℝ} {a b : ℝ} (sa : ConvergesTo s a) (sb : ConvergesTo s b) : + <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem convergesTo_unique {s : ℕ → ℝ} {a b : ℝ} + (sa : ConvergesTo s a) (sb : ConvergesTo s b) : a = b := by by_contra abne have : abs (a - b) > 0 := by sorry
html/C05_Number_Theory.html
- @@ -283,11 +283,13 @@ factorization of <code class="docutils literal notranslate">n<
 rw [Nat.factorization_mul mnez nnez] rfl - theorem factorization_pow' (n k p : ℕ) : (n ^ k).factorization p = k * n.factorization p := by + theorem factorization_pow' (n k p : ℕ) : + (n ^ k).factorization p = k * n.factorization p := by rw [Nat.factorization_pow] rfl - theorem Nat.Prime.factorization' {p : ℕ} (prime_p : p.Prime) : p.factorization p = 1 := by + theorem Nat.Prime.factorization' {p : ℕ} (prime_p : p.Prime) : + p.factorization p = 1 := by rw [prime_p.factorization] simp </pre></div>
- @@ -308,7 +310,8 @@ of the proof.
 sorry have eq2 : (p * n ^ 2).factorization p = 2 * n.factorization p + 1 := by sorry - have : 2 * m.factorization p % 2 = (2 * n.factorization p + 1) % 2 := by rw [← eq1, sqr_eq, eq2] + have : 2 * m.factorization p % 2 = (2 * n.factorization p + 1) % 2 := by + rw [← eq1, sqr_eq, eq2] rw [add_comm, Nat.add_mul_mod_self_left, Nat.mul_mod_right] at this norm_num at this </pre></div>
- @@ -342,7 +345,8 @@ to finish it off.
 have npow_nz : n ^ k ≠ 0 := fun npowz => nnz (pow_eq_zero npowz) have eq1 : (m ^ k).factorization p = k * m.factorization p := by sorry - have eq2 : (r.succ * n ^ k).factorization p = k * n.factorization p + r.succ.factorization p := by + have eq2 : (r.succ * n ^ k).factorization p = + k * n.factorization p + r.succ.factorization p := by sorry have : r.succ.factorization p = k * m.factorization p - k * n.factorization p := by rw [← eq1, pow_eq, eq2, add_comm, Nat.add_sub_cancel]
- @@ -902,8 +906,9 @@ these methods to prove the two examples below.
 <code class="docutils literal notranslate">n</code> is prime and <code class="docutils literal notranslate">s</code> is a set of primes. To show that, we need the following lemma, which you should be able to prove using the theorem <code class="docutils literal notranslate">Nat.Prime.eq_one_or_self_of_dvd</code>. - <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem Nat.Prime.eq_of_dvd_of_prime {p q : ℕ} (prime_p : Nat.Prime p) (prime_q : Nat.Prime q) - (h : p ∣ q) : p = q := by + <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem Nat.Prime.eq_of_dvd_of_prime {p q : ℕ} + (prime_p : Nat.Prime p) (prime_q : Nat.Prime q) (h : p ∣ q) : + p = q := by sorry </pre></div> </div>
- @@ -931,7 +936,7 @@ and then finish it off.
 linarith [prime_p.two_le] simp [Finset.prod_insert ans, prime_p.dvd_mul] at h₀ h₁ rw [mem_insert] - sorry + sorry </pre></div> </div> We need one last property of finite sets.
- @@ -1095,8 +1100,8 @@ same property.
 apply mod_4_eq_3_or_mod_4_eq_3 rw [neq, h] cases' this with h1 h1 - . sorry - sorry + . sorry + . sorry </pre></div> </div> We are in the home stretch. Given a set <code class="docutils literal notranslate">s</code> of prime
html/C06_Abstract_Algebra.html
- @@ -267,9 +267,12 @@ Then define scalar multiplication for a point and show that it
 distributes over addition. <div class="highlight-lean notranslate"><div class="highlight"><pre>protected theorem add_assoc (a b c : Point) : (a.add b).add c = a.add (b.add c) := by sorry + def smul (r : ℝ) (a : Point) : Point := sorry - theorem smul_distrib (r : ℝ) (a b : Point) : (smul r a).add (smul r b) = smul r (a.add b) := by + + theorem smul_distrib (r : ℝ) (a b : Point) : + (smul r a).add (smul r b) = smul r (a.add b) := by sorry </pre></div> </div>
- @@ -343,8 +346,7 @@ of two points \(a\) and midpoint</code> function above. <div class="highlight-lean notranslate"><div class="highlight"><pre>def weightedAverage (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1) - (a b : StandardTwoSimplex) : StandardTwoSimplex - where + (a b : StandardTwoSimplex) : StandardTwoSimplex := sorry </pre></div> </div>
- @@ -372,7 +374,8 @@ how to sum over it.
 · linarith [a.NonNeg i, b.NonNeg i] norm_num sum_eq_one := by - simp [div_eq_mul_inv, ← Finset.sum_mul, Finset.sum_add_distrib, a.sum_eq_one, b.sum_eq_one] + simp [div_eq_mul_inv, ← Finset.sum_mul, Finset.sum_add_distrib, + a.sum_eq_one, b.sum_eq_one] field_simp end StandardSimplex
- @@ -757,11 +760,12 @@ and define the <code class="docutils literal notranslate">AddG
 def add (a b : Point) : Point := ⟨a.x + b.x, a.y + b.y, a.z + b.z⟩ - def neg (a : point) : point := sorry + def neg (a : Point) : Point := sorry + + def zero : Point := sorry - def zero : point := sorry + def add_group_point : AddGroup₁ point := sorry - def add_group_point : add_group₁ point := sorry end Point </pre></div> </div>
- @@ -1092,7 +1096,8 @@ to use with <code class="docutils literal notranslate">simp</s
 theorem neg_def (x : gaussInt) : -x = ⟨-x.re, -x.im⟩ := rfl - theorem mul_def (x y : gaussInt) : x * y = ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩ := + theorem mul_def (x y : gaussInt) : + x * y = ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩ := rfl </pre></div> </div>
- @@ -1441,9 +1446,11 @@ So we have
 as required. This messy calculation is carried out in the next proof. We encourage you to step through the details and see if you can find a nicer argument. - <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem norm_mod_lt (x : gaussInt) {y : gaussInt} (hy : y ≠ 0) : (x % y).norm < y.norm := by + <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem norm_mod_lt (x : gaussInt) {y : gaussInt} (hy : y ≠ 0) : + (x % y).norm < y.norm := by have norm_y_pos : 0 < norm y := by rwa [norm_pos] - have : x % y * conj y = ⟨Int.mod' (x * conj y).re (norm y), Int.mod' (x * conj y).im (norm y)⟩ := by + have : x % y * conj y = + ⟨Int.mod' (x * conj y).re (norm y), Int.mod' (x * conj y).im (norm y)⟩ := by rw [mod_def, sub_mul, Int.mod'_eq, Int.mod'_eq, sub_eq_add_neg, div_def, norm] ext <;> simp <;> ring have : norm (x % y) * norm y ≤ norm y / 2 * norm y := by
- @@ -1480,7 +1487,8 @@ The second one re-expresses the fact that the norm is decreasing.
 <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem coe_natAbs_norm (x : gaussInt) : (x.norm.natAbs : ℤ) = x.norm := Int.natAbs_of_nonneg (norm_nonneg _) - theorem natAbs_norm_mod_lt (x y : gaussInt) (hy : y ≠ 0) : (x % y).norm.natAbs < y.norm.natAbs := by + 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] apply norm_mod_lt x hy
- @@ -1512,7 +1520,8 @@ and in that case, the required properties are the theorems
 { gaussInt.instCommRing with quotient := (· / ·) remainder := (· % ·) - quotient_mul_add_remainder_eq := fun x y => by simp only; rw [mod_def, add_comm, sub_add_cancel] + quotient_mul_add_remainder_eq := + fun x y => by simp only; rw [mod_def, add_comm, sub_add_cancel] quotient_zero := fun x => by simp [div_def, norm, Int.div'] rfl
html/C07_Topology.html
- @@ -465,9 +465,7 @@ Given <code class="docutils literal notranslate">F <spa
 <li>the condition <code class="docutils literal notranslate">U ∈ F → V ∈ F → U ∩ V ∈ F</code> ensures <code class="docutils literal notranslate">(∀ᶠ x in F, P x) → (∀ᶠ x in F, Q x) → ∀ᶠ x in F, P x ∧ Q x</code>.</li> </ul> <div class="highlight-lean notranslate"><div class="highlight"><pre>#check @eventually_of_forall - #check @Eventually.mono - #check @Eventually.and </pre></div> </div>
- @@ -510,9 +508,7 @@ topology library.
 See if you can prove it using the quoted lemmas, using the fact that <code class="docutils literal notranslate">cluster_pt x F</code> means <code class="docutils literal notranslate">(𝓝 x ⊓ F).ne_bot</code>. <div class="highlight-lean notranslate"><div class="highlight"><pre>#check mem_closure_iff_clusterPt - #check le_principal_iff - #check neBot_of_le example (u : ℕ → ℝ) (M : Set ℝ) (x : ℝ) (hux : Tendsto u atTop (𝓝 x))
- @@ -530,13 +526,9 @@ the function <code class="docutils literal notranslate">fun</s
 <div class="highlight-lean notranslate"><div class="highlight"><pre>variable {X : Type _} [MetricSpace X] (a b c : X) #check (dist a b : ℝ) - #check (dist_nonneg : 0 ≤ dist a b) - #check (dist_eq_zero : dist a b = 0 ↔ a = b) - #check (dist_comm a b : dist a b = dist b a) - #check (dist_triangle a b c : dist a c ≤ dist a b + dist b c) </pre></div> </div>
- @@ -549,11 +541,13 @@ will be explained as part of the calculus chapter.
 Using distance functions, we can already define convergent sequences and continuous functions between metric spaces. They are actually defined in a more general setting covered in the next section, but we have lemmas recasting the definition is terms of distances. - <div class="highlight-lean notranslate"><div class="highlight"><pre>example {u : ℕ → X} {a : X} : Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε := + <div class="highlight-lean notranslate"><div class="highlight"><pre>example {u : ℕ → X} {a : X} : + Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε := Metric.tendsto_atTop example {X Y : Type _} [MetricSpace X] [MetricSpace Y] {f : X → Y} : - Continuous f ↔ ∀ x : X, ∀ ε > 0, ∃ δ > 0, ∀ x', dist x' x < δ → dist (f x') (f x) < ε := + Continuous f ↔ + ∀ x : X, ∀ ε > 0, ∃ δ > 0, ∀ x', dist x' x < δ → dist (f x') (f x) < ε := Metric.continuous_iff </pre></div> </div>
- @@ -670,7 +664,8 @@ but we have lemmas recasting the definition is terms of balls.
 </pre></div> </div> Do the next exercise without using <cite>mem_closure_iff_seq_limit</cite> - <div class="highlight-lean notranslate"><div class="highlight"><pre>example {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a)) {s : Set X} (hs : ∀ n, u n ∈ s) : a ∈ closure s := + <div class="highlight-lean notranslate"><div class="highlight"><pre>example {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a)) {s : Set X} (hs : ∀ n, u n ∈ s) : + a ∈ closure s := sorry </pre></div> </div>
- @@ -709,11 +704,13 @@ are deduced from more general versions, some of which will be discussed in later
 ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (u ∘ φ) atTop (𝓝 a) := hs.tendsto_subseq hu - example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ} (hfs : ContinuousOn f 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 - example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ} (hfs : ContinuousOn f s) : + 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
- @@ -734,7 +731,8 @@ are deduced from more general versions, some of which will be discussed in later
 Again those are defined in a more general context but we have lemmas in the metric name space to access their elementary definitions. We start with uniform continuity. <div class="highlight-lean notranslate"><div class="highlight"><pre>example {X : Type _} [MetricSpace X] {Y : Type _} [MetricSpace Y] {f : X → Y} : - UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : X}, dist a b < δ → dist (f a) (f b) < ε := + UniformContinuous f ↔ + ∀ ε > 0, ∃ δ > 0, ∀ {a b : X}, dist a b < δ → dist (f a) (f b) < ε := Metric.uniformContinuous_iff </pre></div> </div>
- @@ -751,7 +749,8 @@ And <code class="docutils literal notranslate">K</code>
 If <code class="docutils literal notranslate">K</code> is empty then we are clearly done (we can set <code class="docutils literal notranslate">δ = 1</code> for instance). So let’s assume <code class="docutils literal notranslate">K</code> is not empty, and use the extreme value theorem to choose <code class="docutils literal notranslate">(x₀, x₁)</code> attaining the infimum of the distance function on <code class="docutils literal notranslate">K</code>. We can then set <code class="docutils literal notranslate">δ = dist x₀ x₁</code> and check everything works. - <div class="highlight-lean notranslate"><div class="highlight"><pre>example {X : Type _} [MetricSpace X] [CompactSpace X] {Y : Type _} [MetricSpace Y] {f : X → Y} + <div class="highlight-lean notranslate"><div class="highlight"><pre>example {X : Type _} [MetricSpace X] [CompactSpace X] + {Y : Type _} [MetricSpace Y] {f : X → Y} (hf : Continuous f) : UniformContinuous f := sorry </pre></div>
- @@ -763,13 +762,16 @@ of the distance function on <code class="docutils literal notranslate">complete spaces. - <div class="highlight-lean notranslate"><div class="highlight"><pre>example (u : ℕ → X) : CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε := + <div class="highlight-lean notranslate"><div class="highlight"><pre>example (u : ℕ → X) : + CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε := Metric.cauchySeq_iff - example (u : ℕ → X) : CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, dist (u n) (u N) < ε := + example (u : ℕ → X) : + CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, dist (u n) (u N) < ε := Metric.cauchySeq_iff' - example [CompleteSpace X] (u : ℕ → X) (hu : CauchySeq u) : ∃ x, Tendsto u atTop (𝓝 x) := + example [CompleteSpace X] (u : ℕ → X) (hu : CauchySeq u) : + ∃ x, Tendsto u atTop (𝓝 x) := cauchySeq_tendsto_of_complete hu </pre></div> </div>
- @@ -817,18 +819,21 @@ define something inductively in the middle of a proof using <code class="docutil
 intro x rw [mem_closure_iff_nhds_basis nhds_basis_closedBall] intro ε εpos - /- `ε` is positive. We have to find a point in the ball of radius `ε` around `x` belonging to all - `f n`. For this, we construct inductively a sequence `F n = (c n, r n)` such that the closed ball - `closedBall (c n) (r n)` is included in the previous ball and in `f n`, and such that - `r n` is small enough to ensure that `c n` is a Cauchy sequence. Then `c n` converges to a - limit which belongs to all the `f n`. -/ + /- `ε` is positive. We have to find a point in the ball of radius `ε` around `x` + belonging to all `f n`. For this, we construct inductively a sequence + `F n = (c n, r n)` such that the closed ball `closedBall (c n) (r n)` is included + in the previous ball and in `f n`, and such that `r n` is small enough to ensure + that `c n` is a Cauchy sequence. Then `c n` converges to a limit which belongs + to all the `f n`. -/ let F : ℕ → X × ℝ := fun n => - Nat.recOn n (Prod.mk x (min ε (B 0))) fun n p => Prod.mk (center n p.1 p.2) (radius n p.1 p.2) + Nat.recOn n (Prod.mk x (min ε (B 0))) + fun n p => Prod.mk (center n p.1 p.2) (radius n p.1 p.2) let c : ℕ → X := fun n => (F n).1 let r : ℕ → ℝ := fun n => (F n).2 have rpos : ∀ n, 0 < r n := by sorry have rB : ∀ n, r n ≤ B n := by sorry - have incl : ∀ n, closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n := by sorry + have incl : ∀ n, closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n := by + sorry have cdist : ∀ n, dist (c n) (c (n + 1)) ≤ B n := by sorry have : CauchySeq c := cauchySeq_of_le_geometric_two' cdist -- as the sequence `c n` is Cauchy in a complete space, it converges to a limit `y`.
- @@ -867,7 +872,8 @@ has to satisfy a number of axioms presented below (this collection is slightly r
 example {ι : Type _} {s : ι → Set X} (hs : ∀ i, IsOpen <| s i) : IsOpen (⋃ i, s i) := isOpen_iUnion hs - example {ι : Type _} [Fintype ι] {s : ι → Set X} (hs : ∀ i, IsOpen <| s i) : IsOpen (⋂ i, s i) := + example {ι : Type _} [Fintype ι] {s : ι → Set X} (hs : ∀ i, IsOpen <| s i) : + IsOpen (⋂ i, s i) := isOpen_iInter hs </pre></div> </div>
- @@ -1003,8 +1009,10 @@ a function \(g : Y → Z\)
 \[\begin{split}g \text{ continuous } &⇔ g_*(f_*T_X) ≤ T_Z \\ &⇔ (g ∘ f)_* T_X ≤ T_Z \\ &⇔ g ∘ f \text{ continuous}\end{split}\]</div> - <div class="highlight-lean notranslate"><div class="highlight"><pre>example {Z : Type _} (f : X → Y) (T_X : TopologicalSpace X) (T_Z : TopologicalSpace Z) (g : Y → Z) : - @Continuous Y Z (TopologicalSpace.coinduced f T_X) T_Z g ↔ @Continuous X Z T_X T_Z (g ∘ f) := by + <div class="highlight-lean notranslate"><div class="highlight"><pre>example {Z : Type _} (f : X → Y) (T_X : TopologicalSpace X) (T_Z : TopologicalSpace Z) + (g : Y → Z) : + @Continuous Y Z (TopologicalSpace.coinduced f T_X) T_Z g ↔ + @Continuous X Z T_X T_Z (g ∘ f) := by rw [continuous_iff_coinduced_le, coinduced_compose, continuous_iff_coinduced_le] </pre></div> </div>
- @@ -1050,7 +1058,8 @@ neighborhood.
 </pre></div> </div> Note that, in every topological space, each point has a basis of open neighborhood, by definition. - <div class="highlight-lean notranslate"><div class="highlight"><pre>example [TopologicalSpace X] {x : X} : (𝓝 x).HasBasis (fun t : Set X => t ∈ 𝓝 x ∧ IsOpen t) id := + <div class="highlight-lean notranslate"><div class="highlight"><pre>example [TopologicalSpace X] {x : X} : + (𝓝 x).HasBasis (fun t : Set X => t ∈ 𝓝 x ∧ IsOpen t) id := nhds_basis_opens' x </pre></div> </div>
- @@ -1069,8 +1078,9 @@ The assumption “tends to \(x\)<
 <code class="docutils literal notranslate">comap (↑) (𝓝 x)</code>. Let’s prove first an auxiliary lemma, extracted to simplify the context (in particular we don’t need Y to be a topological space here). - <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem aux {X Y A : Type _} [TopologicalSpace X] {c : A → X} {f : A → Y} {x : X} {F : Filter Y} - (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) : + <div class="highlight-lean notranslate"><div class="highlight"><pre>theorem aux {X Y A : Type _} [TopologicalSpace X] {c : A → X} + {f : A → Y} {x : X} {F : Filter Y} + (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) : ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := sorry </pre></div>
- @@ -1112,7 +1122,8 @@ together with the fact that <code class="docutils literal notranslate"><span cla
 space to bring it closer to metric spaces is countability assumption. The main one is first countability asking that every point has a countable neighborhood basic. In particular this ensures that closure of sets can be understood using sequences. - <div class="highlight-lean notranslate"><div class="highlight"><pre>example [TopologicalSpace X] [TopologicalSpace.FirstCountableTopology X] {s : Set X} {a : X} : + <div class="highlight-lean notranslate"><div class="highlight"><pre>example [TopologicalSpace X] [TopologicalSpace.FirstCountableTopology X] + {s : Set X} {a : X} : a ∈ closure s ↔ ∃ u : ℕ → X, (∀ n, u n ∈ s) ∧ Tendsto u atTop (𝓝 a) := mem_closure_iff_seq_limit </pre></div>
- @@ -1132,7 +1143,8 @@ ie such that <code class="docutils literal notranslate">F</spa
 example {F : Filter X} {x : X} : ClusterPt x F ↔ NeBot (𝓝 x ⊓ F) := Iff.rfl - example {s : Set X} : IsCompact s ↔ ∀ (F : Filter X) [NeBot F], F ≤ 𝓟 s → ∃ a ∈ s, ClusterPt a F := + example {s : Set X} : + IsCompact s ↔ ∀ (F : Filter X) [NeBot F], F ≤ 𝓟 s → ∃ a ∈ s, ClusterPt a F := Iff.rfl </pre></div> </div>
html/searchindex.js
- @@ -1,1 +1,1 @@
 - Search.setIndex({"docnames": ["C01_Introduction", "C02_Basics", "C03_Logic", "C04_Sets_and_Functions", "C05_Number_Theory", "C06_Abstract_Algebra", "C07_Topology", "C08_Differential_Calculus", "C09_Integration_and_Measure_Theory", "genindex", "index"], "filenames": ["C01_Introduction.rst", "C02_Basics.rst", "C03_Logic.rst", "C04_Sets_and_Functions.rst", "C05_Number_Theory.rst", "C06_Abstract_Algebra.rst", "C07_Topology.rst", "C08_Differential_Calculus.rst", "C09_Integration_and_Measure_Theory.rst", "genindex.rst", "index.rst"], "titles": ["1. Introduction", "2. Basics", "3. Logic", "4. Sets and Functions", "5. Number Theory", "6. Abstract Algebra", "7. Topology", "Differential Calculus", "Integration and Measure Theory", "Index", "Mathematics in Lean"], "terms": {"The": [0, 1, 4, 5, 6, 10], "goal": [0, 1, 2, 3, 4, 5, 6], "thi": [0, 1, 2, 3, 4, 5, 6, 7], "book": [0, 6], "teach": 0, "you": [0, 1, 2, 3, 4, 5, 6], "formal": [0, 1, 2, 3, 4, 5, 6, 7], "mathemat": [0, 1, 2, 3, 4, 5, 6], "us": [0, 2, 3, 4, 5, 6, 10], "lean": [0, 1, 2, 3, 4, 5, 6], "4": [0, 1, 2, 4, 5, 6], "interact": [0, 5], "proof": [0, 1, 2, 3, 4, 5, 6], "assist": [0, 5], "It": [0, 1, 2, 3, 4, 5, 6], "assum": [0, 1, 2, 3, 4, 6], "know": [0, 1, 2, 3, 4, 5, 6], "some": [0, 1, 2, 3, 4, 5, 6], "doe": [0, 1, 2, 3, 4, 5, 6], "requir": [0, 1, 2, 3, 4, 5, 6], "much": [0, 2, 4, 6, 7], "although": [0, 3, 4, 5, 6], "we": [0, 1, 2, 3, 4, 5, 6, 7], "cover": [0, 1, 3, 6], "exampl": [0, 1, 2, 3, 4, 5, 6], "rang": [0, 2, 3, 4, 6], "from": [0, 1, 2, 3, 4, 5, 6, 7], "number": [0, 1, 2, 3, 5, 6, 7, 10], "theori": [0, 1, 2, 3, 6, 7, 10], "measur": [0, 5, 6, 7], "analysi": [0, 5, 7], "focu": [0, 1, 6], "elementari": [0, 3, 4, 5, 6], "aspect": [0, 5], "those": [0, 1, 2, 3, 5, 6], "field": [0, 1, 5], "hope": 0, "thei": [0, 1, 2, 3, 4, 5, 6], "ar": [0, 1, 2, 3, 4, 5, 6], "familiar": [0, 1, 4, 5, 6, 7], "can": [0, 1, 2, 3, 4, 5, 6], "pick": 0, "them": [0, 1, 2, 3, 4, 5, 6], "up": [0, 2, 3, 4, 5, 6], "go": [0, 1, 2, 3, 4, 6], "also": [0, 1, 2, 3, 4, 5, 6], "don": [0, 1, 2, 3, 4, 5, 6], "t": [0, 1, 2, 3, 4, 5, 6], "presuppos": 0, "ani": [0, 1, 2, 3, 4, 5, 6, 7], "background": 0, "seen": [0, 1, 2, 4, 5, 6], "kind": [0, 1, 6], "comput": [0, 3, 4, 5], "program": [0, 1], "write": [0, 1, 2, 3, 4, 5, 6], "definit": [0, 1, 2, 3, 4, 5, 6], "theorem": [0, 2, 4, 5, 6, 10], "regiment": 0, "languag": [0, 1, 3], "like": [0, 1, 2, 3, 4, 5, 6], "understand": [0, 2, 3, 4, 5, 6], "In": [0, 1, 2, 3, 4, 5, 6, 7], "return": [0, 2, 3, 4, 5, 6], "provid": [0, 1, 2, 3, 4, 5, 6], "feedback": 0, "inform": [0, 1, 2, 3, 5, 6], "interpret": [0, 1, 4, 5, 6], "express": [0, 1, 2, 3, 4, 5, 6], "guarante": [0, 3, 5], "well": [0, 1, 2, 3, 4, 5, 6], "form": [0, 1, 2, 3, 4, 5, 6], "ultim": 0, "certifi": 0, "correct": [0, 1], "our": [0, 1, 2, 3, 4, 5, 6], "learn": [0, 1, 2, 4, 5], "more": [0, 2, 3, 4, 5, 6, 10], "about": [0, 2, 3, 4, 5, 6, 10], "project": [0, 4, 5, 6], "page": [0, 1, 4], "commun": [0, 4], "web": [0, 1, 4], "tutori": 0, "base": [0, 3, 4, 6], "s": [0, 1, 2, 3, 4, 5, 6], "larg": [0, 6], "ever": [0, 6], "grow": 0, "librari": [0, 1, 2, 3, 4, 5, 6], "mathlib": [0, 1, 2, 3, 4, 5, 6], "strongli": 0, "recommend": [0, 1, 3], "take": [0, 1, 2, 3, 4, 5, 6], "look": [0, 1, 2, 3, 4, 6], "zulip": [0, 4], "onlin": 0, "chat": 0, "group": [0, 1, 2, 3, 5, 6], "haven": [0, 2, 6], "alreadi": [0, 1, 2, 3, 4, 5, 6], "ll": [0, 1, 2, 4, 6], "find": [0, 1, 2, 4, 5, 6], "live": [0, 5], "welcom": [0, 1], "enthusiast": 0, "happi": 0, "answer": [0, 5, 6], "question": [0, 4, 6], "offer": [0, 2, 5, 6], "moral": [0, 5], "support": [0, 1, 2, 3, 4, 5, 6], "read": [0, 1, 4, 6], "pdf": 0, "html": 0, "version": [0, 1, 2, 3, 4, 5, 6], "design": [0, 1, 2, 3, 5, 6], "run": 0, "insid": [0, 1, 2, 3], "vs": [0, 1, 2, 3, 5], "code": [0, 1, 2, 3, 5], "editor": [0, 1], "To": [0, 1, 2, 3, 4, 5, 6], "instal": 0, "follow": [0, 1, 2, 3, 4, 5, 6], "instruct": [0, 1, 6], "http": 0, "github": [0, 1], "com": 0, "leanprov": 0, "lean4": 0, "blob": 0, "master": [0, 1, 4], "doc": 0, "quickstart": 0, "md": 0, "_": [0, 1, 2, 3, 4, 5, 6], "termin": 0, "navig": 0, "folder": 0, "where": [0, 1, 2, 3, 4, 5, 6], "want": [0, 1, 2, 3, 4, 5, 6], "put": [0, 1, 2, 3, 4, 5, 6], "copi": [0, 3, 4, 6], "repositori": [0, 1], "type": [0, 1, 2, 3, 4, 5, 6], "git": 0, "clone": 0, "mathematics_in_lean": 0, "fetch": 0, "execut": 0, "lake": 0, "ex": [0, 2], "cach": 0, "compil": 0, "open": [0, 1, 2, 3, 4, 5], "altern": [0, 2, 3, 4, 5, 6], "choos": [0, 2, 3, 4, 5, 6], "file": [0, 1, 4, 5, 6], "menu": [0, 1], "Be": [0, 1, 3], "sure": [0, 1, 2, 3, 5], "other": [0, 1, 2, 3, 4, 5, 6], "simultan": 0, "window": [0, 1, 2, 5], "updat": 0, "newer": 0, "ty": 0, "pull": [0, 6], "cloud": 0, "gitpod": 0, "how": [0, 1, 2, 3, 4, 5, 6], "do": [0, 1, 2, 3, 4, 5, 6], "each": [0, 1, 2, 3, 4, 5, 6], "section": [0, 1, 2, 3, 4, 5, 6], "ha": [0, 1, 2, 3, 4, 5, 6], "an": [0, 1, 2, 3, 4, 5, 6], "associ": [0, 1, 2, 4, 5, 6], "exercis": [0, 1, 2, 3, 5, 6], "src": 0, "organ": 0, "chapter": [0, 1, 2, 3, 4, 5, 6, 7], "make": [0, 1, 2, 3, 4, 5, 6], "so": [0, 1, 2, 3, 4, 5, 6], "experi": [0, 1, 6], "while": [0, 1, 2, 6], "leav": [0, 1, 2, 3, 5], "origin": [0, 1, 5], "intact": 0, "text": [0, 3, 5, 6], "often": [0, 1, 2, 3, 4, 5, 6], "includ": [0, 1, 2, 3, 4, 6], "one": [0, 1, 2, 3, 4, 5, 6], "eval": 0, "hello": 0, "world": 0, "should": [0, 1, 2, 3, 4, 5, 6], "abl": [0, 1, 2, 3, 4, 5], "correspond": [0, 1, 2, 3, 4, 5, 6], "If": [0, 1, 2, 3, 4, 5, 6], "click": [0, 1, 3, 4, 5], "line": [0, 1, 2, 3, 4], "show": [0, 1, 2, 3, 4, 5, 6], "hover": [0, 1, 2, 3, 4, 5], "your": [0, 1, 2, 3, 5, 6], "cursor": [0, 1, 2], "over": [0, 1, 2, 3, 4, 5, 6], "command": [0, 1, 2, 3, 4, 5], "respons": [0, 1], "pop": 0, "encourag": [0, 1, 2, 3, 4, 5], "edit": 0, "try": [0, 1, 2, 3, 4, 5, 6], "own": [0, 1, 4, 5], "moreov": [0, 1, 4, 5, 6], "lot": [0, 3, 5, 6], "challeng": [0, 1, 2, 3, 5], "rush": 0, "past": [0, 1], "just": [0, 1, 2, 3, 4, 5, 6], "work": [0, 1, 2, 3, 4, 5, 6], "through": [0, 1, 3, 4, 5, 6], "central": [0, 4], "alwai": [0, 1, 2, 3, 5], "compar": [0, 5, 6], "solut": [0, 1, 4], "ones": [0, 1, 2, 3, 5], "simpli": [0, 1, 2, 3, 4, 5, 6], "tool": [0, 1, 2, 5], "build": [0, 2, 4, 6, 10], "complex": [0, 1, 2, 4, 5], "known": [0, 1, 2, 3, 4, 5, 6], "depend": [0, 2, 3, 4, 5, 6], "everi": [0, 1, 2, 3, 4, 5, 6], "check": [0, 1, 2, 3, 4, 5, 6], "print": [0, 3, 4, 5], "have": [0, 1, 2, 3, 4, 5, 6], "\u2115": [0, 1, 2, 3, 4, 5, 6], "These": [0, 1, 2, 3, 4, 5], "object": [0, 1, 2, 3, 4, 5], "2": [0, 1, 2, 3, 4, 5, 6], "def": [0, 2, 3, 4, 5, 6], "f": [0, 1, 2, 3, 4, 5, 6], "x": [0, 1, 2, 3, 4, 5, 6], "3": [0, 1, 2, 3, 4, 5, 6], "prop": [0, 2, 3, 4, 5, 6], "statement": [0, 1, 2, 3, 4, 5, 6], "fermatlasttheorem": 0, "y": [0, 1, 2, 3, 4, 5, 6], "z": [0, 1, 2, 5, 6], "n": [0, 1, 2, 3, 4, 5, 6], "0": [0, 1, 2, 3, 4, 5, 6], "p": [0, 2, 3, 4, 5, 6], "itself": [0, 3, 5, 6], "Such": [0, 1, 2], "proposit": [0, 2, 3, 4, 5], "easi": [0, 4, 5, 6], "rfl": [0, 1, 2, 3, 4, 5, 6], "hard": [0, 1, 3, 5], "sorri": [0, 1, 2, 3, 4, 5, 6], "manag": [0, 1, 4, 5, 6], "construct": [0, 2, 3, 4, 5, 6], "fermat_last_theorem": 0, "accept": [0, 1, 6], "term": [0, 1, 2, 3, 4, 5, 6], "done": [0, 2, 3, 4, 6], "someth": [0, 1, 2, 4, 6], "veri": [0, 2, 4, 6], "impress": 0, "cheat": [0, 1], "now": [0, 1, 2, 3, 4, 5, 6, 7], "game": 0, "all": [0, 1, 2, 3, 4, 5, 6], "left": [0, 1, 2, 3, 4, 5, 6], "rule": [0, 2, 4, 5, 6], "complementari": 0, "companion": [0, 1], "prove": [0, 2, 3, 4, 5, 6, 10], "which": [0, 1, 2, 3, 4, 5, 6, 7], "thorough": 0, "underli": [0, 1, 5], "logic": [0, 1, 3, 4, 5, 10], "framework": 0, "core": [0, 4, 5], "syntax": [0, 1, 3, 4], "peopl": [0, 1], "who": [0, 6], "prefer": [0, 1, 3], "user": [0, 2], "manual": [0, 3, 4], "befor": [0, 1, 2, 3, 4, 5], "new": [0, 1, 2, 3, 4, 5, 6], "dishwash": 0, "person": 0, "hit": [0, 1], "button": [0, 1], "figur": [0, 1, 2, 5], "out": [0, 1, 2, 3, 4, 5, 6], "activ": 0, "potscrubb": 0, "featur": [0, 1, 2, 4], "later": [0, 1, 2, 4, 5, 6], "sens": [0, 2, 3, 4, 5, 6], "here": [0, 1, 2, 3, 4, 5, 6], "refer": [0, 1, 2, 4, 5, 6], "back": [0, 1, 2, 3, 5, 6], "necessari": [0, 2, 4, 5], "anoth": [0, 1, 2, 3, 4, 5, 6], "thing": [0, 1, 2, 3, 4, 5, 6], "distinguish": [0, 5, 6], "place": [0, 1, 2, 5, 6], "greater": [0, 1, 2, 3, 4, 6], "emphasi": 0, "tactic": [0, 1, 2, 3, 4, 5, 6], "given": [0, 1, 2, 3, 4, 5, 6], "two": [0, 1, 2, 3, 4, 5, 6], "wai": [0, 1, 2, 3, 4, 5, 6], "down": [0, 3, 4, 6], "themselv": [0, 4, 5], "suitabl": [0, 1, 2, 5, 6], "descript": [0, 1, 2, 4, 6], "thereof": 0, "For": [0, 1, 2, 3, 4, 5, 6], "repres": [0, 1, 2, 3, 4, 5], "fact": [0, 2, 3, 4, 5, 6, 10], "even": [0, 1, 2, 3, 4, 5, 6], "m": [0, 1, 2, 4, 6], "nat": [0, 1, 2, 3, 4, 5, 6], "fun": [0, 2, 3, 4, 5, 6], "k": [0, 2, 4, 5, 6], "hk": 0, "hmn": 0, "rw": [0, 1, 2, 3, 4, 5, 6], "mul_add": [0, 1, 4], "l": [0, 1], "compress": [0, 1, 6], "singl": [0, 1, 2, 3, 4, 5], "instead": [0, 1, 2, 3, 4, 5, 6], "style": [0, 1], "same": [0, 1, 2, 3, 4, 5, 6], "sai": [0, 1, 2, 3, 4, 5, 6], "natur": [0, 1, 2, 3, 4, 5, 6], "rintro": [0, 2, 3, 4, 5, 6], "need": [0, 1, 2, 3, 4, 5, 6], "twice": [0, 6], "let": [0, 1, 2, 3, 4, 5, 6], "substitut": [0, 2], "obviou": [0, 4, 5], "ring": [0, 1, 2, 3, 4, 5], "As": [0, 1, 2, 3, 4, 5, 6], "enter": [0, 1, 2, 3, 6], "displai": [0, 1, 2], "state": [0, 1, 2, 3, 4, 6], "separ": [0, 1, 2, 4, 5], "tell": [0, 2, 3, 4, 5], "what": [0, 1, 2, 3, 4, 5, 6], "establish": [0, 1, 2, 3, 4, 5], "task": [0, 2, 4, 5, 6], "remain": [0, 1, 2, 3, 5, 6], "replai": 0, "step": [0, 1, 2, 3, 4, 5], "sinc": [0, 1, 2, 3, 4, 5, 6], "continu": [0, 1, 4, 5], "point": [0, 1, 2, 3, 5, 6], "see": [0, 1, 2, 3, 4, 5, 6], "first": [0, 1, 2, 3, 4, 5, 6], "introduc": [0, 1, 2, 3, 4, 6], "could": [0, 1, 2, 4, 5, 6], "renam": 0, "decompos": [0, 3, 5], "hypothesi": [0, 1, 2, 3, 4], "assumpt": [0, 1, 2, 3, 4, 5, 6], "second": [0, 1, 2, 3, 4, 5, 6], "declar": [0, 1, 4, 5], "next": [0, 1, 2, 3, 4, 5, 6, 7], "rewrit": [0, 1, 2, 3, 4, 5, 6], "replac": [0, 1, 2, 3, 4], "solv": [0, 1, 2, 3, 4, 5, 6], "result": [0, 1, 2, 3, 4, 5, 6], "abil": 0, "small": [0, 4, 5, 6], "increment": [0, 1], "extrem": [0, 6], "power": [0, 2, 3, 4, 5], "reason": [0, 1, 2, 4, 5, 6], "easier": [0, 1, 3, 4, 6], "quicker": 0, "than": [0, 1, 2, 3, 4, 5, 6], "There": [0, 1, 2, 3, 4, 6], "isn": [0, 2, 3, 4], "sharp": 0, "distinct": [0, 2, 3, 4, 5, 6], "between": [0, 1, 2, 3, 4, 5, 6], "insert": [0, 2, 4, 5, 6], "did": [0, 2, 6], "phrase": [0, 1, 2, 4, 5], "mul_left_comm": [0, 4], "abov": [0, 1, 2, 3, 4, 5, 6], "convers": [0, 1, 2, 4, 6], "short": [0, 1, 2, 3, 4, 5], "middl": [0, 1, 2, 6], "That": [0, 4, 5], "said": [0, 2, 4, 5], "reduc": [0, 2, 3, 4, 5], "liner": 0, "carri": [0, 1, 2, 3, 4, 5, 6], "But": [0, 1, 2, 3, 4, 5, 6], "substanti": 0, "autom": [0, 1, 5], "justifi": [0, 1, 2, 6], "longer": [0, 4, 5], "calcul": [0, 2, 4, 5, 10], "bigger": [0, 3], "inferenti": 0, "invok": [0, 1, 6], "simplifi": [0, 2, 3, 4, 5, 6], "specif": [0, 1, 3, 4, 5], "pariti": [0, 4], "automat": [0, 1, 2, 3, 4, 5, 6], "intro": [0, 1, 2, 3, 4, 5, 6], "simp": [0, 2, 3, 4, 5, 6], "parity_simp": 0, "big": [0, 5, 6], "differ": [0, 1, 2, 3, 4, 5, 6], "onli": [0, 1, 2, 3, 4, 5, 6], "its": [0, 1, 2, 3, 4, 5, 6], "built": [0, 2], "wherea": [0, 1, 3, 5, 6], "top": [0, 6], "meant": [0, 1, 2], "contain": [0, 2, 3, 4, 5, 6], "extens": [0, 1, 6], "document": [0, 1, 3, 4], "rather": [0, 1, 2, 4, 5, 6], "think": [0, 1, 2, 3, 4, 5, 6], "comfort": [0, 2], "brows": [0, 1, 4], "frustrat": 0, "curv": 0, "steep": 0, "newcom": 0, "avail": [0, 4, 5], "round": [0, 1, 5], "clock": 0, "doubt": 0, "soon": [0, 2, 6], "enough": [0, 1, 2, 3, 4, 6], "too": [0, 1, 3, 5, 6], "contribut": [0, 3], "develop": [0, 1, 4], "mission": 0, "dive": 0, "come": [0, 1, 2, 3, 4, 5, 6], "forewarn": 0, "fundament": [0, 4, 5], "life": [0, 2], "mai": [0, 1, 2, 3, 5, 6], "never": 0, "acknowledg": 0, "grate": [0, 5], "gabriel": 0, "ebner": 0, "set": [0, 1, 2, 4, 5, 7, 10], "infrastructur": 0, "scott": 0, "morrison": 0, "mario": 0, "carneiro": 0, "help": [0, 1, 2, 3, 4, 5, 6], "port": 0, "bryan": 0, "gin": 0, "ge": [0, 2, 5], "chen": 0, "johan": 0, "commelin": 0, "mathieu": 0, "guai": 0, "paquet": 0, "julian": 0, "k\u00fclshammer": 0, "giovanni": 0, "mascellani": 0, "hunter": 0, "monro": 0, "pietro": 0, "monticon": 0, "bartosz": 0, "piotrowski": 0, "guilherm": 0, "silva": 0, "been": [0, 1, 2, 4, 5], "partial": [0, 1, 2, 3, 5], "hoskinson": 0, "center": [0, 6], "nut": 1, "bolt": 1, "appli": [1, 2, 3, 4, 5, 6], "gener": [1, 2, 3, 4, 5, 6], "without": [1, 2, 4, 5, 6], "when": [1, 2, 3, 4, 5, 6], "net": 1, "hand": [1, 2, 3, 4, 5, 6], "side": [1, 2, 3, 4, 5, 6], "equal": [1, 2, 3, 4, 5, 6], "right": [1, 2, 3, 4, 5, 6], "tantamount": [1, 3], "name": [1, 2, 3, 4, 5, 6], "abbrevi": [1, 2, 3, 5], "b": [1, 2, 3, 4, 5, 6], "c": [1, 2, 4, 5, 6], "real": [1, 2, 3, 4, 5, 6, 7], "mul_assoc": [1, 2, 4, 5], "mul_comm": [1, 2, 4, 5], "elimin": 1, "explicitli": [1, 2, 3, 5, 6], "purpos": [1, 2, 3, 4, 5, 6], "illustr": [1, 2, 3, 4, 5], "multipl": [1, 2, 3, 4, 5], "written": [1, 2, 3, 4, 5, 6], "howev": [1, 2, 5, 6], "good": [1, 2, 3, 4, 5, 6], "mind": [1, 2, 5], "notat": [1, 2, 3, 4, 5, 6], "convent": [1, 5], "parenthes": [1, 2, 3, 4], "\u211d": [1, 2, 3, 5, 6], "import": [1, 2, 3, 4, 5, 6], "begin": [1, 2, 3, 4, 5], "sake": [1, 4], "breviti": [1, 5], "suppress": 1, "repeat": [1, 4, 5], "full": [1, 3, 4, 5, 6], "process": [1, 3], "chang": [1, 2, 4, 5, 6], "happen": [1, 6], "charact": [1, 3], "r": [1, 2, 4, 5, 6], "symbol": [1, 2, 5], "doesn": [1, 2, 6], "appear": [1, 2, 5, 6], "until": [1, 2, 4, 5, 6], "space": [1, 3, 5, 10], "tab": [1, 2, 3, 4], "kei": [1, 4, 5, 6], "keyboard": 1, "easili": [1, 4, 5], "access": [1, 3, 5, 6], "backslash": [1, 3], "lead": [1, 2, 4, 5, 6], "input": [1, 3, 6], "leader": 1, "report": 1, "current": [1, 2], "infoview": 1, "move": [1, 2, 6], "A": [1, 2, 3, 4, 5, 6], "typic": 1, "might": [1, 2, 3, 4, 5], "1": [1, 2, 3, 4, 5, 6], "h\u2081": [1, 2, 3, 4], "prime": [1, 2, 3, 5, 10], "h\u2082": [1, 3, 4], "h\u2083": [1, 3], "denot": [1, 3, 4, 6], "context": [1, 2, 4, 5, 6], "plai": [1, 3, 4, 6], "three": [1, 2, 4, 5, 6], "label": [1, 2], "everyth": [1, 2, 6], "identifi": [1, 2, 4], "subscript": 1, "h": [1, 2, 3, 4, 5, 6], "legal": 1, "would": [1, 2, 3, 4, 5, 6], "h1": [1, 3, 4], "h2": [1, 3], "h3": 1, "foo": [1, 3, 5], "bar": [1, 2], "baz": 1, "last": [1, 2, 3, 4, 5, 6], "sometim": [1, 2, 3, 4, 5, 6], "target": [1, 6], "combin": [1, 2, 5, 6], "practic": [1, 2, 3, 6], "intend": [1, 2, 5], "mean": [1, 2, 3, 4, 5, 6], "usual": [1, 2, 3, 4, 5, 6], "clear": [1, 2, 4, 5], "case": [1, 2, 3, 4, 5, 6], "With": [1, 3, 4, 6], "arrow": [1, 2, 6], "revers": [1, 2, 3, 5, 6], "argument": [1, 2, 3, 4, 5, 6], "tri": [1, 2, 4], "match": [1, 2, 5], "pattern": [1, 2, 3, 5], "local": [1, 2, 6], "d": [1, 2, 4, 5], "e": [1, 2, 3, 4, 5, 6], "hyp": 1, "sub_self": [1, 2], "list": [1, 2, 3, 4, 5], "relev": [1, 2, 4, 5, 6], "within": [1, 2, 6], "squar": [1, 2, 4, 5], "bracket": [1, 2, 5], "still": [1, 2, 3, 4, 5, 6], "progress": [1, 5], "after": [1, 2, 4, 6], "comma": 1, "trick": [1, 2, 4], "variabl": [1, 2, 3, 4, 5, 6], "onc": [1, 2, 3, 4, 5, 6], "outsid": [1, 4], "mention": [1, 2, 3, 5, 6], "g": [1, 2, 3, 5, 6], "inspect": 1, "reveal": 1, "inde": [1, 5, 6], "delimit": 1, "scope": [1, 2, 3, 5], "end": [1, 2, 3, 4, 5, 6], "block": [1, 4], "final": [1, 2, 3, 5, 6], "recal": [1, 2, 4, 5, 6], "introduct": [1, 2, 6, 10], "determin": [1, 5, 6], "both": [1, 2, 3, 4, 5, 6], "expect": [1, 2, 3, 4, 5, 6], "rais": [1, 4], "error": [1, 2, 3], "explain": [1, 2, 3, 4, 5, 6], "output": 1, "meanwhil": [1, 4], "two_mul": [1, 5], "add_mul": 1, "distribut": [1, 4, 5], "addit": [1, 2, 4, 5, 6], "add_assoc": [1, 4, 5], "precis": [1, 3, 6], "possibl": [1, 2, 3, 4, 5, 6], "calc": [1, 2, 3, 6], "keyword": [1, 2, 4, 5], "notic": [1, 2, 3, 4, 5, 6], "finicki": 1, "dot": [1, 6], "underscir": 1, "justif": [1, 2], "format": 1, "indic": [1, 2, 3, 5], "indent": 1, "One": [1, 2, 3, 4, 5, 6], "outlin": [1, 2, 4, 6], "modulo": [1, 4, 5], "individu": 1, "pure": [1, 6], "littl": [1, 2, 6], "underneath": [1, 3], "pow_two": [1, 4, 5], "mul_sub": 1, "add_sub": 1, "sub_sub": 1, "add_zero": [1, 5], "perform": [1, 2, 3], "exact": [1, 2, 3, 4, 5, 6], "becaus": [1, 2, 3, 4, 5, 6], "exactli": [1, 2, 3, 5, 6], "close": [1, 2, 3], "note": [1, 2, 4, 5, 6], "bit": [1, 4, 6], "commut": [1, 2, 3, 4, 5], "indirectli": 1, "data": [1, 2, 4, 5, 6], "similar": [1, 2, 3, 5, 6], "common": [1, 2, 3, 4, 5, 6], "variat": [1, 3, 4, 5, 6], "call": [1, 2, 3, 4, 5, 6], "nth_rewrit": 1, "allow": [1, 2, 3, 4, 5, 6], "particular": [1, 2, 5, 6], "instanc": [1, 2, 3, 4, 5, 6], "enumer": [1, 2], "start": [1, 2, 3, 4, 6, 7, 10], "zero": [1, 2, 3, 4, 5, 6], "occurr": 1, "nth_rw": 1, "nth_rewrite_lh": 1, "nth_rewrite_rh": 1, "sophist": [1, 6], "subexpress": 1, "consist": [1, 3, 5, 6], "collect": [1, 3, 5, 6], "oper": [1, 2, 3, 4, 5, 6], "time": [1, 4, 5, 6], "constant": [1, 2], "mapsto": [1, 5], "abelian": [1, 5], "negat": [1, 5, 10], "invers": [1, 3, 5], "axiom": [1, 3, 5, 6], "add_comm": [1, 4, 5], "zero_add": [1, 4, 5], "add_left_neg": [1, 5], "mul_on": [1, 5], "one_mul": [1, 2, 5], "being": [1, 3, 5, 6], "suffic": [1, 2, 3, 6], "give": [1, 2, 3, 4, 6], "element": [1, 2, 3, 4, 5, 6], "concret": [1, 2, 4, 5, 6], "integ": [1, 2, 4, 10], "abstract": [1, 2, 6, 10], "character": [1, 3, 4, 6], "axiomat": [1, 2, 3, 5], "train": 1, "recogn": [1, 2, 4, 5, 6], "appropri": [1, 2, 3, 5], "\u2124": [1, 4, 5], "ration": [1, 2, 4, 6], "\u211a": [1, 4, 6], "\u2102": [1, 5], "extend": [1, 3, 4, 5, 6], "Not": [1, 5, 6], "properti": [1, 2, 3, 4, 5, 6], "hold": [1, 2, 3, 4, 5, 6], "arbitrari": [1, 2, 3, 4, 5], "taken": [1, 2], "cours": [1, 2, 4, 6], "linear": [1, 2, 5, 6], "matric": [1, 5], "fail": [1, 2, 3, 4, 5, 6], "commr": [1, 2, 5], "unchang": [1, 2], "linarith": [1, 2, 4, 5], "permiss": 1, "strike": [1, 2], "balanc": 1, "concis": [1, 5], "readabl": [1, 2, 3, 4, 6], "strengthen": [1, 2, 4], "skill": [1, 2, 3, 4], "deriv": [1, 2, 4, 7], "most": [1, 2, 3, 4, 5, 6], "content": [1, 4, 6], "organiz": 1, "mechan": [1, 2, 5], "namespac": [1, 2, 3, 4, 5, 6], "shorter": [1, 3, 4, 6], "avoid": [1, 3, 4, 5], "due": [1, 3], "clash": 1, "myre": 1, "add_right_neg": 1, "effect": [1, 3, 6], "temporarili": [1, 2], "reprov": 1, "care": [1, 2, 3, 5], "earlier": 1, "pai": [1, 2, 6], "attent": [1, 2, 4, 6], "curli": [1, 2], "implicit": [1, 2, 5, 6], "moment": [1, 2, 5], "worri": [1, 3, 4, 5], "neg_add_cancel_left": 1, "add_neg_cancel_right": 1, "add_left_cancel": 1, "add_right_cancel": 1, "plan": [1, 6], "brace": 1, "imagin": 1, "situat": [1, 3, 6], "draw": [1, 5], "conclus": [1, 2, 4], "hypothes": [1, 2, 3, 4, 5], "redund": [1, 5, 6], "few": [1, 2, 3, 4, 6], "extra": [1, 2, 3, 5, 6], "oner": 1, "complic": [1, 2], "tediou": [1, 2], "mark": [1, 2, 6], "suppos": [1, 2, 3, 4, 5, 6], "infer": [1, 2, 3, 5], "mul_zero": [1, 5], "serv": [1, 3, 4, 5], "therefor": [1, 4, 5, 6], "promot": 1, "modular": 1, "subproof": 1, "wa": [1, 3], "except": [1, 5], "ad": [1, 2, 3, 4, 5, 6], "free": [1, 6], "At": [1, 2, 4, 5], "rememb": [1, 2, 3, 4, 5, 6], "zero_mul": [1, 2, 4, 5], "By": [1, 3, 5], "neg_eq_of_add_eq_zero": 1, "eq_neg_of_add_eq_zero": 1, "neg_zero": 1, "neg_neg": 1, "had": 1, "annot": [1, 3, 4, 5], "third": [1, 2, 3, 5, 6], "specifi": [1, 2, 3, 4, 5, 6], "imposs": 1, "default": [1, 2, 3, 4, 5], "subtract": [1, 4, 5], "provabl": [1, 3, 6], "sub_eq_add_neg": [1, 5], "On": [1, 2, 3, 5, 6], "defin": [1, 2, 3, 4, 5, 6], "reflex": [1, 2], "present": [1, 2, 4, 6], "forc": [1, 2, 3], "unfold": [1, 2, 3, 4, 5, 6], "refl": [1, 2, 3, 5], "deal": [1, 2, 3, 4, 5, 6], "equat": [1, 2, 3, 4, 5], "interchang": 1, "self_sub": 1, "either": [1, 2, 3, 5, 6], "effort": [1, 4], "one_add_one_eq_two": 1, "norm_num": [1, 2, 4, 5], "strength": 1, "weaker": [1, 2], "notion": [1, 2, 3, 4, 5, 6, 7], "addgroup": 1, "otherwis": [1, 2, 3, 4, 5], "variant": [1, 2, 6], "addcommgroup": 1, "commgroup": 1, "mul_left_inv": [1, 5], "\u00b9": [1, 3, 5, 6], "feel": [1, 2, 6], "cocki": 1, "helper": 1, "along": [1, 4, 6], "hint": [1, 2], "mul_right_inv": [1, 5], "mul_inv_rev": 1, "non": [1, 3, 6], "abel": 1, "noncomm_r": 1, "seem": [1, 2, 4, 6], "odd": [1, 2, 3, 4], "partli": 1, "histor": 1, "conveni": [1, 2, 3, 5, 6], "great": [1, 5], "sort": [1, 3, 4], "inequ": [1, 2, 6], "le": [1, 5], "whenev": [1, 2, 4, 5], "consid": [1, 2, 3, 4, 5, 6, 7], "le_refl": [1, 2], "le_tran": [1, 2, 5], "detail": [1, 2, 3, 4, 5], "unless": [1, 2, 5], "realli": [1, 2, 3, 4, 6], "insist": 1, "discuss": [1, 2, 4, 5, 6], "implic": [1, 6, 10], "h\u2080": [1, 2, 3, 4, 6], "creat": 1, "option": [1, 2, 4, 5, 6], "visibl": 1, "must": [1, 5, 6], "complet": [1, 2, 3, 4], "decreas": [1, 5], "fourth": [1, 2], "mode": [1, 2, 5], "entir": [1, 3, 5, 6], "lt_of_le_of_lt": [1, 2, 5], "lt_of_lt_of_l": 1, "lt_tran": [1, 2], "togeth": [1, 2, 3, 4, 5, 6], "handl": [1, 3, 4], "arithmet": 1, "5": [1, 2, 5, 6], "pass": [1, 5], "exp_le_exp": 1, "mpr": [1, 2, 5, 6], "exp": [1, 3], "applic": [1, 2, 4, 5], "function": [1, 2, 4, 5, 7, 10], "compound": [1, 2, 6], "pars": [1, 3], "exp_lt_exp": 1, "log_le_log": 1, "log": [1, 3], "log_lt_log": 1, "add_le_add": [1, 2, 5], "add_le_add_left": 1, "add_le_add_right": 1, "add_lt_add_of_le_of_lt": 1, "add_lt_add_of_lt_of_l": 1, "add_lt_add_left": 1, "add_lt_add_right": 1, "add_nonneg": [1, 5], "add_po": 1, "add_pos_of_pos_of_nonneg": 1, "exp_po": [1, 3], "bi": [1, 5, 10], "lr": 1, "iff": [1, 3, 6], "connect": [1, 3, 5, 6], "equival": [1, 2, 3, 4, 5, 6], "mp": [1, 2, 3, 4, 6], "forward": [1, 2, 5, 6], "direct": [1, 2, 3, 6], "stand": [1, 2, 5, 6], "modu": 1, "ponen": 1, "respect": [1, 2, 3, 4, 5, 6], "thu": [1, 3, 4, 5, 6], "again": [1, 2, 3, 4, 5, 6], "numer": [1, 4, 5], "constitut": 1, "part": [1, 2, 3, 4, 5, 6], "strategi": [1, 2, 4], "api": 1, "reli": [1, 2, 3, 5, 6], "guess": [1, 2, 3, 4, 5], "a_of_b_of_c": 1, "approxim": 1, "loud": 1, "probabl": [1, 5, 6], "add_l": 1, "choic": [1, 2, 3, 5, 6], "exist": [1, 2, 3, 6], "jump": [1, 4, 5, 6], "nearbi": [1, 4], "library_search": [1, 4], "sq_nonneg": 1, "delet": [1, 2, 3, 4], "uncom": 1, "previou": [1, 2, 3, 5, 6], "suggest": [1, 2, 4, 5, 6], "long": [1, 2, 3, 5], "better": [1, 3, 4, 5, 6], "confirm": [1, 2, 3, 4], "finish": [1, 2, 3, 4], "job": 1, "pow_two_nonneg": [1, 2], "tend": [1, 6], "around": [1, 3, 6], "binari": [1, 2, 4, 5], "increas": 1, "worth": [1, 2, 5], "definition": [1, 4, 5, 6], "principl": [1, 2, 3, 4], "favor": [1, 2, 5], "timesav": 1, "clever": 1, "involv": [1, 2, 4, 5, 6], "nice": [1, 2, 4, 6], "idea": [1, 2, 3, 5, 6], "abs_l": [1, 5], "ab": [1, 2, 5], "congratul": [1, 2, 4], "becom": [1, 4, 5, 6], "min": [1, 2, 6], "uniqu": [1, 2, 3, 4, 5, 6], "min_le_left": 1, "min_le_right": 1, "le_min": 1, "max": [1, 2, 6], "pair": [1, 2, 4, 5, 6], "act": 1, "curri": 1, "logician": 1, "haskel": 1, "get": [1, 2, 3, 4, 6, 10], "bind": [1, 3], "tighter": [1, 3], "infix": 1, "le_antisymm": [1, 2], "less": [1, 2, 3, 4, 5, 6], "usag": 1, "inconsist": 1, "outer": 1, "level": [1, 2], "nest": [1, 2], "maintain": 1, "bother": [1, 3], "repetit": 1, "foreshadow": 1, "univers": [1, 3, 5, 6, 10], "quantifi": [1, 3, 4, 5, 6, 10], "desir": [1, 3, 6], "implicitli": [1, 2], "mani": [1, 2, 3, 5, 6, 10], "whether": [1, 2, 3, 4, 6], "Of": [1, 2, 4, 6], "interest": [1, 2, 3, 5, 6], "vice": [1, 3], "versa": [1, 3], "word": [1, 2, 3, 4, 5, 6], "switch": 1, "transit": [1, 2, 5, 6], "total": 1, "satisfi": [1, 3, 4, 5, 6], "disjunct": [1, 3, 10], "stick": [1, 2, 6, 7], "split": [1, 2, 3, 4], "aux": [1, 2, 4, 6], "valu": [1, 2, 3, 4, 5, 6], "yield": [1, 2, 3, 4, 5, 6], "made": [1, 2, 3, 5, 6], "manifest": [1, 6], "triangl": [1, 2, 5], "abs_add": [1, 2], "sub_add_cancel": [1, 5], "relat": [1, 2, 3, 5, 6], "ordinari": [1, 2, 4, 5, 6], "unicod": [1, 3], "obtain": [1, 2, 4, 5, 6], "dvd": 1, "dvd_tran": 1, "dvd_mul_of_dvd_left": 1, "dvd_mul_left": 1, "expon": 1, "expand": [1, 2, 3, 4, 5], "w": 1, "greatest": [1, 5, 6], "divisor": [1, 2, 4, 5], "gcd": [1, 2, 4], "least": [1, 5, 6], "lcm": 1, "analog": [1, 2, 3, 4, 5, 6], "divid": [1, 2, 4, 5], "gcd_zero_right": 1, "gcd_zero_left": 1, "lcm_zero_right": 1, "lcm_zero_left": 1, "similarli": [1, 2, 3, 4, 5], "prefix": [1, 4], "dvd_antisymm": 1, "complain": 1, "ambigu": [1, 5], "_root_": 1, "saw": [1, 5, 6], "govern": [1, 5], "class": [1, 4, 5, 6, 7], "describ": [1, 2, 3, 4, 5, 6], "\u03b1": [1, 2, 3, 4, 5, 6], "partialord": [1, 2], "adopt": 1, "letter": [1, 5], "\u03b2": [1, 2, 3, 5, 6], "\u03b3": [1, 2, 5, 6], "greek": [1, 4], "especi": [1, 5, 6], "strict": [1, 2], "somewhat": [1, 3, 6], "lt_irrefl": [1, 2], "lt_iff_le_and_n": 1, "lattic": [1, 5, 6], "inf_le_left": [1, 6], "inf_le_right": 1, "le_inf": 1, "le_sup_left": 1, "le_sup_right": 1, "sup_l": 1, "lower": [1, 2, 4], "bound": [1, 2, 3, 4, 5, 6], "upper": [1, 2], "glb": 1, "lub": 1, "infimum": [1, 6], "supremum": [1, 4], "inf": [1, 6], "sup": [1, 4, 6], "further": [1, 6], "matter": [1, 2], "meet": [1, 2, 3, 5], "join": [1, 5], "keep": [1, 5], "dictionari": 1, "subset": [1, 2, 3, 5, 6], "domain": [1, 2, 3, 4, 5, 6], "boolean": 1, "truth": [1, 4], "fals": [1, 2, 3, 4], "true": [1, 2, 3, 6], "posit": [1, 3, 4, 5, 6], "subspac": 1, "vector": [1, 3], "intersect": [1, 3, 5, 6], "sum": [1, 2, 4, 5, 6], "inclus": [1, 3, 6], "topolog": [1, 5, 10], "union": [1, 3, 4, 5], "inf_comm": 1, "inf_assoc": 1, "sup_comm": 1, "sup_assoc": 1, "absorpt": 1, "law": 1, "absorb1": 1, "absorb2": 1, "found": [1, 5], "inf_sup_self": 1, "sup_inf_self": 1, "distriblattic": 1, "inf_sup_left": 1, "inf_sup_right": 1, "sup_inf_left": 1, "sup_inf_right": 1, "shown": [1, 5], "explicit": [1, 2, 5, 6], "nondistribut": 1, "finit": [1, 3, 4, 5, 6], "impli": [1, 2, 3, 4, 5, 6], "larger": [1, 6], "carrier": [1, 5], "compat": [1, 6], "strictorderedr": 1, "mul_po": [1, 4], "mul_nonneg": 1, "coupl": [1, 2, 6], "metric": [1, 5, 10], "equip": [1, 3, 5, 6], "distanc": [1, 2, 6], "dist": [1, 6], "map": [1, 2, 3, 5, 6], "metricspac": [1, 6], "dist_self": 1, "dist_comm": [1, 6], "dist_triangl": [1, 6], "nonneg": [1, 5], "nonneg_of_mul_nonneg_left": 1, "dist_nonneg": [1, 6], "dealt": 2, "basic": [2, 4, 5, 6, 10], "simpl": [2, 4, 5], "absolut": 2, "\u03b5": [2, 6], "though": [2, 3, 4, 5], "treat": [2, 3, 5, 6], "my_lemma": 2, "\u03b4": [2, 6], "hb": [2, 6], "subsequ": [2, 4, 6], "lemma": [2, 4, 5, 6, 10], "my_lemma2": 2, "stage": [2, 5], "my_lemma3": 2, "epo": 2, "ele1": 2, "xlt": 2, "ylt": 2, "essenti": [2, 3, 5, 6], "colon": 2, "why": [2, 4, 6], "off": [2, 3, 4], "my_lemma4": 2, "abs_mul": 2, "mul_le_mul": 2, "abs_nonneg": 2, "mul_lt_mul_right": 2, "extract": [2, 6], "hidden": 2, "expos": [2, 6], "predic": [2, 3, 4, 6], "fn_ub": 2, "fn_lb": 2, "fnub": 2, "fnlb": 2, "hfa": 2, "hgb": 2, "dsimp": [2, 3, 4, 5], "simplif": [2, 3, 4], "contract": 2, "anyhow": 2, "control": 2, "transform": [2, 3], "rest": [2, 3, 5, 6], "routin": 2, "nnf": 2, "nng": 2, "hfb": 2, "nna": 2, "order": [2, 3, 4, 5, 6, 10], "codomain": [2, 4, 6], "structur": [2, 4, 6, 10], "monoid": [2, 3, 4], "fn_ub_add": 2, "orderedcanceladdcommmonoid": 2, "high": 2, "monoton": [2, 6], "nondecreas": [2, 4], "placehold": 2, "Or": [2, 3], "backward": [2, 6], "subgoal": 2, "mf": 2, "mg": 2, "aleb": 2, "lambda": [2, 5], "underscor": [2, 3], "flag": [2, 3], "squiggli": 2, "marker": 2, "nnc": 2, "bbb": [2, 5], "fneven": 2, "fnodd": 2, "ef": 2, "eg": 2, "og": 2, "shorten": 2, "rid": 2, "won": [2, 4, 6], "cannot": [2, 3, 4, 5, 6], "contrari": 2, "syntact": 2, "reduct": [2, 3], "erw": 2, "harder": 2, "spot": 2, "rudimentari": 2, "foundat": [2, 3, 4, 5], "impos": 2, "restrict": [2, 3, 4, 6], "talk": [2, 4, 6], "assert": [2, 3], "ask": [2, 4, 5, 6], "xs": [2, 3], "tran": [2, 4, 5], "setub": 2, "inject": [2, 3, 4, 6], "x_1": [2, 3], "x_2": [2, 3], "x\u2081": [2, 3, 5, 6], "x\u2082": [2, 3, 5], "add": [2, 4, 5, 6], "nonzero": [2, 4, 5], "add_left_inj": 2, "composit": [2, 3, 5, 6], "injg": 2, "injf": [2, 3], "canon": [2, 3, 4, 5], "exhibit": [2, 6], "anonym": [2, 3, 4, 5], "constructor": [2, 3, 4, 5], "angl": 2, "whatev": [2, 4], "certain": [2, 6], "fnhasub": 2, "fnhaslb": 2, "fnub_add": 2, "gun": 2, "ubf": 2, "ubg": 2, "ubfa": 2, "ubfb": 2, "unpack": [2, 3], "claus": 2, "whose": [2, 4, 5, 6], "els": [2, 3, 4], "turn": [2, 3, 4, 5, 6, 7], "directli": [2, 4, 5, 6], "lbf": 2, "lbg": 2, "cousin": 2, "rcase": [2, 3, 4, 5, 6], "flexibl": [2, 6], "recurs": [2, 3, 5, 10], "harm": [2, 3], "swiss": 2, "armi": 2, "knive": 2, "wide": 2, "old": [2, 5], "chestnut": 2, "product": [2, 4, 5, 6], "magic": [2, 5], "verifi": 2, "sumofsquar": 2, "sumofsquares_mul": 2, "sosx": 2, "sosi": 2, "xeq": [2, 3], "yeq": 2, "insight": 2, "motiv": 2, "gaussian": [2, 10], "i": [2, 3, 4, 5, 6], "sqrt": [2, 3, 4, 5], "norm": [2, 5, 6], "reflect": 2, "di": [2, 5], "xy": [2, 5], "cryptic": 2, "easiest": [2, 4], "perspicu": 2, "divis": [2, 4, 5, 10], "divab": 2, "divbc": 2, "beq": 2, "ceq": 2, "And": [2, 4, 6], "pretti": [2, 6], "Then": [2, 3, 5, 6], "divac": 2, "alpha": [2, 3], "beta": [2, 3], "surject": [2, 3, 6], "yourself": [2, 5], "field_simp": [2, 5], "denomin": [2, 4, 5], "div_mul_cancel": 2, "hx": [2, 3, 5], "method": [2, 3, 4, 5], "surjg": 2, "surjf": [2, 3], "strictli": 2, "contradict": [2, 3, 4], "speak": [2, 5, 6], "irreflex": 2, "asymmetri": 2, "lt_asymm": 2, "sugar": 2, "eventu": [2, 3, 6], "fnuba": 2, "not_le_of_gt": 2, "not_lt_of_g": [2, 4, 5], "lt_of_not_g": 2, "le_of_not_gt": 2, "snippet": [2, 4, 5], "counterexampl": 2, "monof": 2, "noth": [2, 3, 4, 5], "four": [2, 5], "valid": 2, "far": [2, 3, 6], "q": [2, 4, 5, 6], "straightforward": 2, "difficult": 2, "conclud": 2, "nonexist": 2, "contradictori": 2, "classic": [2, 3, 4], "by_contra": [2, 4], "not_not": 2, "front": 2, "push": [2, 4, 6], "inward": 2, "facilit": [2, 6], "push_neg": [2, 3, 4], "restat": 2, "contrapos": [2, 3, 4], "yet": [2, 3, 4, 5, 6], "semicolon": [2, 4], "falso": 2, "anyth": [2, 5, 6], "elim": 2, "strang": [2, 4], "fairli": 2, "reach": 2, "37": 2, "exfalso": 2, "absurd": [2, 4], "slick": 2, "drop": 2, "manner": [2, 5], "contrast": [2, 3, 5, 6], "compon": [2, 3, 5, 6], "techniqu": [2, 6], "variou": [2, 3, 5], "xltz": 2, "zlty": 2, "10": 2, "7": [2, 4, 6], "behav": [2, 3, 6], "roughli": [2, 3, 4], "friend": [2, 5], "were": [2, 4, 5, 6], "inscrut": [2, 3], "gadget": [2, 6], "auxiliari": [2, 6], "pow_eq_zero": [2, 4], "doubl": [2, 3], "symmetr": [2, 3], "abs_lt": 2, "dvd_gcd_iff": 2, "8": [2, 4, 6], "6": [2, 4, 5, 6], "15": 2, "below": [2, 3, 4, 5, 6], "not_monotone_iff": 2, "antisymmetr": 2, "aris": 2, "preorder": [2, 6], "pre": 2, "lt_iff_le_not_l": 2, "beyond": 2, "repeatedli": [2, 6], "instanti": [2, 5, 6], "inl": [2, 3], "inr": [2, 3], "produc": 2, "branch": [2, 3], "le_or_gt": 2, "abs_of_nonneg": [2, 5], "abs_of_neg": 2, "immedi": [2, 3, 5], "myab": 2, "le_abs_self": [2, 5], "neg_le_abs_self": 2, "enjoi": [2, 3, 4, 6], "pun": 2, "lt_ab": 2, "genuin": 2, "vertic": [2, 5], "lt_trichotomi": 2, "xgt": 2, "dvd_mul_right": [2, 4], "eq_zero_or_eq_zero_of_mul_eq_zero": 2, "nontrivi": [2, 3, 4, 5, 6], "integr": [2, 7], "isdomain": 2, "em": [2, 3], "exclud": [2, 4], "by_cas": [2, 3, 4], "dispos": 2, "s_0": [2, 3], "s_1": 2, "s_2": 2, "ldot": [2, 3, 4], "varepsilon": [2, 6], "s_n": [2, 3], "render": [2, 4], "convergesto": 2, "ext": [2, 3, 4, 5], "enabl": [2, 3, 4, 5], "actual": [2, 3, 4, 6], "u": [2, 3, 5, 6], "v": [2, 3, 5, 6], "congr": 2, "reconcil": 2, "peel": 2, "convert": [2, 4], "quit": [2, 6], "zero_lt_on": [2, 4], "fill": [2, 3, 4, 5], "convergesto_const": 2, "\u03b5po": [2, 6], "nge": 2, "abs_zero": 2, "save": [2, 3], "troubl": [2, 3, 5], "pen": 2, "paper": [2, 3, 5, 6], "ns": 2, "nt": 2, "maximum": [2, 4, 6], "implement": [2, 5], "convergesto_add": 2, "cs": 2, "ct": 2, "\u03b52po": 2, "hs": [2, 4, 6], "ht": 2, "le_of_max_le_left": 2, "le_of_max_le_right": 2, "tricki": [2, 3, 4], "convergesto_mul_const": 2, "mulzeroclass": 2, "acpo": 2, "abs_po": 2, "independ": [2, 3, 5], "exists_abs_le_of_convergesto": 2, "strong": [2, 4], "n\u2080": 2, "bpo": [2, 6], "pos\u2080": 2, "div_po": 2, "n\u2081": 2, "convergesto_mul": 2, "sketch": [2, 3, 4, 6], "limit": [2, 6], "bold": 2, "scratch": 2, "convergesto_uniqu": 2, "sa": 2, "sb": 2, "abn": 2, "na": 2, "hna": 2, "nb": 2, "hnb": 2, "absa": 2, "absb": 2, "observ": [2, 4, 6], "everywher": [2, 3, 6], "linearord": 2, "vastli": 2, "awai": [2, 5], "vocabulari": 3, "uniform": [3, 6], "primit": 3, "conceptu": 3, "advantag": [3, 4, 5], "overload": 3, "verbos": 3, "system": [3, 4, 5], "wrong": 3, "theoret": [3, 6], "ss": 3, "sub": [3, 6], "cap": 3, "un": 3, "cup": 3, "univ": [3, 6], "empti": [3, 4, 5, 6], "member": [3, 6], "membership": [3, 4], "mem": 3, "notin": 3, "ident": [3, 4, 5, 6, 10], "databas": [3, 4, 6], "unlik": [3, 4], "existenti": [3, 10], "subset_def": 3, "inter_def": 3, "xu": 3, "mem_inter_iff": 3, "xsu": 3, "phenomenon": 3, "quirk": 3, "pitfal": 3, "heavili": [3, 6], "fall": 3, "union_def": 3, "mem_union": [3, 4], "xtu": 3, "xt": 3, "unnecessari": 3, "clearer": [3, 5], "correctli": 3, "special": [3, 4, 5, 6], "rewritten": 3, "diff_eq": 3, "mem_diff": 3, "xstu": 3, "xnt": 3, "xnu": 3, "extension": [3, 5], "unsurprisingli": 3, "dollar": 3, "sign": [3, 6], "and_comm": 3, "antisymm": 3, "hood": [3, 5], "builder": 3, "trivial": [3, 4, 6], "eq_two_or_odd": 3, "even_iff": 3, "confus": [3, 4, 6], "fortun": 3, "agre": 3, "prime_iff": 3, "symm": [3, 4, 5, 6], "rwa": [3, 4, 5], "signific": 3, "ball": 3, "bex": 3, "bex_def": 3, "prime_x": 3, "slight": 3, "ssubt": 3, "index": [3, 6], "model": [3, 6], "sequenc": [3, 6, 10], "a_0": 3, "a_1": 3, "a_2": 3, "mem_iunion": 3, "xai": 3, "mem_iint": 3, "mem_union\u2082": 3, "mem_inter\u2082": 3, "mem_iunion\u2082": 3, "exists_prime_and_dvd": 3, "eq_univ": 3, "eq_univ_of_foral": 3, "exists_infinite_prim": 3, "\u2080": 3, "sunion": 3, "sinter": 3, "relationship": [3, 4], "mem_iinter\u2082": 3, "sunion_eq_biunion": 3, "sinter_eq_biint": 3, "preimag": [3, 6], "imag": [3, 4, 6], "tripl": 3, "tag": 3, "mem_image_of_mem": 3, "galoi": [3, 5, 6], "image_subset_iff": 3, "represent": [3, 4, 5], "asid": 3, "raini": 3, "dai": 3, "behavior": [3, 6], "nonempti": [3, 6], "condit": [3, 4, 6], "fxeq": 3, "ai": 3, "fx": 3, "eq": [3, 5], "injon": 3, "theme": 3, "rel": [3, 5], "relativ": 3, "xpo": 3, "ypo": 3, "exp_log": 3, "ingredi": [3, 5, 6], "assign": [3, 5], "inhabit": [3, 5, 6], "appeal": 3, "choose_spec": 3, "some_spec": 3, "noncomput": [3, 5], "inverse_spec": 3, "dif_po": 3, "dif_neg": 3, "fulli": [3, 6], "alon": 3, "leftinvers": 3, "rightinvers": 3, "hack": 3, "half": 3, "dozen": 3, "condens": 3, "cantor": 3, "famou": 3, "miss": [3, 4], "j": [3, 5], "intuit": [3, 6], "cardin": 3, "biject": [3, 5], "nineteenth": 3, "centuri": 3, "infinit": [3, 6, 10], "dedekind": 3, "quickli": 3, "behind": 3, "problem": [3, 4, 5, 6], "shade": 3, "region": 3, "diagram": 3, "circ": [3, 5], "scale": 3, "inner": 3, "smaller": [3, 4, 6], "concentr": 3, "unshad": 3, "compos": [3, 5, 6], "disjoint": 3, "sound": [3, 5], "plausibl": 3, "delic": 3, "improv": [3, 4], "confid": 3, "invfun": [3, 5], "leftinverse_invfun": 3, "invfun_eq": 3, "sbaux": 3, "sbset": 3, "sb_aux": 3, "s_": 3, "sb_set": 3, "bigcup_": 3, "mathbb": [3, 4, 5], "sbfun": 3, "complement": [3, 6], "outermost": 3, "setminu": 3, "inv_fun": 3, "inv_fun_eq": 3, "sb_right_inv": 3, "goe": [3, 4, 5, 6], "henc": [3, 4, 5, 6], "neither": [3, 5], "nor": [3, 5], "sb_inject": 3, "hf": [3, 6], "hg": [3, 6], "a_def": 3, "h_def": 3, "hxeq": 3, "xa": [3, 5], "wlog": 3, "x\u2081a": 3, "resolve_left": 3, "x\u2082a": 3, "not_imp_self": 3, "x\u2082na": 3, "if_po": 3, "if_neg": 3, "x\u2082eq": 3, "hn": [3, 4, 6], "sb_fun": 3, "bring": [3, 4, 6], "tradeoff": 3, "encapsul": [3, 5], "symmetri": 3, "dwell": 3, "succ": [3, 4], "sb_surject": 3, "gya": 3, "xmem": 3, "sweet": 3, "schroeder_bernstein": 3, "substant": 4, "ancient": 4, "fraction": 4, "lowest": 4, "2c": 4, "4c": 4, "factor": [4, 5], "coprim": 4, "smart": 4, "12": 4, "encount": 4, "algebra": [4, 6, 10], "prime_def_lt": 4, "eq_one_or_self_of_dvd": 4, "prime_p": 4, "17": 4, "commonli": [4, 5], "prime_two": 4, "prime_thre": 4, "broader": [4, 7], "irreduc": [4, 5], "coincid": [4, 5, 6], "rise": 4, "dvd_mul": 4, "even_of_even_sqr": 4, "dvd_of_dvd_pow": 4, "proce": 4, "profici": 4, "ctrl": [4, 5], "search": [4, 5], "engin": 4, "hesit": 4, "mul_right_inj": 4, "heart": 4, "irration": 4, "dvd_gcd": 4, "coprime_mn": 4, "sqr_eq": 4, "meq": 4, "dvd_iff_exists_eq_mul_left": 4, "two_l": 4, "le_of_dvd": 4, "approach": [4, 5, 6], "quick": 4, "ne": [4, 5], "occur": 4, "suffici": [4, 6], "permut": 4, "prime_of_mem_factor": 4, "prod_factor": 4, "factors_uniqu": 4, "factorization_mul": 4, "mnez": 4, "nnez": 4, "factorization_pow": 4, "black": 4, "box": 4, "simpa": 4, "nnz": 4, "nsqr_nez": 4, "eq1": 4, "eq2": 4, "add_mul_mod_self_left": 4, "mul_mod_right": 4, "count_factors_mul_of_po": 4, "successor": 4, "succ_ne_zero": 4, "npow_nz": 4, "dvd_sub": 4, "pow_eq": 4, "npowz": 4, "add_sub_cancel": 4, "understood": [4, 6], "quotient": [4, 5, 6], "pictur": [4, 5], "mediat": 4, "headach": 4, "contend": 4, "issu": [4, 5, 6], "th": 4, "topic": 4, "enat": 4, "infin": [4, 6], "appreci": 4, "role": [4, 5, 6], "_section_induction_and_recurs": 4, "writ": 4, "datatyp": 4, "freeli": 4, "translat": [4, 6], "mathematician": [4, 6], "inj": 4, "factori": 4, "fac": 4, "ih": 4, "fac_po": 4, "succ_po": 4, "dvd_fac": 4, "ipo": 4, "il": 4, "of_le_succ": 4, "dvd_mul_of_dvd_right": 4, "crude": 4, "remaind": [4, 5], "pow_two_le_fac": 4, "finset": [4, 5, 6], "bigoper": [4, 5], "prod": [4, 6], "sum_range_zero": 4, "sum_range_succ": 4, "summat": 4, "prod_range_zero": 4, "prod_range_succ": 4, "deserv": 4, "comment": 4, "danger": [4, 5], "ordinarili": [4, 5], "loop": 4, "indefinit": 4, "fix": [4, 6], "placement": 4, "re": [4, 5], "handi": 4, "sum_id": 4, "div_eq_of_eq_mul_right": 4, "succ_eq_add_on": 4, "sum_sqr": 4, "mynat": 4, "thumb": 4, "decid": [4, 6], "preced": 4, "truncat": 4, "exponenti": 4, "cut": 4, "predecessor": 4, "pred": 4, "mul": [4, 5, 6], "succ_add": 4, "succ_mul": 4, "explor": [4, 6], "standard": [4, 5, 6], "formul": [4, 6], "quirki": 4, "among": 4, "annoi": 4, "h0": 4, "succ_le_succ": 4, "zero_l": [4, 5], "interval_cas": 4, "interv": [4, 6], "decis": 4, "procedur": 4, "revert": [4, 5], "minfac": 4, "smallest": [4, 6], "strong_induction_on": 4, "subsum": 4, "exists_prime_factor": 4, "np": 4, "mltn": 4, "mdvdn": 4, "mne1": 4, "mz": 4, "zero_dvd_iff": 4, "mgt2": 4, "pp": 4, "pdvd": 4, "factorial_po": 4, "dvd_factori": 4, "primes_infinit": 4, "refin": 4, "ple": 4, "p_1": 4, "p_n": 4, "prod_": 4, "p_i": [4, 6], "computation": 4, "test": 4, "decidableeq": 4, "abandon": 4, "ourselv": 4, "subset_iff": 4, "mem_int": 4, "mem_sdiff": 4, "tauto": 4, "dispens": 4, "tautolog": 4, "dvd_prod_of_mem": 4, "eq_of_dvd_of_prim": 4, "prime_q": 4, "preserv": [4, 6], "induction_on": 4, "singleton": 4, "prod_empti": 4, "prod_insert": 4, "mem_of_dvd_prod_prim": 4, "mem_insert": 4, "wrote": 4, "filter": [4, 10], "mem_filt": 4, "aim": 4, "prod_po": 4, "_def": 4, "mem_": 4, "id": [4, 6], "bounded_of_ex_finset": 4, "qk": 4, "lt_succ_of_l": 4, "le_sup": 4, "ex_finset_of_bound": 4, "decidablepr": 4, "lt_succ_iff": 4, "congruent": 4, "p_k": 4, "loss": 4, "27": 4, "mod_4_eq_3_or_mod_4_eq_3": 4, "mul_mod": 4, "mod_lt": 4, "hm": 4, "two_le_of_mod_4_eq_3": 4, "neq": 4, "div_dvd_of_dvd": 4, "div_lt_self": 4, "piec": [4, 5, 6], "exists_prime_factor_mod_4_eq_3": 4, "dvd_rfl": 4, "mge2": 4, "mul_div_cancel": 4, "home": [4, 5], "stretch": [4, 5], "remov": [4, 6], "eras": 4, "mem_eras": 4, "readi": [4, 6], "dvd_add_iff_left": 4, "primes_mod_4_eq_3_infinit": 4, "p4": 4, "pltn": 4, "p4eq": 4, "ps": 4, "pne3": 4, "seriou": [4, 6], "feat": 4, "modern": 5, "subject": 5, "mysteri": 5, "technic": 5, "consult": 5, "ann": 5, "baanen": 5, "abus": 5, "paramet": 5, "broadest": 5, "constraint": [5, 6], "bundl": [5, 6], "tupl": 5, "hy": 5, "hz": 5, "mypoint1": 5, "mypoint2": 5, "mypoint3": 5, "mk": [5, 6], "former": 5, "latter": [5, 6], "quot": [5, 6], "protect": 5, "intern": 5, "add_x": 5, "addalt": 5, "etc": [5, 6], "y\u2081": 5, "z\u2081": 5, "y\u2082": 5, "z\u2082": 5, "addalt_x": 5, "addalt_comm": 5, "ya": 5, "za": 5, "xb": 5, "yb": 5, "zb": 5, "apart": 5, "effici": [5, 6], "scalar": 5, "smul": 5, "smul_distrib": 5, "road": 5, "link": 5, "belong": [5, 6], "simplex": 5, "convinc": 5, "equilater": 5, "interior": 5, "standardtwosimplex": 5, "x_nonneg": 5, "y_nonneg": 5, "z_nonneg": 5, "sum_eq": 5, "swap": 5, "swapxi": 5, "interestingli": 5, "midpoint": 5, "div_nonneg": 5, "weight": 5, "averag": 5, "weightedaverag": 5, "lambda_nonneg": 5, "lambda_l": 5, "fin": 5, "standardsimplex": 5, "sum_eq_on": 5, "div_eq_mul_inv": 5, "sum_mul": 5, "sum_add_distrib": 5, "mul_sum": 5, "manipul": [5, 6], "islinear": 5, "is_addit": 5, "preserves_mul": 5, "linf": 5, "subtyp": [5, 6], "preal": 5, "val": 5, "sigma": 5, "wherebi": [5, 6], "stdsimplex": 5, "\u03c3": 5, "fst": [5, 6], "snd": [5, 6], "custom": 5, "robust": 5, "interfac": 5, "redefin": 5, "accessor": 5, "weav": 5, "rich": 5, "interconnect": 5, "hierarchi": 5, "clarifi": 5, "antireflex": 5, "cdot": 5, "mathcal": 5, "proxi": 5, "bipartit": 5, "graph": 5, "categori": [5, 6], "morphism": 5, "basi": [5, 6], "discret": 5, "inherit": 5, "polynomi": 5, "coeffici": 5, "dual": [5, 6], "accommod": 5, "almost": [5, 6], "marriag": 5, "heaven": 5, "group\u2081": 5, "inv": 5, "struc": 5, "counterpart": 5, "chosen": 5, "assur": 5, "groupcat": 5, "group\u2081cat": 5, "str": 5, "capit": 5, "roman": 5, "equiv": 5, "tofun": 5, "right_inv": 5, "left_inv": 5, "creativ": 5, "evid": 5, "coercion": [5, 6], "omit": 5, "perm": 5, "under": [5, 6], "orient": 5, "permgroup": 5, "trans_assoc": 5, "trans_refl": 5, "refl_tran": 5, "self_trans_symm": 5, "grouptheori": 5, "g_1": 5, "g_2": 5, "g_3": 5, "tightli": 5, "isomorph": 5, "additivegroup": 5, "Its": 5, "neg": [5, 6], "reproduc": 5, "accompani": 5, "addgroup\u2081": 5, "scheme": 5, "add_group_point": 5, "add_group\u2081": 5, "arrang": 5, "mul_inv_cancel_right": 5, "achiev": [5, 6], "silent": 5, "regist": 5, "grp": 5, "contextu": 5, "cue": 5, "synthes": 5, "whole": 5, "_inst_1": 5, "candid": 5, "group\u2082": 5, "mysquar": 5, "my_squar": 5, "remark": 5, "head": 5, "store": 5, "headi": 5, "hasmulgroup\u2082": 5, "hasonegroup\u2082": 5, "hasinvgroup\u2082": 5, "suppli": 5, "accord": 5, "capabl": 5, "chain": 5, "recent": 5, "prioriti": 5, "bad": [5, 6], "artifici": 5, "addgroup\u2082": 5, "subtl": [5, 6], "configur": 5, "invis": 5, "wise": 5, "euclidean": 5, "terminolog": 5, "mid": 5, "imaginari": 5, "gaussint": 5, "im": 5, "pointwis": [5, 6], "root": [5, 10], "ac": 5, "bci": 5, "adi": 5, "bd": 5, "bc": 5, "hasmul": 5, "zero_def": 5, "one_def": 5, "add_def": 5, "neg_def": 5, "mul_def": 5, "zero_r": 5, "zero_im": 5, "one_r": 5, "one_im": 5, "add_r": 5, "add_im": 5, "neg_r": 5, "neg_im": 5, "mul_r": 5, "mul_im": 5, "surprisingli": 5, "concept": [5, 6], "light": 5, "bulb": 5, "skeleton": [5, 6], "scari": 5, "entri": 5, "instcommr": 5, "left_distrib": 5, "right_distrib": 5, "ext_iff": 5, "bq": 5, "archetyp": 5, "int": 5, "ediv_add_emod": 5, "emod_nonneg": 5, "emod_lt": 5, "unit": [5, 6], "algorithm": 5, "conjug": 5, "frac": 5, "nearest": 5, "size": 5, "vi": 5, "multipli": 5, "view": [5, 6], "emb": 5, "forth": 5, "quadrat": 5, "gaussian_int": 5, "stai": 5, "face": [5, 6], "machineri": [5, 6], "adapt": 5, "invest": 5, "pragmat": 5, "seek": 5, "heather": 5, "macbeth": 5, "eleg": 5, "div": 5, "mod": 5, "_add_mod": 5, "abs_mod": 5, "_le": 5, "emod_lt_of_po": 5, "zero_lt_two": 5, "fixm": 5, "_eq": 5, "sq_add_sq_eq_zero": 5, "linearorderedr": 5, "norm_nonneg": 5, "norm_eq_zero": 5, "norm_po": 5, "norm_mul": 5, "conj": 5, "conj_r": 5, "conj_im": 5, "norm_conj": 5, "bespok": 5, "quad": 5, "record": 5, "div_def": 5, "mod_def": 5, "messi": 5, "nicer": [5, 6], "norm_mod_lt": 5, "norm_y_po": 5, "sub_mul": 5, "conv": 5, "lh": 5, "sq_le_sq": 5, "mul_le_mul_of_nonneg_left": 5, "ediv_mul_l": 5, "ediv_nonneg": 5, "le_of_mul_le_mul_right": 5, "ediv_lt_of_lt_mul": 5, "natab": 5, "coe_natabs_norm": 5, "natabs_of_nonneg": 5, "natabs_norm_mod_lt": 5, "ofnat_lt": 5, "coe_natab": 5, "not_norm_mul_left_lt_norm": 5, "natabs_mul": 5, "le_mul_of_one_le_right": 5, "ofnat_l": 5, "add_one_le_of_lt": 5, "euclideandomain": 5, "quotient_mul_add_remainder_eq": 5, "quotient_zero": 5, "r_wellfound": 5, "remainder_lt": 5, "mul_left_not_lt": 5, "payoff": 5, "principalidealr": 5, "irreducible_iff_prim": 5, "calculu": 6, "quantiti": 6, "studi": 6, "begun": 6, "paradox": 6, "layer": 6, "naiv": 6, "slightli": 6, "exot": 6, "intermedi": 6, "x\u2080": 6, "convention": 6, "eight": 6, "varieti": 6, "wish": 6, "64": 6, "y\u2080": 6, "z\u2080": 6, "paragraph": 6, "512": 6, "bourbaki": 6, "spell": 6, "dualli": 6, "arbitrarili": 6, "neighborhood": 6, "at_top": 6, "\ud835\udcdd": 6, "\ud835\udce4": 6, "entourag": 6, "\u03bc": 6, "a_": 6, "univ_set": 6, "sets_of_superset": 6, "inter_set": 6, "blur": 6, "princip": 6, "\ud835\udcdf": 6, "demonstr": 6, "opportun": 6, "x_0": 6, "ioo": 6, "tendsto\u2081": 6, "tendsto": 6, "lim_": 6, "sourc": 6, "abstractli": 6, "hide": 6, "salient": 6, "pushforward": 6, "f_": 6, "ve": 6, "tendsto\u2082": 6, "via": 6, "promis": 6, "leverag": 6, "map_mono": 6, "map_map": 6, "shot": 6, "256": 6, "pullback": 6, "comap": 6, "map_le_iff_le_comap": 6, "contravari": 6, "comap_comap": 6, "shift": 6, "plane": 6, "\u1da0": 6, "nhds_prod_eq": 6, "aforement": 6, "le_inf_iff": 6, "attop": 6, "bottom": 6, "shouldn": 6, "prohibit": 6, "global": 6, "precondit": 6, "closur": 6, "ne_bot": 6, "tour": 6, "claim": 6, "recaptur": 6, "superfici": 6, "stronger": 6, "famili": 6, "\u03b9": 6, "select": 6, "hasbasi": 6, "nhds_basis_ioo_po": 6, "has_basi": 6, "tendsto_iff": 6, "reformul": 6, "ici": 6, "attop_basi": 6, "knew": 6, "gave": 6, "n_p": 6, "n_q": 6, "tiresom": 6, "unpleas": 6, "superscript": 6, "hp": 6, "hq": 6, "eventually_eq": 6, "tendsto_congr": 6, "review": 6, "ensur": 6, "eventually_of_foral": 6, "mono": 6, "item": 6, "filter_upward": 6, "hr": 6, "reader": 6, "ae": 6, "aka": 6, "occasion": 6, "frequent": 6, "mem_closure_of_tendsto": 6, "cluster_pt": 6, "mem_closure_iff_clusterpt": 6, "le_principal_iff": 6, "nebot_of_l": 6, "hux": 6, "hum": 6, "dist_eq_zero": 6, "emetricspac": 6, "pseudometricspac": 6, "pseudoemetricspac": 6, "journei": 6, "recast": 6, "tendsto_attop": 6, "continuous_iff": 6, "devot": 6, "uncurri": 6, "slow": 6, "continuous_fst": 6, "comp": 6, "assembl": 6, "prod_mk": 6, "continuous_snd": 6, "continuous_dist": 6, "clunki": 6, "crucial": 6, "gradual": 6, "elabor": 6, "refus": 6, "prod_map": 6, "sad": 6, "wrap": 6, "border": 6, "obfusc": 6, "continuous_pow": 6, "continuous_id": 6, "continuousat": 6, "continuousat_iff": 6, "geometr": 6, "closedbal": 6, "radiu": 6, "mem_ball_self": 6, "mem_closedball_self": 6, "isopen": 6, "isopen_iff": 6, "Their": 6, "isclos": 6, "s\u1d9c": 6, "isopen_compl_iff": 6, "hu": 6, "mem_of_tendsto": 6, "mem_closure_iff": 6, "mem_closure_iff_seq_limit": 6, "main": 6, "nhds_basis_bal": 6, "nhds_basis_closedbal": 6, "mem_iff": 6, "segment": 6, "somewher": 6, "continuouson": 6, "minimum": 6, "deduc": 6, "iscompact": 6, "icc": 6, "iscompact_icc": 6, "\u03c6": 6, "strictmono": 6, "tendsto_subseq": 6, "exists_forall_l": 6, "exists_forall_g": 6, "compactspac": 6, "iscompact_univ": 6, "cauchi": 6, "uniformcontinu": 6, "uniformcontinuous_iff": 6, "clearli": 6, "isclosed_l": 6, "eq_empty_or_nonempti": 6, "attain": 6, "closer": 6, "cauchyseq": 6, "cauchyseq_iff": 6, "completespac": 6, "cauchyseq_tendsto_of_complet": 6, "criterion": 6, "explan": 6, "tendsto_pow_attop_nhds_0_of_lt_1": 6, "dist_le_range_sum_dist": 6, "cauchyseq_of_le_geometric_two": 6, "\u03b5_po": 6, "le_iff_exists_add": 6, "boss": 6, "bair": 6, "exclam": 6, "induct": [6, 10], "rec_on": 6, "ho": 6, "hd": 6, "dens": 6, "densiti": 6, "\u03b4po": 6, "hpo": 6, "hball": 6, "mem_closure_iff_nhds_basi": 6, "recon": 6, "rpo": 6, "rb": 6, "incl": 6, "cdist": 6, "ylim": 6, "yball": 6, "categor": 6, "ignor": 6, "topologicalspac": 6, "isopen_univ": 6, "isopen_empti": 6, "isopen_iunion": 6, "fintyp": 6, "isopen_iint": 6, "continuous_def": 6, "attach": 6, "filteri": 6, "sent": 6, "mem_nhds_iff": 6, "weird": 6, "digress": 6, "pure_le_nhd": 6, "eventually_eventually_nhd": 6, "topological_spac": 6, "mk_of_nhd": 6, "nhds_mk_of_nhd": 6, "clean": 6, "fonctori": 6, "induc": 6, "sensibl": 6, "uncount": 6, "relatedli": 6, "coinduc": 6, "t_x": 6, "t_y": 6, "coinduced_le_iff_le_induc": 6, "covari": 6, "coinduced_compos": 6, "induced_compos": 6, "topological_structur": 6, "primarili": 6, "ie": 6, "focus": 6, "nhd": 6, "opposit": 6, "recov": 6, "foward": 6, "continuous_iff_coinduced_l": 6, "g_": 6, "t_z": 6, "wasn": 6, "\u03c0": 6, "papar": 6, "t_": 6, "x_i": 6, "pi": 6, "defect": 6, "functori": 6, "price": 6, "patholog": 6, "t2_space": 6, "hausdorff": 6, "regular": 6, "t2space": 6, "tendsto_nhds_uniqu": 6, "regularspac": 6, "closed_nhds_basi": 6, "nhds_basis_open": 6, "denseinduc": 6, "continuousat_extend": 6, "funni": 6, "_in": 6, "thank": 6, "nhds_induc": 6, "is_open": 6, "fortiori": 6, "f_cont": 6, "tendsto_right_iff": 6, "firstcountabletopolog": 6, "sever": 6, "cluster": 6, "clusterpt": 6, "nebot": 6, "hfx": 6, "push_pul": 6, "of_map": 6, "f_ne": 6, "f_le": 6, "map_eq": 6, "hne": 6, "hle": 6, "huo": 6, "hsu": 6, "elim_finite_subcov": 6, "elementary_differential_calculu": 7, "introductori": 7, "normed_spac": 7, "overview": 10, "conjunct": 10, "converg": 10, "schr\u00f6der": 10, "bernstein": 10, "irrat": 10}, "objects": {}, "objtypes": {}, "objnames": {}, "titleterms": {"introduct": 0, "get": 0, "start": 0, "overview": 0, "basic": 1, "calcul": 1, "prove": 1, "ident": 1, "algebra": [1, 5], "structur": [1, 5], "us": 1, "theorem": [1, 3], "lemma": 1, "more": 1, "order": 1, "divis": 1, "fact": 1, "about": 1, "logic": 2, "implic": 2, "univers": 2, "quantifi": 2, "The": [2, 3], "existenti": 2, "negat": 2, "conjunct": 2, "bi": 2, "disjunct": 2, "sequenc": 2, "converg": [2, 6], "set": [3, 6], "function": [3, 6], "schr\u00f6der": 3, "bernstein": 3, "number": 4, "theori": [4, 8], "irrat": 4, "root": 4, "induct": 4, "recurs": 4, "infinit": 4, "mani": 4, "prime": 4, "abstract": 5, "build": 5, "gaussian": 5, "integ": 5, "topolog": 6, "filter": 6, "metric": 6, "space": 6, "continu": 6, "ball": 6, "open": 6, "close": 6, "compact": 6, "uniformli": 6, "complet": 6, "fundament": 6, "separ": 6, "countabl": 6, "differenti": 7, "calculu": 7, "integr": 8, "measur": 8, "index": 9, "mathemat": 10, "lean": 10}, "envversion": {"sphinx.domains.c": 2, "sphinx.domains.changeset": 1, "sphinx.domains.citation": 1, "sphinx.domains.cpp": 6, "sphinx.domains.index": 1, "sphinx.domains.javascript": 2, "sphinx.domains.math": 2, "sphinx.domains.python": 3, "sphinx.domains.rst": 2, "sphinx.domains.std": 2, "sphinx": 56}}) + Search.setIndex({"docnames": ["C01_Introduction", "C02_Basics", "C03_Logic", "C04_Sets_and_Functions", "C05_Number_Theory", "C06_Abstract_Algebra", "C07_Topology", "C08_Differential_Calculus", "C09_Integration_and_Measure_Theory", "genindex", "index"], "filenames": ["C01_Introduction.rst", "C02_Basics.rst", "C03_Logic.rst", "C04_Sets_and_Functions.rst", "C05_Number_Theory.rst", "C06_Abstract_Algebra.rst", "C07_Topology.rst", "C08_Differential_Calculus.rst", "C09_Integration_and_Measure_Theory.rst", "genindex.rst", "index.rst"], "titles": ["1. Introduction", "2. Basics", "3. Logic", "4. Sets and Functions", "5. Number Theory", "6. Abstract Algebra", "7. Topology", "Differential Calculus", "Integration and Measure Theory", "Index", "Mathematics in Lean"], "terms": {"The": [0, 1, 4, 5, 6, 10], "goal": [0, 1, 2, 3, 4, 5, 6], "thi": [0, 1, 2, 3, 4, 5, 6, 7], "book": [0, 6], "teach": 0, "you": [0, 1, 2, 3, 4, 5, 6], "formal": [0, 1, 2, 3, 4, 5, 6, 7], "mathemat": [0, 1, 2, 3, 4, 5, 6], "us": [0, 2, 3, 4, 5, 6, 10], "lean": [0, 1, 2, 3, 4, 5, 6], "4": [0, 1, 2, 4, 5, 6], "interact": [0, 5], "proof": [0, 1, 2, 3, 4, 5, 6], "assist": [0, 5], "It": [0, 1, 2, 3, 4, 5, 6], "assum": [0, 1, 2, 3, 4, 6], "know": [0, 1, 2, 3, 4, 5, 6], "some": [0, 1, 2, 3, 4, 5, 6], "doe": [0, 1, 2, 3, 4, 5, 6], "requir": [0, 1, 2, 3, 4, 5, 6], "much": [0, 2, 4, 6, 7], "although": [0, 3, 4, 5, 6], "we": [0, 1, 2, 3, 4, 5, 6, 7], "cover": [0, 1, 3, 6], "exampl": [0, 1, 2, 3, 4, 5, 6], "rang": [0, 2, 3, 4, 6], "from": [0, 1, 2, 3, 4, 5, 6, 7], "number": [0, 1, 2, 3, 5, 6, 7, 10], "theori": [0, 1, 2, 3, 6, 7, 10], "measur": [0, 5, 6, 7], "analysi": [0, 5, 7], "focu": [0, 1, 6], "elementari": [0, 3, 4, 5, 6], "aspect": [0, 5], "those": [0, 1, 2, 3, 5, 6], "field": [0, 1, 5], "hope": 0, "thei": [0, 1, 2, 3, 4, 5, 6], "ar": [0, 1, 2, 3, 4, 5, 6], "familiar": [0, 1, 4, 5, 6, 7], "can": [0, 1, 2, 3, 4, 5, 6], "pick": 0, "them": [0, 1, 2, 3, 4, 5, 6], "up": [0, 2, 3, 4, 5, 6], "go": [0, 1, 2, 3, 4, 6], "also": [0, 1, 2, 3, 4, 5, 6], "don": [0, 1, 2, 3, 4, 5, 6], "t": [0, 1, 2, 3, 4, 5, 6], "presuppos": 0, "ani": [0, 1, 2, 3, 4, 5, 6, 7], "background": 0, "seen": [0, 1, 2, 4, 5, 6], "kind": [0, 1, 6], "comput": [0, 3, 4, 5], "program": [0, 1], "write": [0, 1, 2, 3, 4, 5, 6], "definit": [0, 1, 2, 3, 4, 5, 6], "theorem": [0, 2, 4, 5, 6, 10], "regiment": 0, "languag": [0, 1, 3], "like": [0, 1, 2, 3, 4, 5, 6], "understand": [0, 2, 3, 4, 5, 6], "In": [0, 1, 2, 3, 4, 5, 6, 7], "return": [0, 2, 3, 4, 5, 6], "provid": [0, 1, 2, 3, 4, 5, 6], "feedback": 0, "inform": [0, 1, 2, 3, 5, 6], "interpret": [0, 1, 4, 5, 6], "express": [0, 1, 2, 3, 4, 5, 6], "guarante": [0, 3, 5], "well": [0, 1, 2, 3, 4, 5, 6], "form": [0, 1, 2, 3, 4, 5, 6], "ultim": 0, "certifi": 0, "correct": [0, 1], "our": [0, 1, 2, 3, 4, 5, 6], "learn": [0, 1, 2, 4, 5], "more": [0, 2, 3, 4, 5, 6, 10], "about": [0, 2, 3, 4, 5, 6, 10], "project": [0, 4, 5, 6], "page": [0, 1, 4], "commun": [0, 4], "web": [0, 1, 4], "tutori": 0, "base": [0, 3, 4, 6], "s": [0, 1, 2, 3, 4, 5, 6], "larg": [0, 6], "ever": [0, 6], "grow": 0, "librari": [0, 1, 2, 3, 4, 5, 6], "mathlib": [0, 1, 2, 3, 4, 5, 6], "strongli": 0, "recommend": [0, 1, 3], "take": [0, 1, 2, 3, 4, 5, 6], "look": [0, 1, 2, 3, 4, 6], "zulip": [0, 4], "onlin": 0, "chat": 0, "group": [0, 1, 2, 3, 5, 6], "haven": [0, 2, 6], "alreadi": [0, 1, 2, 3, 4, 5, 6], "ll": [0, 1, 2, 4, 6], "find": [0, 1, 2, 4, 5, 6], "live": [0, 5], "welcom": [0, 1], "enthusiast": 0, "happi": 0, "answer": [0, 5, 6], "question": [0, 4, 6], "offer": [0, 2, 5, 6], "moral": [0, 5], "support": [0, 1, 2, 3, 4, 5, 6], "read": [0, 1, 4, 6], "pdf": 0, "html": 0, "version": [0, 1, 2, 3, 4, 5, 6], "design": [0, 1, 2, 3, 5, 6], "run": 0, "insid": [0, 1, 2, 3], "vs": [0, 1, 2, 3, 5], "code": [0, 1, 2, 3, 5], "editor": [0, 1], "To": [0, 1, 2, 3, 4, 5, 6], "instal": 0, "follow": [0, 1, 2, 3, 4, 5, 6], "instruct": [0, 1, 6], "http": 0, "github": [0, 1], "com": 0, "leanprov": 0, "lean4": 0, "blob": 0, "master": [0, 1, 4], "doc": 0, "quickstart": 0, "md": 0, "_": [0, 1, 2, 3, 4, 5, 6], "termin": 0, "navig": 0, "folder": 0, "where": [0, 1, 2, 3, 4, 5, 6], "want": [0, 1, 2, 3, 4, 5, 6], "put": [0, 1, 2, 3, 4, 5, 6], "copi": [0, 3, 4, 6], "repositori": [0, 1], "type": [0, 1, 2, 3, 4, 5, 6], "git": 0, "clone": 0, "mathematics_in_lean": 0, "fetch": 0, "execut": 0, "lake": 0, "ex": [0, 2], "cach": 0, "compil": 0, "open": [0, 1, 2, 3, 4, 5], "altern": [0, 2, 3, 4, 5, 6], "choos": [0, 2, 3, 4, 5, 6], "file": [0, 1, 4, 5, 6], "menu": [0, 1], "Be": [0, 1, 3], "sure": [0, 1, 2, 3, 5], "other": [0, 1, 2, 3, 4, 5, 6], "simultan": 0, "window": [0, 1, 2, 5], "updat": 0, "newer": 0, "ty": 0, "pull": [0, 6], "cloud": 0, "gitpod": 0, "how": [0, 1, 2, 3, 4, 5, 6], "do": [0, 1, 2, 3, 4, 5, 6], "each": [0, 1, 2, 3, 4, 5, 6], "section": [0, 1, 2, 3, 4, 5, 6], "ha": [0, 1, 2, 3, 4, 5, 6], "an": [0, 1, 2, 3, 4, 5, 6], "associ": [0, 1, 2, 4, 5, 6], "exercis": [0, 1, 2, 3, 5, 6], "src": 0, "organ": 0, "chapter": [0, 1, 2, 3, 4, 5, 6, 7], "make": [0, 1, 2, 3, 4, 5, 6], "so": [0, 1, 2, 3, 4, 5, 6], "experi": [0, 1, 6], "while": [0, 1, 2, 6], "leav": [0, 1, 2, 3, 5], "origin": [0, 1, 5], "intact": 0, "text": [0, 3, 5, 6], "often": [0, 1, 2, 3, 4, 5, 6], "includ": [0, 1, 2, 3, 4, 6], "one": [0, 1, 2, 3, 4, 5, 6], "eval": 0, "hello": 0, "world": 0, "should": [0, 1, 2, 3, 4, 5, 6], "abl": [0, 1, 2, 3, 4, 5], "correspond": [0, 1, 2, 3, 4, 5, 6], "If": [0, 1, 2, 3, 4, 5, 6], "click": [0, 1, 3, 4, 5], "line": [0, 1, 2, 3, 4], "show": [0, 1, 2, 3, 4, 5, 6], "hover": [0, 1, 2, 3, 4, 5], "your": [0, 1, 2, 3, 5, 6], "cursor": [0, 1, 2], "over": [0, 1, 2, 3, 4, 5, 6], "command": [0, 1, 2, 3, 4, 5], "respons": [0, 1], "pop": 0, "encourag": [0, 1, 2, 3, 4, 5], "edit": 0, "try": [0, 1, 2, 3, 4, 5, 6], "own": [0, 1, 4, 5], "moreov": [0, 1, 4, 5, 6], "lot": [0, 3, 5, 6], "challeng": [0, 1, 2, 3, 5], "rush": 0, "past": [0, 1], "just": [0, 1, 2, 3, 4, 5, 6], "work": [0, 1, 2, 3, 4, 5, 6], "through": [0, 1, 3, 4, 5, 6], "central": [0, 4], "alwai": [0, 1, 2, 3, 5], "compar": [0, 5, 6], "solut": [0, 1, 4], "ones": [0, 1, 2, 3, 5], "simpli": [0, 1, 2, 3, 4, 5, 6], "tool": [0, 1, 2, 5], "build": [0, 2, 4, 6, 10], "complex": [0, 1, 2, 4, 5], "known": [0, 1, 2, 3, 4, 5, 6], "depend": [0, 2, 3, 4, 5, 6], "everi": [0, 1, 2, 3, 4, 5, 6], "check": [0, 1, 2, 3, 4, 5, 6], "print": [0, 3, 4, 5], "have": [0, 1, 2, 3, 4, 5, 6], "\u2115": [0, 1, 2, 3, 4, 5, 6], "These": [0, 1, 2, 3, 4, 5], "object": [0, 1, 2, 3, 4, 5], "2": [0, 1, 2, 3, 4, 5, 6], "def": [0, 2, 3, 4, 5, 6], "f": [0, 1, 2, 3, 4, 5, 6], "x": [0, 1, 2, 3, 4, 5, 6], "3": [0, 1, 2, 3, 4, 5, 6], "prop": [0, 2, 3, 4, 5, 6], "statement": [0, 1, 2, 3, 4, 5, 6], "fermatlasttheorem": 0, "y": [0, 1, 2, 3, 4, 5, 6], "z": [0, 1, 2, 5, 6], "n": [0, 1, 2, 3, 4, 5, 6], "0": [0, 1, 2, 3, 4, 5, 6], "p": [0, 2, 3, 4, 5, 6], "itself": [0, 3, 5, 6], "Such": [0, 1, 2], "proposit": [0, 2, 3, 4, 5], "easi": [0, 4, 5, 6], "rfl": [0, 1, 2, 3, 4, 5, 6], "hard": [0, 1, 3, 5], "sorri": [0, 1, 2, 3, 4, 5, 6], "manag": [0, 1, 4, 5, 6], "construct": [0, 2, 3, 4, 5, 6], "fermat_last_theorem": 0, "accept": [0, 1, 6], "term": [0, 1, 2, 3, 4, 5, 6], "done": [0, 2, 3, 4, 6], "someth": [0, 1, 2, 4, 6], "veri": [0, 2, 4, 6], "impress": 0, "cheat": [0, 1], "now": [0, 1, 2, 3, 4, 5, 6, 7], "game": 0, "all": [0, 1, 2, 3, 4, 5, 6], "left": [0, 1, 2, 3, 4, 5, 6], "rule": [0, 2, 4, 5, 6], "complementari": 0, "companion": [0, 1], "prove": [0, 2, 3, 4, 5, 6, 10], "which": [0, 1, 2, 3, 4, 5, 6, 7], "thorough": 0, "underli": [0, 1, 5], "logic": [0, 1, 3, 4, 5, 10], "framework": 0, "core": [0, 4, 5], "syntax": [0, 1, 3, 4], "peopl": [0, 1], "who": [0, 6], "prefer": [0, 1, 3], "user": [0, 2], "manual": [0, 3, 4], "befor": [0, 1, 2, 3, 4, 5], "new": [0, 1, 2, 3, 4, 5, 6], "dishwash": 0, "person": 0, "hit": [0, 1], "button": [0, 1], "figur": [0, 1, 2, 5], "out": [0, 1, 2, 3, 4, 5, 6], "activ": 0, "potscrubb": 0, "featur": [0, 1, 2, 4], "later": [0, 1, 2, 4, 5, 6], "sens": [0, 2, 3, 4, 5, 6], "here": [0, 1, 2, 3, 4, 5, 6], "refer": [0, 1, 2, 4, 5, 6], "back": [0, 1, 2, 3, 5, 6], "necessari": [0, 2, 4, 5], "anoth": [0, 1, 2, 3, 4, 5, 6], "thing": [0, 1, 2, 3, 4, 5, 6], "distinguish": [0, 5, 6], "place": [0, 1, 2, 5, 6], "greater": [0, 1, 2, 3, 4, 6], "emphasi": 0, "tactic": [0, 1, 2, 3, 4, 5, 6], "given": [0, 1, 2, 3, 4, 5, 6], "two": [0, 1, 2, 3, 4, 5, 6], "wai": [0, 1, 2, 3, 4, 5, 6], "down": [0, 3, 4, 6], "themselv": [0, 4, 5], "suitabl": [0, 1, 2, 5, 6], "descript": [0, 1, 2, 4, 6], "thereof": 0, "For": [0, 1, 2, 3, 4, 5, 6], "repres": [0, 1, 2, 3, 4, 5], "fact": [0, 2, 3, 4, 5, 6, 10], "even": [0, 1, 2, 3, 4, 5, 6], "m": [0, 1, 2, 4, 6], "nat": [0, 1, 2, 3, 4, 5, 6], "fun": [0, 2, 3, 4, 5, 6], "k": [0, 2, 4, 5, 6], "hk": 0, "hmn": 0, "rw": [0, 1, 2, 3, 4, 5, 6], "mul_add": [0, 1, 4], "l": [0, 1], "compress": [0, 1, 6], "singl": [0, 1, 2, 3, 4, 5], "instead": [0, 1, 2, 3, 4, 5, 6], "style": [0, 1], "same": [0, 1, 2, 3, 4, 5, 6], "sai": [0, 1, 2, 3, 4, 5, 6], "natur": [0, 1, 2, 3, 4, 5, 6], "rintro": [0, 2, 3, 4, 5, 6], "need": [0, 1, 2, 3, 4, 5, 6], "twice": [0, 6], "let": [0, 1, 2, 3, 4, 5, 6], "substitut": [0, 2], "obviou": [0, 4, 5], "ring": [0, 1, 2, 3, 4, 5], "As": [0, 1, 2, 3, 4, 5, 6], "enter": [0, 1, 2, 3, 6], "displai": [0, 1, 2], "state": [0, 1, 2, 3, 4, 6], "separ": [0, 1, 2, 4, 5], "tell": [0, 2, 3, 4, 5], "what": [0, 1, 2, 3, 4, 5, 6], "establish": [0, 1, 2, 3, 4, 5], "task": [0, 2, 4, 5, 6], "remain": [0, 1, 2, 3, 5, 6], "replai": 0, "step": [0, 1, 2, 3, 4, 5], "sinc": [0, 1, 2, 3, 4, 5, 6], "continu": [0, 1, 4, 5], "point": [0, 1, 2, 3, 5, 6], "see": [0, 1, 2, 3, 4, 5, 6], "first": [0, 1, 2, 3, 4, 5, 6], "introduc": [0, 1, 2, 3, 4, 6], "could": [0, 1, 2, 4, 5, 6], "renam": 0, "decompos": [0, 3, 5], "hypothesi": [0, 1, 2, 3, 4], "assumpt": [0, 1, 2, 3, 4, 5, 6], "second": [0, 1, 2, 3, 4, 5, 6], "declar": [0, 1, 4, 5], "next": [0, 1, 2, 3, 4, 5, 6, 7], "rewrit": [0, 1, 2, 3, 4, 5, 6], "replac": [0, 1, 2, 3, 4], "solv": [0, 1, 2, 3, 4, 5, 6], "result": [0, 1, 2, 3, 4, 5, 6], "abil": 0, "small": [0, 4, 5, 6], "increment": [0, 1], "extrem": [0, 6], "power": [0, 2, 3, 4, 5], "reason": [0, 1, 2, 4, 5, 6], "easier": [0, 1, 3, 4, 6], "quicker": 0, "than": [0, 1, 2, 3, 4, 5, 6], "There": [0, 1, 2, 3, 4, 6], "isn": [0, 2, 3, 4], "sharp": 0, "distinct": [0, 2, 3, 4, 5, 6], "between": [0, 1, 2, 3, 4, 5, 6], "insert": [0, 2, 4, 5, 6], "did": [0, 2, 6], "phrase": [0, 1, 2, 4, 5], "mul_left_comm": [0, 4], "abov": [0, 1, 2, 3, 4, 5, 6], "convers": [0, 1, 2, 4, 6], "short": [0, 1, 2, 3, 4, 5], "middl": [0, 1, 2, 6], "That": [0, 4, 5], "said": [0, 2, 4, 5], "reduc": [0, 2, 3, 4, 5], "liner": 0, "carri": [0, 1, 2, 3, 4, 5, 6], "But": [0, 1, 2, 3, 4, 5, 6], "substanti": 0, "autom": [0, 1, 5], "justifi": [0, 1, 2, 6], "longer": [0, 4, 5], "calcul": [0, 2, 4, 5, 10], "bigger": [0, 3], "inferenti": 0, "invok": [0, 1, 6], "simplifi": [0, 2, 3, 4, 5, 6], "specif": [0, 1, 3, 4, 5], "pariti": [0, 4], "automat": [0, 1, 2, 3, 4, 5, 6], "intro": [0, 1, 2, 3, 4, 5, 6], "simp": [0, 2, 3, 4, 5, 6], "parity_simp": 0, "big": [0, 5, 6], "differ": [0, 1, 2, 3, 4, 5, 6], "onli": [0, 1, 2, 3, 4, 5, 6], "its": [0, 1, 2, 3, 4, 5, 6], "built": [0, 2], "wherea": [0, 1, 3, 5, 6], "top": [0, 6], "meant": [0, 1, 2], "contain": [0, 2, 3, 4, 5, 6], "extens": [0, 1, 6], "document": [0, 1, 3, 4], "rather": [0, 1, 2, 4, 5, 6], "think": [0, 1, 2, 3, 4, 5, 6], "comfort": [0, 2], "brows": [0, 1, 4], "frustrat": 0, "curv": 0, "steep": 0, "newcom": 0, "avail": [0, 4, 5], "round": [0, 1, 5], "clock": 0, "doubt": 0, "soon": [0, 2, 6], "enough": [0, 1, 2, 3, 4, 6], "too": [0, 1, 3, 5, 6], "contribut": [0, 3], "develop": [0, 1, 4], "mission": 0, "dive": 0, "come": [0, 1, 2, 3, 4, 5, 6], "forewarn": 0, "fundament": [0, 4, 5], "life": [0, 2], "mai": [0, 1, 2, 3, 5, 6], "never": 0, "acknowledg": 0, "grate": [0, 5], "gabriel": 0, "ebner": 0, "set": [0, 1, 2, 4, 5, 7, 10], "infrastructur": 0, "scott": 0, "morrison": 0, "mario": 0, "carneiro": 0, "help": [0, 1, 2, 3, 4, 5, 6], "port": 0, "bryan": 0, "gin": 0, "ge": [0, 2, 5], "chen": 0, "johan": 0, "commelin": 0, "mathieu": 0, "guai": 0, "paquet": 0, "julian": 0, "k\u00fclshammer": 0, "giovanni": 0, "mascellani": 0, "hunter": 0, "monro": 0, "pietro": 0, "monticon": 0, "bartosz": 0, "piotrowski": 0, "guilherm": 0, "silva": 0, "been": [0, 1, 2, 4, 5], "partial": [0, 1, 2, 3, 5], "hoskinson": 0, "center": [0, 6], "nut": 1, "bolt": 1, "appli": [1, 2, 3, 4, 5, 6], "gener": [1, 2, 3, 4, 5, 6], "without": [1, 2, 4, 5, 6], "when": [1, 2, 3, 4, 5, 6], "net": 1, "hand": [1, 2, 3, 4, 5, 6], "side": [1, 2, 3, 4, 5, 6], "equal": [1, 2, 3, 4, 5, 6], "right": [1, 2, 3, 4, 5, 6], "tantamount": [1, 3], "name": [1, 2, 3, 4, 5, 6], "abbrevi": [1, 2, 3, 5], "b": [1, 2, 3, 4, 5, 6], "c": [1, 2, 4, 5, 6], "real": [1, 2, 3, 4, 5, 6, 7], "mul_assoc": [1, 2, 4, 5], "mul_comm": [1, 2, 4, 5], "elimin": 1, "explicitli": [1, 2, 3, 5, 6], "purpos": [1, 2, 3, 4, 5, 6], "illustr": [1, 2, 3, 4, 5], "multipl": [1, 2, 3, 4, 5], "written": [1, 2, 3, 4, 5, 6], "howev": [1, 2, 5, 6], "good": [1, 2, 3, 4, 5, 6], "mind": [1, 2, 5], "notat": [1, 2, 3, 4, 5, 6], "convent": [1, 5], "parenthes": [1, 2, 3, 4], "\u211d": [1, 2, 3, 5, 6], "import": [1, 2, 3, 4, 5, 6], "begin": [1, 2, 3, 4, 5], "sake": [1, 4], "breviti": [1, 5], "suppress": 1, "repeat": [1, 4, 5], "full": [1, 3, 4, 5, 6], "process": [1, 3], "chang": [1, 2, 4, 5, 6], "happen": [1, 6], "charact": [1, 3], "r": [1, 2, 4, 5, 6], "symbol": [1, 2, 5], "doesn": [1, 2, 6], "appear": [1, 2, 5, 6], "until": [1, 2, 4, 5, 6], "space": [1, 3, 5, 10], "tab": [1, 2, 3, 4], "kei": [1, 4, 5, 6], "keyboard": 1, "easili": [1, 4, 5], "access": [1, 3, 5, 6], "backslash": [1, 3], "lead": [1, 2, 4, 5, 6], "input": [1, 3, 6], "leader": 1, "report": 1, "current": [1, 2], "infoview": 1, "move": [1, 2, 6], "A": [1, 2, 3, 4, 5, 6], "typic": 1, "might": [1, 2, 3, 4, 5], "1": [1, 2, 3, 4, 5, 6], "h\u2081": [1, 2, 3, 4], "prime": [1, 2, 3, 5, 10], "h\u2082": [1, 3, 4], "h\u2083": [1, 3], "denot": [1, 3, 4, 6], "context": [1, 2, 4, 5, 6], "plai": [1, 3, 4, 6], "three": [1, 2, 4, 5, 6], "label": [1, 2], "everyth": [1, 2, 6], "identifi": [1, 2, 4], "subscript": 1, "h": [1, 2, 3, 4, 5, 6], "legal": 1, "would": [1, 2, 3, 4, 5, 6], "h1": [1, 3, 4], "h2": [1, 3], "h3": 1, "foo": [1, 3, 5], "bar": [1, 2], "baz": 1, "last": [1, 2, 3, 4, 5, 6], "sometim": [1, 2, 3, 4, 5, 6], "target": [1, 6], "combin": [1, 2, 5, 6], "practic": [1, 2, 3, 6], "intend": [1, 2, 5], "mean": [1, 2, 3, 4, 5, 6], "usual": [1, 2, 3, 4, 5, 6], "clear": [1, 2, 4, 5], "case": [1, 2, 3, 4, 5, 6], "With": [1, 3, 4, 6], "arrow": [1, 2, 6], "revers": [1, 2, 3, 5, 6], "argument": [1, 2, 3, 4, 5, 6], "tri": [1, 2, 4], "match": [1, 2, 5], "pattern": [1, 2, 3, 5], "local": [1, 2, 6], "d": [1, 2, 4, 5], "e": [1, 2, 3, 4, 5, 6], "hyp": 1, "sub_self": [1, 2], "list": [1, 2, 3, 4, 5], "relev": [1, 2, 4, 5, 6], "within": [1, 2, 6], "squar": [1, 2, 4, 5], "bracket": [1, 2, 5], "still": [1, 2, 3, 4, 5, 6], "progress": [1, 5], "after": [1, 2, 4, 6], "comma": 1, "trick": [1, 2, 4], "variabl": [1, 2, 3, 4, 5, 6], "onc": [1, 2, 3, 4, 5, 6], "outsid": [1, 4], "mention": [1, 2, 3, 5, 6], "g": [1, 2, 3, 5, 6], "inspect": 1, "reveal": 1, "inde": [1, 5, 6], "delimit": 1, "scope": [1, 2, 3, 5], "end": [1, 2, 3, 4, 5, 6], "block": [1, 4], "final": [1, 2, 3, 5, 6], "recal": [1, 2, 4, 5, 6], "introduct": [1, 2, 6, 10], "determin": [1, 5, 6], "both": [1, 2, 3, 4, 5, 6], "expect": [1, 2, 3, 4, 5, 6], "rais": [1, 4], "error": [1, 2, 3], "explain": [1, 2, 3, 4, 5, 6], "output": 1, "meanwhil": [1, 4], "two_mul": [1, 5], "add_mul": 1, "distribut": [1, 4, 5], "addit": [1, 2, 4, 5, 6], "add_assoc": [1, 4, 5], "precis": [1, 3, 6], "possibl": [1, 2, 3, 4, 5, 6], "calc": [1, 2, 3, 6], "keyword": [1, 2, 4, 5], "notic": [1, 2, 3, 4, 5, 6], "finicki": 1, "dot": [1, 6], "underscir": 1, "justif": [1, 2], "format": 1, "indic": [1, 2, 3, 5], "indent": 1, "One": [1, 2, 3, 4, 5, 6], "outlin": [1, 2, 4, 6], "modulo": [1, 4, 5], "individu": 1, "pure": [1, 6], "littl": [1, 2, 6], "underneath": [1, 3], "pow_two": [1, 4, 5], "mul_sub": 1, "add_sub": 1, "sub_sub": 1, "add_zero": [1, 5], "perform": [1, 2, 3], "exact": [1, 2, 3, 4, 5, 6], "becaus": [1, 2, 3, 4, 5, 6], "exactli": [1, 2, 3, 5, 6], "close": [1, 2, 3], "note": [1, 2, 4, 5, 6], "bit": [1, 4, 6], "commut": [1, 2, 3, 4, 5], "indirectli": 1, "data": [1, 2, 4, 5, 6], "similar": [1, 2, 3, 5, 6], "common": [1, 2, 3, 4, 5, 6], "variat": [1, 3, 4, 5, 6], "call": [1, 2, 3, 4, 5, 6], "nth_rewrit": 1, "allow": [1, 2, 3, 4, 5, 6], "particular": [1, 2, 5, 6], "instanc": [1, 2, 3, 4, 5, 6], "enumer": [1, 2], "start": [1, 2, 3, 4, 6, 7, 10], "zero": [1, 2, 3, 4, 5, 6], "occurr": 1, "nth_rw": 1, "nth_rewrite_lh": 1, "nth_rewrite_rh": 1, "sophist": [1, 6], "subexpress": 1, "consist": [1, 3, 5, 6], "collect": [1, 3, 5, 6], "oper": [1, 2, 3, 4, 5, 6], "time": [1, 4, 5, 6], "constant": [1, 2], "mapsto": [1, 5], "abelian": [1, 5], "negat": [1, 5, 10], "invers": [1, 3, 5], "axiom": [1, 3, 5, 6], "add_comm": [1, 4, 5], "zero_add": [1, 4, 5], "add_left_neg": [1, 5], "mul_on": [1, 5], "one_mul": [1, 2, 5], "being": [1, 3, 5, 6], "suffic": [1, 2, 3, 6], "give": [1, 2, 3, 4, 6], "element": [1, 2, 3, 4, 5, 6], "concret": [1, 2, 4, 5, 6], "integ": [1, 2, 4, 10], "abstract": [1, 2, 6, 10], "character": [1, 3, 4, 6], "axiomat": [1, 2, 3, 5], "train": 1, "recogn": [1, 2, 4, 5, 6], "appropri": [1, 2, 3, 5], "\u2124": [1, 4, 5], "ration": [1, 2, 4, 6], "\u211a": [1, 4, 6], "\u2102": [1, 5], "extend": [1, 3, 4, 5, 6], "Not": [1, 5, 6], "properti": [1, 2, 3, 4, 5, 6], "hold": [1, 2, 3, 4, 5, 6], "arbitrari": [1, 2, 3, 4, 5], "taken": [1, 2], "cours": [1, 2, 4, 6], "linear": [1, 2, 5, 6], "matric": [1, 5], "fail": [1, 2, 3, 4, 5, 6], "commr": [1, 2, 5], "unchang": [1, 2], "linarith": [1, 2, 4, 5], "permiss": 1, "strike": [1, 2], "balanc": 1, "concis": [1, 5], "readabl": [1, 2, 3, 4, 6], "strengthen": [1, 2, 4], "skill": [1, 2, 3, 4], "deriv": [1, 2, 4, 7], "most": [1, 2, 3, 4, 5, 6], "content": [1, 4, 6], "organiz": 1, "mechan": [1, 2, 5], "namespac": [1, 2, 3, 4, 5, 6], "shorter": [1, 3, 4, 6], "avoid": [1, 3, 4, 5], "due": [1, 3], "clash": 1, "myre": 1, "add_right_neg": 1, "effect": [1, 3, 6], "temporarili": [1, 2], "reprov": 1, "care": [1, 2, 3, 5], "earlier": 1, "pai": [1, 2, 6], "attent": [1, 2, 4, 6], "curli": [1, 2], "implicit": [1, 2, 5, 6], "moment": [1, 2, 5], "worri": [1, 3, 4, 5], "neg_add_cancel_left": 1, "add_neg_cancel_right": 1, "add_left_cancel": 1, "add_right_cancel": 1, "plan": [1, 6], "brace": 1, "imagin": 1, "situat": [1, 3, 6], "draw": [1, 5], "conclus": [1, 2, 4], "hypothes": [1, 2, 3, 4, 5], "redund": [1, 5, 6], "few": [1, 2, 3, 4, 6], "extra": [1, 2, 3, 5, 6], "oner": 1, "complic": [1, 2], "tediou": [1, 2], "mark": [1, 2, 6], "suppos": [1, 2, 3, 4, 5, 6], "infer": [1, 2, 3, 5], "mul_zero": [1, 5], "serv": [1, 3, 4, 5], "therefor": [1, 4, 5, 6], "promot": 1, "modular": 1, "subproof": 1, "wa": [1, 3], "except": [1, 5], "ad": [1, 2, 3, 4, 5, 6], "free": [1, 6], "At": [1, 2, 4, 5], "rememb": [1, 2, 3, 4, 5, 6], "zero_mul": [1, 2, 4, 5], "By": [1, 3, 5], "neg_eq_of_add_eq_zero": 1, "eq_neg_of_add_eq_zero": 1, "neg_zero": 1, "neg_neg": 1, "had": 1, "annot": [1, 3, 4, 5], "third": [1, 2, 3, 5, 6], "specifi": [1, 2, 3, 4, 5, 6], "imposs": 1, "default": [1, 2, 3, 4, 5], "subtract": [1, 4, 5], "provabl": [1, 3, 6], "sub_eq_add_neg": [1, 5], "On": [1, 2, 3, 5, 6], "defin": [1, 2, 3, 4, 5, 6], "reflex": [1, 2], "present": [1, 2, 4, 6], "forc": [1, 2, 3], "unfold": [1, 2, 3, 4, 5, 6], "refl": [1, 2, 3, 5], "deal": [1, 2, 3, 4, 5, 6], "equat": [1, 2, 3, 4, 5], "interchang": 1, "self_sub": 1, "either": [1, 2, 3, 5, 6], "effort": [1, 4], "one_add_one_eq_two": 1, "norm_num": [1, 2, 4, 5], "strength": 1, "weaker": [1, 2], "notion": [1, 2, 3, 4, 5, 6, 7], "addgroup": 1, "otherwis": [1, 2, 3, 4, 5], "variant": [1, 2, 6], "addcommgroup": 1, "commgroup": 1, "mul_left_inv": [1, 5], "\u00b9": [1, 3, 5, 6], "feel": [1, 2, 6], "cocki": 1, "helper": 1, "along": [1, 4, 6], "hint": [1, 2], "mul_right_inv": [1, 5], "mul_inv_rev": 1, "non": [1, 3, 6], "abel": 1, "noncomm_r": 1, "seem": [1, 2, 4, 6], "odd": [1, 2, 3, 4], "partli": 1, "histor": 1, "conveni": [1, 2, 3, 5, 6], "great": [1, 5], "sort": [1, 3, 4], "inequ": [1, 2, 6], "le": [1, 5], "whenev": [1, 2, 4, 5], "consid": [1, 2, 3, 4, 5, 6, 7], "le_refl": [1, 2], "le_tran": [1, 2, 5], "detail": [1, 2, 3, 4, 5], "unless": [1, 2, 5], "realli": [1, 2, 3, 4, 6], "insist": 1, "discuss": [1, 2, 4, 5, 6], "implic": [1, 6, 10], "h\u2080": [1, 2, 3, 4, 6], "creat": 1, "option": [1, 2, 4, 5, 6], "visibl": 1, "must": [1, 5, 6], "complet": [1, 2, 3, 4], "decreas": [1, 5], "fourth": [1, 2], "mode": [1, 2, 5], "entir": [1, 3, 5, 6], "lt_of_le_of_lt": [1, 2, 5], "lt_of_lt_of_l": 1, "lt_tran": [1, 2], "togeth": [1, 2, 3, 4, 5, 6], "handl": [1, 3, 4], "arithmet": 1, "5": [1, 2, 5, 6], "pass": [1, 5], "exp_le_exp": 1, "mpr": [1, 2, 5, 6], "exp": [1, 3], "applic": [1, 2, 4, 5], "function": [1, 2, 4, 5, 7, 10], "compound": [1, 2, 6], "pars": [1, 3], "exp_lt_exp": 1, "log_le_log": 1, "log": [1, 3], "log_lt_log": 1, "add_le_add": [1, 2, 5], "add_le_add_left": 1, "add_le_add_right": 1, "add_lt_add_of_le_of_lt": 1, "add_lt_add_of_lt_of_l": 1, "add_lt_add_left": 1, "add_lt_add_right": 1, "add_nonneg": [1, 5], "add_po": 1, "add_pos_of_pos_of_nonneg": 1, "exp_po": [1, 3], "bi": [1, 5, 10], "lr": 1, "iff": [1, 3, 6], "connect": [1, 3, 5, 6], "equival": [1, 2, 3, 4, 5, 6], "mp": [1, 2, 3, 4, 6], "forward": [1, 2, 5, 6], "direct": [1, 2, 3, 6], "stand": [1, 2, 5, 6], "modu": 1, "ponen": 1, "respect": [1, 2, 3, 4, 5, 6], "thu": [1, 3, 4, 5, 6], "again": [1, 2, 3, 4, 5, 6], "numer": [1, 4, 5], "constitut": 1, "part": [1, 2, 3, 4, 5, 6], "strategi": [1, 2, 4], "api": 1, "reli": [1, 2, 3, 5, 6], "guess": [1, 2, 3, 4, 5], "a_of_b_of_c": 1, "approxim": 1, "loud": 1, "probabl": [1, 5, 6], "add_l": 1, "choic": [1, 2, 3, 5, 6], "exist": [1, 2, 3, 6], "jump": [1, 4, 5, 6], "nearbi": [1, 4], "library_search": [1, 4], "sq_nonneg": 1, "delet": [1, 2, 3, 4], "uncom": 1, "previou": [1, 2, 3, 5, 6], "suggest": [1, 2, 4, 5, 6], "long": [1, 2, 3, 5], "better": [1, 3, 4, 5, 6], "confirm": [1, 2, 3, 4], "finish": [1, 2, 3, 4], "job": 1, "pow_two_nonneg": [1, 2], "tend": [1, 6], "around": [1, 3, 6], "binari": [1, 2, 4, 5], "increas": 1, "worth": [1, 2, 5], "definition": [1, 4, 5, 6], "principl": [1, 2, 3, 4], "favor": [1, 2, 5], "timesav": 1, "clever": 1, "involv": [1, 2, 4, 5, 6], "nice": [1, 2, 4, 6], "idea": [1, 2, 3, 5, 6], "abs_l": [1, 5], "ab": [1, 2, 5], "congratul": [1, 2, 4], "becom": [1, 4, 5, 6], "min": [1, 2, 6], "uniqu": [1, 2, 3, 4, 5, 6], "min_le_left": 1, "min_le_right": 1, "le_min": 1, "max": [1, 2, 6], "pair": [1, 2, 4, 5, 6], "act": 1, "curri": 1, "logician": 1, "haskel": 1, "get": [1, 2, 3, 4, 6, 10], "bind": [1, 3], "tighter": [1, 3], "infix": 1, "le_antisymm": [1, 2], "less": [1, 2, 3, 4, 5, 6], "usag": 1, "inconsist": 1, "outer": 1, "level": [1, 2], "nest": [1, 2], "maintain": 1, "bother": [1, 3], "repetit": 1, "foreshadow": 1, "univers": [1, 3, 5, 6, 10], "quantifi": [1, 3, 4, 5, 6, 10], "desir": [1, 3, 6], "implicitli": [1, 2], "mani": [1, 2, 3, 5, 6, 10], "whether": [1, 2, 3, 4, 6], "Of": [1, 2, 4, 6], "interest": [1, 2, 3, 5, 6], "vice": [1, 3], "versa": [1, 3], "word": [1, 2, 3, 4, 5, 6], "switch": 1, "transit": [1, 2, 5, 6], "total": 1, "satisfi": [1, 3, 4, 5, 6], "disjunct": [1, 3, 10], "stick": [1, 2, 6, 7], "split": [1, 2, 3, 4], "aux": [1, 2, 4, 6], "valu": [1, 2, 3, 4, 5, 6], "yield": [1, 2, 3, 4, 5, 6], "made": [1, 2, 3, 5, 6], "manifest": [1, 6], "triangl": [1, 2, 5], "abs_add": [1, 2], "sub_add_cancel": [1, 5], "relat": [1, 2, 3, 5, 6], "ordinari": [1, 2, 4, 5, 6], "unicod": [1, 3], "obtain": [1, 2, 4, 5, 6], "dvd": 1, "dvd_tran": 1, "dvd_mul_of_dvd_left": 1, "dvd_mul_left": 1, "expon": 1, "expand": [1, 2, 3, 4, 5], "w": 1, "greatest": [1, 5, 6], "divisor": [1, 2, 4, 5], "gcd": [1, 2, 4], "least": [1, 5, 6], "lcm": 1, "analog": [1, 2, 3, 4, 5, 6], "divid": [1, 2, 4, 5], "gcd_zero_right": 1, "gcd_zero_left": 1, "lcm_zero_right": 1, "lcm_zero_left": 1, "similarli": [1, 2, 3, 4, 5], "prefix": [1, 4], "dvd_antisymm": 1, "complain": 1, "ambigu": [1, 5], "_root_": 1, "saw": [1, 5, 6], "govern": [1, 5], "class": [1, 4, 5, 6, 7], "describ": [1, 2, 3, 4, 5, 6], "\u03b1": [1, 2, 3, 4, 5, 6], "partialord": [1, 2], "adopt": 1, "letter": [1, 5], "\u03b2": [1, 2, 3, 5, 6], "\u03b3": [1, 2, 5, 6], "greek": [1, 4], "especi": [1, 5, 6], "strict": [1, 2], "somewhat": [1, 3, 6], "lt_irrefl": [1, 2], "lt_iff_le_and_n": 1, "lattic": [1, 5, 6], "inf_le_left": [1, 6], "inf_le_right": 1, "le_inf": 1, "le_sup_left": 1, "le_sup_right": 1, "sup_l": 1, "lower": [1, 2, 4], "bound": [1, 2, 3, 4, 5, 6], "upper": [1, 2], "glb": 1, "lub": 1, "infimum": [1, 6], "supremum": [1, 4], "inf": [1, 6], "sup": [1, 4, 6], "further": [1, 6], "matter": [1, 2], "meet": [1, 2, 3, 5], "join": [1, 5], "keep": [1, 5], "dictionari": 1, "subset": [1, 2, 3, 5, 6], "domain": [1, 2, 3, 4, 5, 6], "boolean": 1, "truth": [1, 4], "fals": [1, 2, 3, 4], "true": [1, 2, 3, 6], "posit": [1, 3, 4, 5, 6], "subspac": 1, "vector": [1, 3], "intersect": [1, 3, 5, 6], "sum": [1, 2, 4, 5, 6], "inclus": [1, 3, 6], "topolog": [1, 5, 10], "union": [1, 3, 4, 5], "inf_comm": 1, "inf_assoc": 1, "sup_comm": 1, "sup_assoc": 1, "absorpt": 1, "law": 1, "absorb1": 1, "absorb2": 1, "found": [1, 5], "inf_sup_self": 1, "sup_inf_self": 1, "distriblattic": 1, "inf_sup_left": 1, "inf_sup_right": 1, "sup_inf_left": 1, "sup_inf_right": 1, "shown": [1, 5], "explicit": [1, 2, 5, 6], "nondistribut": 1, "finit": [1, 3, 4, 5, 6], "impli": [1, 2, 3, 4, 5, 6], "larger": [1, 6], "carrier": [1, 5], "compat": [1, 6], "strictorderedr": 1, "mul_po": [1, 4], "mul_nonneg": 1, "coupl": [1, 2, 6], "metric": [1, 5, 10], "equip": [1, 3, 5, 6], "distanc": [1, 2, 6], "dist": [1, 6], "map": [1, 2, 3, 5, 6], "metricspac": [1, 6], "dist_self": 1, "dist_comm": [1, 6], "dist_triangl": [1, 6], "nonneg": [1, 5], "nonneg_of_mul_nonneg_left": 1, "dist_nonneg": [1, 6], "dealt": 2, "basic": [2, 4, 5, 6, 10], "simpl": [2, 4, 5], "absolut": 2, "\u03b5": [2, 6], "though": [2, 3, 4, 5], "treat": [2, 3, 5, 6], "my_lemma": 2, "\u03b4": [2, 6], "hb": [2, 6], "subsequ": [2, 4, 6], "lemma": [2, 4, 5, 6, 10], "my_lemma2": 2, "stage": [2, 5], "my_lemma3": 2, "epo": 2, "ele1": 2, "xlt": 2, "ylt": 2, "essenti": [2, 3, 5, 6], "colon": 2, "why": [2, 4, 6], "off": [2, 3, 4], "my_lemma4": 2, "abs_mul": 2, "mul_le_mul": 2, "abs_nonneg": 2, "mul_lt_mul_right": 2, "extract": [2, 6], "hidden": 2, "expos": [2, 6], "predic": [2, 3, 4, 6], "fn_ub": 2, "fn_lb": 2, "fnub": 2, "fnlb": 2, "hfa": 2, "hgb": 2, "dsimp": [2, 3, 4, 5], "simplif": [2, 3, 4], "contract": 2, "anyhow": 2, "control": 2, "transform": [2, 3], "rest": [2, 3, 5, 6], "routin": 2, "nnf": 2, "nng": 2, "hfb": 2, "nna": 2, "order": [2, 3, 4, 5, 6, 10], "codomain": [2, 4, 6], "structur": [2, 4, 6, 10], "monoid": [2, 3, 4], "fn_ub_add": 2, "orderedcanceladdcommmonoid": 2, "high": 2, "monoton": [2, 6], "nondecreas": [2, 4], "placehold": 2, "Or": [2, 3], "backward": [2, 6], "subgoal": 2, "mf": 2, "mg": 2, "aleb": 2, "lambda": [2, 5], "underscor": [2, 3], "flag": [2, 3], "squiggli": 2, "marker": 2, "nnc": 2, "bbb": [2, 5], "fneven": 2, "fnodd": 2, "ef": 2, "eg": 2, "og": 2, "shorten": 2, "rid": 2, "won": [2, 4, 6], "cannot": [2, 3, 4, 5, 6], "contrari": 2, "syntact": 2, "reduct": [2, 3], "erw": 2, "harder": 2, "spot": 2, "rudimentari": 2, "foundat": [2, 3, 4, 5], "impos": 2, "restrict": [2, 3, 4, 6], "talk": [2, 4, 6], "assert": [2, 3], "ask": [2, 4, 5, 6], "xs": [2, 3], "tran": [2, 4, 5], "setub": 2, "inject": [2, 3, 4, 6], "x_1": [2, 3], "x_2": [2, 3], "x\u2081": [2, 3, 5, 6], "x\u2082": [2, 3, 5], "add": [2, 4, 5, 6], "nonzero": [2, 4, 5], "add_left_inj": 2, "composit": [2, 3, 5, 6], "injg": 2, "injf": [2, 3], "canon": [2, 3, 4, 5], "exhibit": [2, 6], "anonym": [2, 3, 4, 5], "constructor": [2, 3, 4, 5], "angl": 2, "whatev": [2, 4], "certain": [2, 6], "fnhasub": 2, "fnhaslb": 2, "fnub_add": 2, "gun": 2, "ubf": 2, "ubg": 2, "ubfa": 2, "ubfb": 2, "unpack": [2, 3], "claus": 2, "whose": [2, 4, 5, 6], "els": [2, 3, 4], "turn": [2, 3, 4, 5, 6, 7], "directli": [2, 4, 5, 6], "lbf": 2, "lbg": 2, "cousin": 2, "rcase": [2, 3, 4, 5, 6], "flexibl": [2, 6], "recurs": [2, 3, 5, 10], "harm": [2, 3], "swiss": 2, "armi": 2, "knive": 2, "wide": 2, "old": [2, 5], "chestnut": 2, "product": [2, 4, 5, 6], "magic": [2, 5], "verifi": 2, "sumofsquar": 2, "sumofsquares_mul": 2, "sosx": 2, "sosi": 2, "xeq": [2, 3], "yeq": 2, "insight": 2, "motiv": 2, "gaussian": [2, 10], "i": [2, 3, 4, 5, 6], "sqrt": [2, 3, 4, 5], "norm": [2, 5, 6], "reflect": 2, "di": [2, 5], "xy": [2, 5], "cryptic": 2, "easiest": [2, 4], "perspicu": 2, "divis": [2, 4, 5, 10], "divab": 2, "divbc": 2, "beq": 2, "ceq": 2, "And": [2, 4, 6], "pretti": [2, 6], "Then": [2, 3, 5, 6], "divac": 2, "alpha": [2, 3], "beta": [2, 3], "surject": [2, 3, 6], "yourself": [2, 5], "field_simp": [2, 5], "denomin": [2, 4, 5], "div_mul_cancel": 2, "hx": [2, 3, 5], "method": [2, 3, 4, 5], "surjg": 2, "surjf": [2, 3], "strictli": 2, "contradict": [2, 3, 4], "speak": [2, 5, 6], "irreflex": 2, "asymmetri": 2, "lt_asymm": 2, "sugar": 2, "eventu": [2, 3, 6], "fnuba": 2, "not_le_of_gt": 2, "not_lt_of_g": [2, 4, 5], "lt_of_not_g": 2, "le_of_not_gt": 2, "snippet": [2, 4, 5], "counterexampl": 2, "monof": 2, "noth": [2, 3, 4, 5], "four": [2, 5], "valid": 2, "far": [2, 3, 6], "q": [2, 4, 5, 6], "straightforward": 2, "difficult": 2, "conclud": 2, "nonexist": 2, "contradictori": 2, "classic": [2, 3, 4], "by_contra": [2, 4], "not_not": 2, "front": 2, "push": [2, 4, 6], "inward": 2, "facilit": [2, 6], "push_neg": [2, 3, 4], "restat": 2, "contrapos": [2, 3, 4], "yet": [2, 3, 4, 5, 6], "semicolon": [2, 4], "falso": 2, "anyth": [2, 5, 6], "elim": 2, "strang": [2, 4], "fairli": 2, "reach": 2, "37": 2, "exfalso": 2, "absurd": [2, 4], "slick": 2, "drop": 2, "manner": [2, 5], "contrast": [2, 3, 5, 6], "compon": [2, 3, 5, 6], "techniqu": [2, 6], "variou": [2, 3, 5], "xltz": 2, "zlty": 2, "10": 2, "7": [2, 4, 6], "behav": [2, 3, 6], "roughli": [2, 3, 4], "friend": [2, 5], "were": [2, 4, 5, 6], "inscrut": [2, 3], "gadget": [2, 6], "auxiliari": [2, 6], "pow_eq_zero": [2, 4], "doubl": [2, 3], "symmetr": [2, 3], "abs_lt": 2, "dvd_gcd_iff": 2, "8": [2, 4, 6], "6": [2, 4, 5, 6], "15": 2, "below": [2, 3, 4, 5, 6], "not_monotone_iff": 2, "antisymmetr": 2, "aris": 2, "preorder": [2, 6], "pre": 2, "lt_iff_le_not_l": 2, "beyond": 2, "repeatedli": [2, 6], "instanti": [2, 5, 6], "inl": [2, 3], "inr": [2, 3], "produc": 2, "branch": [2, 3], "le_or_gt": 2, "abs_of_nonneg": [2, 5], "abs_of_neg": 2, "immedi": [2, 3, 5], "myab": 2, "le_abs_self": [2, 5], "neg_le_abs_self": 2, "enjoi": [2, 3, 4, 6], "pun": 2, "lt_ab": 2, "genuin": 2, "vertic": [2, 5], "lt_trichotomi": 2, "xgt": 2, "dvd_mul_right": [2, 4], "eq_zero_or_eq_zero_of_mul_eq_zero": 2, "nontrivi": [2, 3, 4, 5, 6], "integr": [2, 7], "isdomain": 2, "em": [2, 3], "exclud": [2, 4], "by_cas": [2, 3, 4], "dispos": 2, "s_0": [2, 3], "s_1": 2, "s_2": 2, "ldot": [2, 3, 4], "varepsilon": [2, 6], "s_n": [2, 3], "render": [2, 4], "convergesto": 2, "ext": [2, 3, 4, 5], "enabl": [2, 3, 4, 5], "actual": [2, 3, 4, 6], "u": [2, 3, 5, 6], "v": [2, 3, 5, 6], "congr": 2, "reconcil": 2, "peel": 2, "convert": [2, 4], "quit": [2, 6], "zero_lt_on": [2, 4], "fill": [2, 3, 4, 5], "convergesto_const": 2, "\u03b5po": [2, 6], "nge": 2, "abs_zero": 2, "save": [2, 3], "troubl": [2, 3, 5], "pen": 2, "paper": [2, 3, 5, 6], "ns": 2, "nt": 2, "maximum": [2, 4, 6], "implement": [2, 5], "convergesto_add": 2, "cs": 2, "ct": 2, "\u03b52po": 2, "hs": [2, 4, 6], "ht": 2, "le_of_max_le_left": 2, "le_of_max_le_right": 2, "tricki": [2, 3, 4], "convergesto_mul_const": 2, "mulzeroclass": 2, "acpo": 2, "abs_po": 2, "independ": [2, 3, 5], "exists_abs_le_of_convergesto": 2, "strong": [2, 4], "n\u2080": 2, "bpo": [2, 6], "pos\u2080": 2, "div_po": 2, "n\u2081": 2, "convergesto_mul": 2, "sketch": [2, 3, 4, 6], "limit": [2, 6], "bold": 2, "scratch": 2, "convergesto_uniqu": 2, "sa": 2, "sb": 2, "abn": 2, "na": 2, "hna": 2, "nb": 2, "hnb": 2, "absa": 2, "absb": 2, "observ": [2, 4, 6], "everywher": [2, 3, 6], "linearord": 2, "vastli": 2, "awai": [2, 5], "vocabulari": 3, "uniform": [3, 6], "primit": 3, "conceptu": 3, "advantag": [3, 4, 5], "overload": 3, "verbos": 3, "system": [3, 4, 5], "wrong": 3, "theoret": [3, 6], "ss": 3, "sub": [3, 6], "cap": 3, "un": 3, "cup": 3, "univ": [3, 6], "empti": [3, 4, 5, 6], "member": [3, 6], "membership": [3, 4], "mem": 3, "notin": 3, "ident": [3, 4, 5, 6, 10], "databas": [3, 4, 6], "unlik": [3, 4], "existenti": [3, 10], "subset_def": 3, "inter_def": 3, "xu": 3, "mem_inter_iff": 3, "xsu": 3, "phenomenon": 3, "quirk": 3, "pitfal": 3, "heavili": [3, 6], "fall": 3, "union_def": 3, "mem_union": [3, 4], "xtu": 3, "xt": 3, "unnecessari": 3, "clearer": [3, 5], "correctli": 3, "special": [3, 4, 5, 6], "rewritten": 3, "diff_eq": 3, "mem_diff": 3, "xstu": 3, "xnt": 3, "xnu": 3, "extension": [3, 5], "unsurprisingli": 3, "dollar": 3, "sign": [3, 6], "and_comm": 3, "antisymm": 3, "hood": [3, 5], "builder": 3, "trivial": [3, 4, 6], "eq_two_or_odd": 3, "even_iff": 3, "confus": [3, 4, 6], "fortun": 3, "agre": 3, "prime_iff": 3, "symm": [3, 4, 5, 6], "rwa": [3, 4, 5], "signific": 3, "ball": 3, "bex": 3, "bex_def": 3, "prime_x": 3, "slight": 3, "ssubt": 3, "index": [3, 6], "model": [3, 6], "sequenc": [3, 6, 10], "a_0": 3, "a_1": 3, "a_2": 3, "mem_iunion": 3, "xai": 3, "mem_iint": 3, "mem_union\u2082": 3, "mem_inter\u2082": 3, "mem_iunion\u2082": 3, "exists_prime_and_dvd": 3, "eq_univ": 3, "eq_univ_of_foral": 3, "exists_infinite_prim": 3, "\u2080": 3, "sunion": 3, "sinter": 3, "relationship": [3, 4], "mem_iinter\u2082": 3, "sunion_eq_biunion": 3, "sinter_eq_biint": 3, "preimag": [3, 6], "imag": [3, 4, 6], "tripl": 3, "tag": 3, "mem_image_of_mem": 3, "galoi": [3, 5, 6], "image_subset_iff": 3, "represent": [3, 4, 5], "asid": 3, "raini": 3, "dai": 3, "behavior": [3, 6], "nonempti": [3, 6], "condit": [3, 4, 6], "fxeq": 3, "ai": 3, "fx": 3, "eq": [3, 5], "injon": 3, "theme": 3, "rel": [3, 5], "relativ": 3, "xpo": 3, "ypo": 3, "exp_log": 3, "ingredi": [3, 5, 6], "assign": [3, 5], "inhabit": [3, 5, 6], "appeal": 3, "choose_spec": 3, "some_spec": 3, "noncomput": [3, 5], "inverse_spec": 3, "dif_po": 3, "dif_neg": 3, "fulli": [3, 6], "alon": 3, "leftinvers": 3, "rightinvers": 3, "hack": 3, "half": 3, "dozen": 3, "condens": 3, "cantor": 3, "famou": 3, "miss": [3, 4], "j": [3, 5], "intuit": [3, 6], "cardin": 3, "biject": [3, 5], "nineteenth": 3, "centuri": 3, "infinit": [3, 6, 10], "dedekind": 3, "quickli": 3, "behind": 3, "problem": [3, 4, 5, 6], "shade": 3, "region": 3, "diagram": 3, "circ": [3, 5], "scale": 3, "inner": 3, "smaller": [3, 4, 6], "concentr": 3, "unshad": 3, "compos": [3, 5, 6], "disjoint": 3, "sound": [3, 5], "plausibl": 3, "delic": 3, "improv": [3, 4], "confid": 3, "invfun": [3, 5], "leftinverse_invfun": 3, "invfun_eq": 3, "sbaux": 3, "sbset": 3, "sb_aux": 3, "s_": 3, "sb_set": 3, "bigcup_": 3, "mathbb": [3, 4, 5], "sbfun": 3, "complement": [3, 6], "outermost": 3, "setminu": 3, "inv_fun": 3, "inv_fun_eq": 3, "sb_right_inv": 3, "goe": [3, 4, 5, 6], "henc": [3, 4, 5, 6], "neither": [3, 5], "nor": [3, 5], "sb_inject": 3, "hf": [3, 6], "hg": [3, 6], "a_def": 3, "h_def": 3, "hxeq": 3, "xa": [3, 5], "wlog": 3, "x\u2081a": 3, "resolve_left": 3, "x\u2082a": 3, "not_imp_self": 3, "x\u2082na": 3, "if_po": 3, "if_neg": 3, "x\u2082eq": 3, "hn": [3, 4, 6], "sb_fun": 3, "bring": [3, 4, 6], "tradeoff": 3, "encapsul": [3, 5], "symmetri": 3, "dwell": 3, "succ": [3, 4], "sb_surject": 3, "gya": 3, "xmem": 3, "sweet": 3, "schroeder_bernstein": 3, "substant": 4, "ancient": 4, "fraction": 4, "lowest": 4, "2c": 4, "4c": 4, "factor": [4, 5], "coprim": 4, "smart": 4, "12": 4, "encount": 4, "algebra": [4, 6, 10], "prime_def_lt": 4, "eq_one_or_self_of_dvd": 4, "prime_p": 4, "17": 4, "commonli": [4, 5], "prime_two": 4, "prime_thre": 4, "broader": [4, 7], "irreduc": [4, 5], "coincid": [4, 5, 6], "rise": 4, "dvd_mul": 4, "even_of_even_sqr": 4, "dvd_of_dvd_pow": 4, "proce": 4, "profici": 4, "ctrl": [4, 5], "search": [4, 5], "engin": 4, "hesit": 4, "mul_right_inj": 4, "heart": 4, "irration": 4, "dvd_gcd": 4, "coprime_mn": 4, "sqr_eq": 4, "meq": 4, "dvd_iff_exists_eq_mul_left": 4, "two_l": 4, "le_of_dvd": 4, "approach": [4, 5, 6], "quick": 4, "ne": [4, 5], "occur": 4, "suffici": [4, 6], "permut": 4, "prime_of_mem_factor": 4, "prod_factor": 4, "factors_uniqu": 4, "factorization_mul": 4, "mnez": 4, "nnez": 4, "factorization_pow": 4, "black": 4, "box": 4, "simpa": 4, "nnz": 4, "nsqr_nez": 4, "eq1": 4, "eq2": 4, "add_mul_mod_self_left": 4, "mul_mod_right": 4, "count_factors_mul_of_po": 4, "successor": 4, "succ_ne_zero": 4, "npow_nz": 4, "dvd_sub": 4, "pow_eq": 4, "npowz": 4, "add_sub_cancel": 4, "understood": [4, 6], "quotient": [4, 5, 6], "pictur": [4, 5], "mediat": 4, "headach": 4, "contend": 4, "issu": [4, 5, 6], "th": 4, "topic": 4, "enat": 4, "infin": [4, 6], "appreci": 4, "role": [4, 5, 6], "_section_induction_and_recurs": 4, "writ": 4, "datatyp": 4, "freeli": 4, "translat": [4, 6], "mathematician": [4, 6], "inj": 4, "factori": 4, "fac": 4, "ih": 4, "fac_po": 4, "succ_po": 4, "dvd_fac": 4, "ipo": 4, "il": 4, "of_le_succ": 4, "dvd_mul_of_dvd_right": 4, "crude": 4, "remaind": [4, 5], "pow_two_le_fac": 4, "finset": [4, 5, 6], "bigoper": [4, 5], "prod": [4, 6], "sum_range_zero": 4, "sum_range_succ": 4, "summat": 4, "prod_range_zero": 4, "prod_range_succ": 4, "deserv": 4, "comment": 4, "danger": [4, 5], "ordinarili": [4, 5], "loop": 4, "indefinit": 4, "fix": [4, 6], "placement": 4, "re": [4, 5], "handi": 4, "sum_id": 4, "div_eq_of_eq_mul_right": 4, "succ_eq_add_on": 4, "sum_sqr": 4, "mynat": 4, "thumb": 4, "decid": [4, 6], "preced": 4, "truncat": 4, "exponenti": 4, "cut": 4, "predecessor": 4, "pred": 4, "mul": [4, 5, 6], "succ_add": 4, "succ_mul": 4, "explor": [4, 6], "standard": [4, 5, 6], "formul": [4, 6], "quirki": 4, "among": 4, "annoi": 4, "h0": 4, "succ_le_succ": 4, "zero_l": [4, 5], "interval_cas": 4, "interv": [4, 6], "decis": 4, "procedur": 4, "revert": [4, 5], "minfac": 4, "smallest": [4, 6], "strong_induction_on": 4, "subsum": 4, "exists_prime_factor": 4, "np": 4, "mltn": 4, "mdvdn": 4, "mne1": 4, "mz": 4, "zero_dvd_iff": 4, "mgt2": 4, "pp": 4, "pdvd": 4, "factorial_po": 4, "dvd_factori": 4, "primes_infinit": 4, "refin": 4, "ple": 4, "p_1": 4, "p_n": 4, "prod_": 4, "p_i": [4, 6], "computation": 4, "test": 4, "decidableeq": 4, "abandon": 4, "ourselv": 4, "subset_iff": 4, "mem_int": 4, "mem_sdiff": 4, "tauto": 4, "dispens": 4, "tautolog": 4, "dvd_prod_of_mem": 4, "eq_of_dvd_of_prim": 4, "prime_q": 4, "preserv": [4, 6], "induction_on": 4, "singleton": 4, "prod_empti": 4, "prod_insert": 4, "mem_of_dvd_prod_prim": 4, "mem_insert": 4, "wrote": 4, "filter": [4, 10], "mem_filt": 4, "aim": 4, "prod_po": 4, "_def": 4, "mem_": 4, "id": [4, 6], "bounded_of_ex_finset": 4, "qk": 4, "lt_succ_of_l": 4, "le_sup": 4, "ex_finset_of_bound": 4, "decidablepr": 4, "lt_succ_iff": 4, "congruent": 4, "p_k": 4, "loss": 4, "27": 4, "mod_4_eq_3_or_mod_4_eq_3": 4, "mul_mod": 4, "mod_lt": 4, "hm": 4, "two_le_of_mod_4_eq_3": 4, "neq": 4, "div_dvd_of_dvd": 4, "div_lt_self": 4, "piec": [4, 5, 6], "exists_prime_factor_mod_4_eq_3": 4, "dvd_rfl": 4, "mge2": 4, "mul_div_cancel": 4, "home": [4, 5], "stretch": [4, 5], "remov": [4, 6], "eras": 4, "mem_eras": 4, "readi": [4, 6], "dvd_add_iff_left": 4, "primes_mod_4_eq_3_infinit": 4, "p4": 4, "pltn": 4, "p4eq": 4, "ps": 4, "pne3": 4, "seriou": [4, 6], "feat": 4, "modern": 5, "subject": 5, "mysteri": 5, "technic": 5, "consult": 5, "ann": 5, "baanen": 5, "abus": 5, "paramet": 5, "broadest": 5, "constraint": [5, 6], "bundl": [5, 6], "tupl": 5, "hy": 5, "hz": 5, "mypoint1": 5, "mypoint2": 5, "mypoint3": 5, "mk": [5, 6], "former": 5, "latter": [5, 6], "quot": [5, 6], "protect": 5, "intern": 5, "add_x": 5, "addalt": 5, "etc": [5, 6], "y\u2081": 5, "z\u2081": 5, "y\u2082": 5, "z\u2082": 5, "addalt_x": 5, "addalt_comm": 5, "ya": 5, "za": 5, "xb": 5, "yb": 5, "zb": 5, "apart": 5, "effici": [5, 6], "scalar": 5, "smul": 5, "smul_distrib": 5, "road": 5, "link": 5, "belong": [5, 6], "simplex": 5, "convinc": 5, "equilater": 5, "interior": 5, "standardtwosimplex": 5, "x_nonneg": 5, "y_nonneg": 5, "z_nonneg": 5, "sum_eq": 5, "swap": 5, "swapxi": 5, "interestingli": 5, "midpoint": 5, "div_nonneg": 5, "weight": 5, "averag": 5, "weightedaverag": 5, "lambda_nonneg": 5, "lambda_l": 5, "fin": 5, "standardsimplex": 5, "sum_eq_on": 5, "div_eq_mul_inv": 5, "sum_mul": 5, "sum_add_distrib": 5, "mul_sum": 5, "manipul": [5, 6], "islinear": 5, "is_addit": 5, "preserves_mul": 5, "linf": 5, "subtyp": [5, 6], "preal": 5, "val": 5, "sigma": 5, "wherebi": [5, 6], "stdsimplex": 5, "\u03c3": 5, "fst": [5, 6], "snd": [5, 6], "custom": 5, "robust": 5, "interfac": 5, "redefin": 5, "accessor": 5, "weav": 5, "rich": 5, "interconnect": 5, "hierarchi": 5, "clarifi": 5, "antireflex": 5, "cdot": 5, "mathcal": 5, "proxi": 5, "bipartit": 5, "graph": 5, "categori": [5, 6], "morphism": 5, "basi": [5, 6], "discret": 5, "inherit": 5, "polynomi": 5, "coeffici": 5, "dual": [5, 6], "accommod": 5, "almost": [5, 6], "marriag": 5, "heaven": 5, "group\u2081": 5, "inv": 5, "struc": 5, "counterpart": 5, "chosen": 5, "assur": 5, "groupcat": 5, "group\u2081cat": 5, "str": 5, "capit": 5, "roman": 5, "equiv": 5, "tofun": 5, "right_inv": 5, "left_inv": 5, "creativ": 5, "evid": 5, "coercion": [5, 6], "omit": 5, "perm": 5, "under": [5, 6], "orient": 5, "permgroup": 5, "trans_assoc": 5, "trans_refl": 5, "refl_tran": 5, "self_trans_symm": 5, "grouptheori": 5, "g_1": 5, "g_2": 5, "g_3": 5, "tightli": 5, "isomorph": 5, "additivegroup": 5, "Its": 5, "neg": [5, 6], "reproduc": 5, "accompani": 5, "addgroup\u2081": 5, "scheme": 5, "add_group_point": 5, "arrang": 5, "mul_inv_cancel_right": 5, "achiev": [5, 6], "silent": 5, "regist": 5, "grp": 5, "contextu": 5, "cue": 5, "synthes": 5, "whole": 5, "_inst_1": 5, "candid": 5, "group\u2082": 5, "mysquar": 5, "my_squar": 5, "remark": 5, "head": 5, "store": 5, "headi": 5, "hasmulgroup\u2082": 5, "hasonegroup\u2082": 5, "hasinvgroup\u2082": 5, "suppli": 5, "accord": 5, "capabl": 5, "chain": 5, "recent": 5, "prioriti": 5, "bad": [5, 6], "artifici": 5, "addgroup\u2082": 5, "subtl": [5, 6], "configur": 5, "invis": 5, "wise": 5, "euclidean": 5, "terminolog": 5, "mid": 5, "imaginari": 5, "gaussint": 5, "im": 5, "pointwis": [5, 6], "root": [5, 10], "ac": 5, "bci": 5, "adi": 5, "bd": 5, "bc": 5, "hasmul": 5, "zero_def": 5, "one_def": 5, "add_def": 5, "neg_def": 5, "mul_def": 5, "zero_r": 5, "zero_im": 5, "one_r": 5, "one_im": 5, "add_r": 5, "add_im": 5, "neg_r": 5, "neg_im": 5, "mul_r": 5, "mul_im": 5, "surprisingli": 5, "concept": [5, 6], "light": 5, "bulb": 5, "skeleton": [5, 6], "scari": 5, "entri": 5, "instcommr": 5, "left_distrib": 5, "right_distrib": 5, "ext_iff": 5, "bq": 5, "archetyp": 5, "int": 5, "ediv_add_emod": 5, "emod_nonneg": 5, "emod_lt": 5, "unit": [5, 6], "algorithm": 5, "conjug": 5, "frac": 5, "nearest": 5, "size": 5, "vi": 5, "multipli": 5, "view": [5, 6], "emb": 5, "forth": 5, "quadrat": 5, "gaussian_int": 5, "stai": 5, "face": [5, 6], "machineri": [5, 6], "adapt": 5, "invest": 5, "pragmat": 5, "seek": 5, "heather": 5, "macbeth": 5, "eleg": 5, "div": 5, "mod": 5, "_add_mod": 5, "abs_mod": 5, "_le": 5, "emod_lt_of_po": 5, "zero_lt_two": 5, "fixm": 5, "_eq": 5, "sq_add_sq_eq_zero": 5, "linearorderedr": 5, "norm_nonneg": 5, "norm_eq_zero": 5, "norm_po": 5, "norm_mul": 5, "conj": 5, "conj_r": 5, "conj_im": 5, "norm_conj": 5, "bespok": 5, "quad": 5, "record": 5, "div_def": 5, "mod_def": 5, "messi": 5, "nicer": [5, 6], "norm_mod_lt": 5, "norm_y_po": 5, "sub_mul": 5, "conv": 5, "lh": 5, "sq_le_sq": 5, "mul_le_mul_of_nonneg_left": 5, "ediv_mul_l": 5, "ediv_nonneg": 5, "le_of_mul_le_mul_right": 5, "ediv_lt_of_lt_mul": 5, "natab": 5, "coe_natabs_norm": 5, "natabs_of_nonneg": 5, "natabs_norm_mod_lt": 5, "ofnat_lt": 5, "coe_natab": 5, "not_norm_mul_left_lt_norm": 5, "natabs_mul": 5, "le_mul_of_one_le_right": 5, "ofnat_l": 5, "add_one_le_of_lt": 5, "euclideandomain": 5, "quotient_mul_add_remainder_eq": 5, "quotient_zero": 5, "r_wellfound": 5, "remainder_lt": 5, "mul_left_not_lt": 5, "payoff": 5, "principalidealr": 5, "irreducible_iff_prim": 5, "calculu": 6, "quantiti": 6, "studi": 6, "begun": 6, "paradox": 6, "layer": 6, "naiv": 6, "slightli": 6, "exot": 6, "intermedi": 6, "x\u2080": 6, "convention": 6, "eight": 6, "varieti": 6, "wish": 6, "64": 6, "y\u2080": 6, "z\u2080": 6, "paragraph": 6, "512": 6, "bourbaki": 6, "spell": 6, "dualli": 6, "arbitrarili": 6, "neighborhood": 6, "at_top": 6, "\ud835\udcdd": 6, "\ud835\udce4": 6, "entourag": 6, "\u03bc": 6, "a_": 6, "univ_set": 6, "sets_of_superset": 6, "inter_set": 6, "blur": 6, "princip": 6, "\ud835\udcdf": 6, "demonstr": 6, "opportun": 6, "x_0": 6, "ioo": 6, "tendsto\u2081": 6, "tendsto": 6, "lim_": 6, "sourc": 6, "abstractli": 6, "hide": 6, "salient": 6, "pushforward": 6, "f_": 6, "ve": 6, "tendsto\u2082": 6, "via": 6, "promis": 6, "leverag": 6, "map_mono": 6, "map_map": 6, "shot": 6, "256": 6, "pullback": 6, "comap": 6, "map_le_iff_le_comap": 6, "contravari": 6, "comap_comap": 6, "shift": 6, "plane": 6, "\u1da0": 6, "nhds_prod_eq": 6, "aforement": 6, "le_inf_iff": 6, "attop": 6, "bottom": 6, "shouldn": 6, "prohibit": 6, "global": 6, "precondit": 6, "closur": 6, "ne_bot": 6, "tour": 6, "claim": 6, "recaptur": 6, "superfici": 6, "stronger": 6, "famili": 6, "\u03b9": 6, "select": 6, "hasbasi": 6, "nhds_basis_ioo_po": 6, "has_basi": 6, "tendsto_iff": 6, "reformul": 6, "ici": 6, "attop_basi": 6, "knew": 6, "gave": 6, "n_p": 6, "n_q": 6, "tiresom": 6, "unpleas": 6, "superscript": 6, "hp": 6, "hq": 6, "eventually_eq": 6, "tendsto_congr": 6, "review": 6, "ensur": 6, "eventually_of_foral": 6, "mono": 6, "item": 6, "filter_upward": 6, "hr": 6, "reader": 6, "ae": 6, "aka": 6, "occasion": 6, "frequent": 6, "mem_closure_of_tendsto": 6, "cluster_pt": 6, "mem_closure_iff_clusterpt": 6, "le_principal_iff": 6, "nebot_of_l": 6, "hux": 6, "hum": 6, "dist_eq_zero": 6, "emetricspac": 6, "pseudometricspac": 6, "pseudoemetricspac": 6, "journei": 6, "recast": 6, "tendsto_attop": 6, "continuous_iff": 6, "devot": 6, "uncurri": 6, "slow": 6, "continuous_fst": 6, "comp": 6, "assembl": 6, "prod_mk": 6, "continuous_snd": 6, "continuous_dist": 6, "clunki": 6, "crucial": 6, "gradual": 6, "elabor": 6, "refus": 6, "prod_map": 6, "sad": 6, "wrap": 6, "border": 6, "obfusc": 6, "continuous_pow": 6, "continuous_id": 6, "continuousat": 6, "continuousat_iff": 6, "geometr": 6, "closedbal": 6, "radiu": 6, "mem_ball_self": 6, "mem_closedball_self": 6, "isopen": 6, "isopen_iff": 6, "Their": 6, "isclos": 6, "s\u1d9c": 6, "isopen_compl_iff": 6, "hu": 6, "mem_of_tendsto": 6, "mem_closure_iff": 6, "mem_closure_iff_seq_limit": 6, "main": 6, "nhds_basis_bal": 6, "nhds_basis_closedbal": 6, "mem_iff": 6, "segment": 6, "somewher": 6, "continuouson": 6, "minimum": 6, "deduc": 6, "iscompact": 6, "icc": 6, "iscompact_icc": 6, "\u03c6": 6, "strictmono": 6, "tendsto_subseq": 6, "exists_forall_l": 6, "exists_forall_g": 6, "compactspac": 6, "iscompact_univ": 6, "cauchi": 6, "uniformcontinu": 6, "uniformcontinuous_iff": 6, "clearli": 6, "isclosed_l": 6, "eq_empty_or_nonempti": 6, "attain": 6, "closer": 6, "cauchyseq": 6, "cauchyseq_iff": 6, "completespac": 6, "cauchyseq_tendsto_of_complet": 6, "criterion": 6, "explan": 6, "tendsto_pow_attop_nhds_0_of_lt_1": 6, "dist_le_range_sum_dist": 6, "cauchyseq_of_le_geometric_two": 6, "\u03b5_po": 6, "le_iff_exists_add": 6, "boss": 6, "bair": 6, "exclam": 6, "induct": [6, 10], "rec_on": 6, "ho": 6, "hd": 6, "dens": 6, "densiti": 6, "\u03b4po": 6, "hpo": 6, "hball": 6, "mem_closure_iff_nhds_basi": 6, "recon": 6, "rpo": 6, "rb": 6, "incl": 6, "cdist": 6, "ylim": 6, "yball": 6, "categor": 6, "ignor": 6, "topologicalspac": 6, "isopen_univ": 6, "isopen_empti": 6, "isopen_iunion": 6, "fintyp": 6, "isopen_iint": 6, "continuous_def": 6, "attach": 6, "filteri": 6, "sent": 6, "mem_nhds_iff": 6, "weird": 6, "digress": 6, "pure_le_nhd": 6, "eventually_eventually_nhd": 6, "topological_spac": 6, "mk_of_nhd": 6, "nhds_mk_of_nhd": 6, "clean": 6, "fonctori": 6, "induc": 6, "sensibl": 6, "uncount": 6, "relatedli": 6, "coinduc": 6, "t_x": 6, "t_y": 6, "coinduced_le_iff_le_induc": 6, "covari": 6, "coinduced_compos": 6, "induced_compos": 6, "topological_structur": 6, "primarili": 6, "ie": 6, "focus": 6, "nhd": 6, "opposit": 6, "recov": 6, "foward": 6, "continuous_iff_coinduced_l": 6, "g_": 6, "t_z": 6, "wasn": 6, "\u03c0": 6, "papar": 6, "t_": 6, "x_i": 6, "pi": 6, "defect": 6, "functori": 6, "price": 6, "patholog": 6, "t2_space": 6, "hausdorff": 6, "regular": 6, "t2space": 6, "tendsto_nhds_uniqu": 6, "regularspac": 6, "closed_nhds_basi": 6, "nhds_basis_open": 6, "denseinduc": 6, "continuousat_extend": 6, "funni": 6, "_in": 6, "thank": 6, "nhds_induc": 6, "is_open": 6, "fortiori": 6, "f_cont": 6, "tendsto_right_iff": 6, "firstcountabletopolog": 6, "sever": 6, "cluster": 6, "clusterpt": 6, "nebot": 6, "hfx": 6, "push_pul": 6, "of_map": 6, "f_ne": 6, "f_le": 6, "map_eq": 6, "hne": 6, "hle": 6, "huo": 6, "hsu": 6, "elim_finite_subcov": 6, "elementary_differential_calculu": 7, "introductori": 7, "normed_spac": 7, "overview": 10, "conjunct": 10, "converg": 10, "schr\u00f6der": 10, "bernstein": 10, "irrat": 10}, "objects": {}, "objtypes": {}, "objnames": {}, "titleterms": {"introduct": 0, "get": 0, "start": 0, "overview": 0, "basic": 1, "calcul": 1, "prove": 1, "ident": 1, "algebra": [1, 5], "structur": [1, 5], "us": 1, "theorem": [1, 3], "lemma": 1, "more": 1, "order": 1, "divis": 1, "fact": 1, "about": 1, "logic": 2, "implic": 2, "univers": 2, "quantifi": 2, "The": [2, 3], "existenti": 2, "negat": 2, "conjunct": 2, "bi": 2, "disjunct": 2, "sequenc": 2, "converg": [2, 6], "set": [3, 6], "function": [3, 6], "schr\u00f6der": 3, "bernstein": 3, "number": 4, "theori": [4, 8], "irrat": 4, "root": 4, "induct": 4, "recurs": 4, "infinit": 4, "mani": 4, "prime": 4, "abstract": 5, "build": 5, "gaussian": 5, "integ": 5, "topolog": 6, "filter": 6, "metric": 6, "space": 6, "continu": 6, "ball": 6, "open": 6, "close": 6, "compact": 6, "uniformli": 6, "complet": 6, "fundament": 6, "separ": 6, "countabl": 6, "differenti": 7, "calculu": 7, "integr": 8, "measur": 8, "index": 9, "mathemat": 10, "lean": 10}, "envversion": {"sphinx.domains.c": 2, "sphinx.domains.changeset": 1, "sphinx.domains.citation": 1, "sphinx.domains.cpp": 6, "sphinx.domains.index": 1, "sphinx.domains.javascript": 2, "sphinx.domains.math": 2, "sphinx.domains.python": 3, "sphinx.domains.rst": 2, "sphinx.domains.std": 2, "sphinx": 56}})
mathematics_in_lean.pdf
src/C01_Introduction/S02_Overview.lean
- @@ -36,7 +36,8 @@ example : ∀ m n : Nat, Even n → Even (m * n) := fun m n ⟨k, (hk : n = k +
  have hmn : m * n = m * k + m * k := by rw [hk, mul_add] show ∃ l, m * n = l + l from ⟨_, hmn⟩ - example : ∀ m n : Nat, Even n → Even (m * n) := fun m n ⟨k, hk⟩ => ⟨m * k, by rw [hk, mul_add]⟩ + example : ∀ m n : Nat, Even n → Even (m * n) := + fun m n ⟨k, hk⟩ => ⟨m * k, by rw [hk, mul_add]⟩ example : ∀ m n : Nat, Even n → Even (m * n) := by -- say m and n are natural numbers, and assume n=2*k
src/C02_Basics/S04_More_on_Order_and_Divisibility.lean
- @@ -73,17 +73,12 @@ example (h : x ∣ w) : x ∣ y * (x * z) + x ^ 2 + w ^ 2 := by
  end section - variable (m n : ℕ) - open Nat #check (gcd_zero_right n : gcd n 0 = n) - #check (gcd_zero_left n : gcd 0 n = n) - #check (lcm_zero_right n : lcm n 0 = 0) - #check (lcm_zero_left n : lcm 0 n = 0) example : gcd m n = gcd n m := by
src/C02_Basics/solutions/Solutions_S04_More_on_Order_and_Divisibility.lean
- @@ -96,17 +96,12 @@ example (h : x ∣ w) : x ∣ y * (x * z) + x ^ 2 + w ^ 2 := by
  end section - variable (m n : ℕ) - open Nat #check (gcd_zero_right n : gcd n 0 = n) - #check (gcd_zero_left n : gcd 0 n = n) - #check (lcm_zero_right n : lcm n 0 = 0) - #check (lcm_zero_left n : lcm 0 n = 0) example : gcd m n = gcd n m := by
src/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean
- @@ -30,11 +30,13 @@ variable (ha : abs a < δ) (hb : abs b < δ)
 end - theorem my_lemma3 : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε := by + theorem my_lemma3 : + ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε := by intro x y ε epos ele1 xlt ylt sorry - theorem my_lemma4 : ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε := by + theorem my_lemma4 : + ∀ {x y ε : ℝ}, 0 < ε → ε ≤ 1 → abs x < ε → abs y < ε → abs (x * y) < ε := by intro x y ε epos ele1 xlt ylt calc abs (x * y) = abs x * abs y := sorry
src/C03_Logic/S06_Sequences_and_Convergence.lean
- @@ -23,7 +23,8 @@ theorem convergesTo_const (a : ℝ) : ConvergesTo (fun x : ℕ => a) a := by
  rw [sub_self, abs_zero] apply εpos - theorem convergesTo_add {s t : ℕ → ℝ} {a b : ℝ} (cs : ConvergesTo s a) (ct : ConvergesTo t b) : + theorem convergesTo_add {s t : ℕ → ℝ} {a b : ℝ} + (cs : ConvergesTo s a) (ct : ConvergesTo t b) : ConvergesTo (fun n => s n + t n) (a + b) := by intro ε εpos dsimp
- @@ -58,7 +59,8 @@ theorem aux {s t : ℕ → ℝ} {a : ℝ} (cs : ConvergesTo s a) (ct : Converges
  cases' ct _ pos₀ with N₁ h₁ sorry - theorem convergesTo_mul {s t : ℕ → ℝ} {a b : ℝ} (cs : ConvergesTo s a) (ct : ConvergesTo t b) : + theorem convergesTo_mul {s t : ℕ → ℝ} {a b : ℝ} + (cs : ConvergesTo s a) (ct : ConvergesTo t b) : ConvergesTo (fun n => s n * t n) (a * b) := by have h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0 := by apply aux cs
- @@ -69,7 +71,8 @@ theorem convergesTo_mul {s t : ℕ → ℝ} {a b : ℝ} (cs : ConvergesTo s a) (
  · ext; ring ring - theorem convergesTo_unique {s : ℕ → ℝ} {a b : ℝ} (sa : ConvergesTo s a) (sb : ConvergesTo s b) : + theorem convergesTo_unique {s : ℕ → ℝ} {a b : ℝ} + (sa : ConvergesTo s a) (sb : ConvergesTo s b) : a = b := by by_contra abne have : abs (a - b) > 0 := by sorry
src/C03_Logic/solutions/Solutions_S06_Sequences_and_Convergence.lean
- @@ -10,7 +10,8 @@ theorem convergesTo_const (a : ℝ) : ConvergesTo (fun x : ℕ => a) a := by
 rw [sub_self, abs_zero] apply εpos - theorem convergesTo_add {s t : ℕ → ℝ} {a b : ℝ} (cs : ConvergesTo s a) (ct : ConvergesTo t b) : + theorem convergesTo_add {s t : ℕ → ℝ} {a b : ℝ} + (cs : ConvergesTo s a) (ct : ConvergesTo t b) : ConvergesTo (fun n => s n + t n) (a + b) := by intro ε εpos dsimp
- @@ -76,7 +77,8 @@ theorem aux {s t : ℕ → ℝ} {a : ℝ} (cs : ConvergesTo s a) (ct : Converges
 _ < B * (ε / B) := (mul_lt_mul'' (h₀ n ngeN₀) (h₁ n ngeN₁) (abs_nonneg _) (abs_nonneg _)) _ = ε := mul_div_cancel' _ (ne_of_lt Bpos).symm - theorem convergesTo_mul {s t : ℕ → ℝ} {a b : ℝ} (cs : ConvergesTo s a) (ct : ConvergesTo t b) : + theorem convergesTo_mul {s t : ℕ → ℝ} {a b : ℝ} + (cs : ConvergesTo s a) (ct : ConvergesTo t b) : ConvergesTo (fun n => s n * t n) (a * b) := by have h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0 := by apply aux cs
- @@ -87,7 +89,8 @@ theorem convergesTo_mul {s t : ℕ → ℝ} {a b : ℝ} (cs : ConvergesTo s a) (
 · ext; ring ring - theorem convergesTo_unique {s : ℕ → ℝ} {a b : ℝ} (sa : ConvergesTo s a) (sb : ConvergesTo s b) : + theorem convergesTo_unique {s : ℕ → ℝ} {a b : ℝ} + (sa : ConvergesTo s a) (sb : ConvergesTo s b) : a = b := by by_contra abne have : abs (a - b) > 0 := by
src/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean
- @@ -3,7 +3,6 @@ import Mathlib.Data.Set.Function
  import Mathlib.Tactic open Set - open Function noncomputable section
src/C05_Number_Theory/S01_Irrational_Roots.lean
- @@ -80,11 +80,13 @@ theorem factorization_mul' {m n : ℕ} (mnez : m ≠ 0) (nnez : n ≠ 0) (p :
  rw [Nat.factorization_mul mnez nnez] rfl - theorem factorization_pow' (n k p : ℕ) : (n ^ k).factorization p = k * n.factorization p := by + theorem factorization_pow' (n k p : ℕ) : + (n ^ k).factorization p = k * n.factorization p := by rw [Nat.factorization_pow] rfl - theorem Nat.Prime.factorization' {p : ℕ} (prime_p : p.Prime) : p.factorization p = 1 := by + theorem Nat.Prime.factorization' {p : ℕ} (prime_p : p.Prime) : + p.factorization p = 1 := by rw [prime_p.factorization] simp
- @@ -95,7 +97,8 @@ example {m n p : ℕ} (nnz : n ≠ 0) (prime_p : p.Prime) : m ^ 2 ≠ p * n ^ 2
  sorry have eq2 : (p * n ^ 2).factorization p = 2 * n.factorization p + 1 := by sorry - have : 2 * m.factorization p % 2 = (2 * n.factorization p + 1) % 2 := by rw [← eq1, sqr_eq, eq2] + have : 2 * m.factorization p % 2 = (2 * n.factorization p + 1) % 2 := by + rw [← eq1, sqr_eq, eq2] rw [add_comm, Nat.add_mul_mod_self_left, Nat.mul_mod_right] at this norm_num at this
- @@ -106,7 +109,8 @@ example {m n k r : ℕ} (nnz : n ≠ 0) (pow_eq : m ^ k = r * n ^ k) {p : ℕ} (
  have npow_nz : n ^ k ≠ 0 := fun npowz => nnz (pow_eq_zero npowz) have eq1 : (m ^ k).factorization p = k * m.factorization p := by sorry - have eq2 : (r.succ * n ^ k).factorization p = k * n.factorization p + r.succ.factorization p := by + have eq2 : (r.succ * n ^ k).factorization p = + k * n.factorization p + r.succ.factorization p := by sorry have : r.succ.factorization p = k * m.factorization p - k * n.factorization p := by rw [← eq1, pow_eq, eq2, add_comm, Nat.add_sub_cancel]
src/C05_Number_Theory/S03_Infinitely_Many_Primes.lean
- @@ -94,14 +94,17 @@ example : (r ∪ s) ∩ (r ∪ t) = r ∪ s ∩ t := by
  sorry example : (r \ s) \ t = r \ (s ∪ t) := by sorry + end example (s : Finset ℕ) (n : ℕ) (h : n ∈ s) : n ∣ ∏ i in s, i := Finset.dvd_prod_of_mem _ h - theorem Nat.Prime.eq_of_dvd_of_prime {p q : ℕ} (prime_p : Nat.Prime p) (prime_q : Nat.Prime q) - (h : p ∣ q) : p = q := by + theorem Nat.Prime.eq_of_dvd_of_prime {p q : ℕ} + (prime_p : Nat.Prime p) (prime_q : Nat.Prime q) (h : p ∣ q) : + p = q := by sorry + theorem mem_of_dvd_prod_primes {s : Finset ℕ} {p : ℕ} (prime_p : p.Prime) : (∀ n ∈ s, Nat.Prime n) → (p ∣ ∏ n in s, n) → p ∈ s := by intro h₀ h₁
- @@ -193,7 +196,7 @@ theorem exists_prime_factor_mod_4_eq_3 {n : Nat} (h : n % 4 = 3) :
  rw [neq, h] cases' this with h1 h1 . sorry - sorry + . sorry example (m n : ℕ) (s : Finset ℕ) (h : m ∈ erase s n) : m ≠ n ∧ m ∈ s := by rwa [mem_erase] at h
src/C05_Number_Theory/solutions/Solutions_S01_Irrational_Roots.lean
- @@ -64,11 +64,13 @@ theorem factorization_mul' {m n : ℕ} (mnez : m ≠ 0) (nnez : n ≠ 0) (p :
  rw [Nat.factorization_mul mnez nnez] rfl - theorem factorization_pow' (n k p : ℕ) : (n ^ k).factorization p = k * n.factorization p := by + theorem factorization_pow' (n k p : ℕ) : + (n ^ k).factorization p = k * n.factorization p := by rw [Nat.factorization_pow] rfl - theorem Nat.Prime.factorization' {p : ℕ} (prime_p : p.Prime) : p.factorization p = 1 := by + theorem Nat.Prime.factorization' {p : ℕ} (prime_p : p.Prime) : + p.factorization p = 1 := by rw [prime_p.factorization] simp
- @@ -80,7 +82,8 @@ example {m n p : ℕ} (nnz : n ≠ 0) (prime_p : p.Prime) : m ^ 2 ≠ p * n ^ 2
  have eq2 : (p * n ^ 2).factorization p = 2 * n.factorization p + 1 := by rw [factorization_mul' prime_p.ne_zero nsqr_nez, prime_p.factorization', factorization_pow', add_comm] - have : 2 * m.factorization p % 2 = (2 * n.factorization p + 1) % 2 := by rw [← eq1, sqr_eq, eq2] + have : 2 * m.factorization p % 2 = (2 * n.factorization p + 1) % 2 := by + rw [← eq1, sqr_eq, eq2] rw [add_comm, Nat.add_mul_mod_self_left, Nat.mul_mod_right] at this norm_num at this
- @@ -91,7 +94,8 @@ example {m n k r : ℕ} (nnz : n ≠ 0) (pow_eq : m ^ k = r * n ^ k) {p : ℕ} (
  have npow_nz : n ^ k ≠ 0 := fun npowz => nnz (pow_eq_zero npowz) have eq1 : (m ^ k).factorization p = k * m.factorization p := by rw [factorization_pow'] - have eq2 : (r.succ * n ^ k).factorization p = k * n.factorization p + r.succ.factorization p := by + have eq2 : (r.succ * n ^ k).factorization p = + k * n.factorization p + r.succ.factorization p := by rw [factorization_mul' r.succ_ne_zero npow_nz, factorization_pow', add_comm] have : r.succ.factorization p = k * m.factorization p - k * n.factorization p := by rw [← eq1, pow_eq, eq2, add_comm, Nat.add_sub_cancel]
src/C05_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean
- @@ -80,8 +80,9 @@ example : (r \ s) \ t = r \ (s ∪ t) := by
  end - theorem Nat.Prime.eq_of_dvd_of_prime {p q : ℕ} (prime_p : Nat.Prime p) (prime_q : Nat.Prime q) - (h : p ∣ q) : p = q := by + theorem Nat.Prime.eq_of_dvd_of_prime {p q : ℕ} + (prime_p : Nat.Prime p) (prime_q : Nat.Prime q) (h : p ∣ q) : + p = q := by cases prime_q.eq_one_or_self_of_dvd _ h · linarith [prime_p.two_le] assumption
src/C06_Abstract_Algebra/S01_Structures.lean
- @@ -96,9 +96,12 @@ example : ∀ a b : Point, add a b = add b a := fun ⟨xa, ya, za⟩ ⟨xb, yb,
  protected theorem add_assoc (a b c : Point) : (a.add b).add c = a.add (b.add c) := by sorry + def smul (r : ℝ) (a : Point) : Point := sorry - theorem smul_distrib (r : ℝ) (a b : Point) : (smul r a).add (smul r b) = smul r (a.add b) := by + + theorem smul_distrib (r : ℝ) (a b : Point) : + (smul r a).add (smul r b) = smul r (a.add b) := by sorry end Point
- @@ -162,7 +165,8 @@ def midpoint (n : ℕ) (a b : StandardSimplex n) : StandardSimplex n
  · linarith [a.NonNeg i, b.NonNeg i] norm_num sum_eq_one := by - simp [div_eq_mul_inv, ← Finset.sum_mul, Finset.sum_add_distrib, a.sum_eq_one, b.sum_eq_one] + simp [div_eq_mul_inv, ← Finset.sum_mul, Finset.sum_add_distrib, + a.sum_eq_one, b.sum_eq_one] field_simp end StandardSimplex
src/C06_Abstract_Algebra/S02_Algebraic_Structures.lean
- @@ -68,11 +68,11 @@ def neg (a : Point) : Point := sorry
  def zero : Point := sorry - def add_group_point : AddGroup₁ Point := sorry + def add_group_point : AddGroup₁ point := sorry + end Point section - variable {α : Type _} (f g : Equiv.Perm α) (n : ℕ) #check f * g
src/C06_Abstract_Algebra/S03_Building_the_Gaussian_Integers.lean
- @@ -37,7 +37,8 @@ theorem add_def (x y : gaussInt) : x + y = ⟨x.re + y.re, x.im + y.im⟩ :=
 theorem neg_def (x : gaussInt) : -x = ⟨-x.re, -x.im⟩ := rfl - theorem mul_def (x y : gaussInt) : x * y = ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩ := + theorem mul_def (x y : gaussInt) : + x * y = ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩ := rfl @[simp]
- @@ -207,9 +208,11 @@ theorem div_def (x y : gaussInt) :
 theorem mod_def (x y : gaussInt) : x % y = x - y * (x / y) := rfl - theorem norm_mod_lt (x : gaussInt) {y : gaussInt} (hy : y ≠ 0) : (x % y).norm < y.norm := by + theorem norm_mod_lt (x : gaussInt) {y : gaussInt} (hy : y ≠ 0) : + (x % y).norm < y.norm := by have norm_y_pos : 0 < norm y := by rwa [norm_pos] - have : x % y * conj y = ⟨Int.mod' (x * conj y).re (norm y), Int.mod' (x * conj y).im (norm y)⟩ := by + have : x % y * conj y = + ⟨Int.mod' (x * conj y).re (norm y), Int.mod' (x * conj y).im (norm y)⟩ := by rw [mod_def, sub_mul, Int.mod'_eq, Int.mod'_eq, sub_eq_add_neg, div_def, norm] ext <;> simp <;> ring have : norm (x % y) * norm y ≤ norm y / 2 * norm y := by
- @@ -238,7 +241,8 @@ theorem norm_mod_lt (x : gaussInt) {y : gaussInt} (hy : y ≠ 0) : (x % y).norm
 theorem coe_natAbs_norm (x : gaussInt) : (x.norm.natAbs : ℤ) = x.norm := Int.natAbs_of_nonneg (norm_nonneg _) - theorem natAbs_norm_mod_lt (x y : gaussInt) (hy : y ≠ 0) : (x % y).norm.natAbs < y.norm.natAbs := by + 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] apply norm_mod_lt x hy
- @@ -256,7 +260,8 @@ instance : EuclideanDomain gaussInt :=
 { gaussInt.instCommRing with quotient := (· / ·) remainder := (· % ·) - quotient_mul_add_remainder_eq := fun x y => by simp only; rw [mod_def, add_comm, sub_add_cancel] + quotient_mul_add_remainder_eq := + fun x y => by simp only; rw [mod_def, add_comm, sub_add_cancel] quotient_zero := fun x => by simp [div_def, norm, Int.div'] rfl
src/C06_Abstract_Algebra/solutions/Solutions_S01_Structures.lean
- @@ -20,7 +20,8 @@ protected theorem add_assoc (a b c : Point) : (a.add b).add c = a.add (b.add c)
  def smul (r : ℝ) (a : Point) : Point := ⟨r * a.x, r * a.y, r * a.z⟩ - theorem smul_distrib (r : ℝ) (a b : Point) : (smul r a).add (smul r b) = smul r (a.add b) := by + theorem smul_distrib (r : ℝ) (a b : Point) : + (smul r a).add (smul r b) = smul r (a.add b) := by simp [add, smul, mul_add] end Point
- @@ -39,8 +40,8 @@ namespace StandardTwoSimplex
  noncomputable section def weightedAverage (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1) - (a b : StandardTwoSimplex) : StandardTwoSimplex - where + (a b : StandardTwoSimplex) : StandardTwoSimplex + where x := lambda * a.x + (1 - lambda) * b.x y := lambda * a.y + (1 - lambda) * b.y z := lambda * a.z + (1 - lambda) * b.z
- @@ -74,7 +75,8 @@ def midpoint (n : ℕ) (a b : StandardSimplex n) : StandardSimplex n
  · linarith [a.NonNeg i, b.NonNeg i] norm_num sum_eq_one := by - simp [div_eq_mul_inv, ← Finset.sum_mul, Finset.sum_add_distrib, a.sum_eq_one, b.sum_eq_one] + simp [div_eq_mul_inv, ← Finset.sum_mul, Finset.sum_add_distrib, + a.sum_eq_one, b.sum_eq_one] field_simp end StandardSimplex
src/C06_Abstract_Algebra/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean
- @@ -37,7 +37,8 @@ theorem add_def (x y : gaussInt) : x + y = ⟨x.re + y.re, x.im + y.im⟩ :=
 theorem neg_def (x : gaussInt) : -x = ⟨-x.re, -x.im⟩ := rfl - theorem mul_def (x y : gaussInt) : x * y = ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩ := + theorem mul_def (x y : gaussInt) : + x * y = ⟨x.re * y.re - x.im * y.im, x.re * y.im + x.im * y.re⟩ := rfl @[simp]
- @@ -221,9 +222,11 @@ theorem div_def (x y : gaussInt) :
 theorem mod_def (x y : gaussInt) : x % y = x - y * (x / y) := rfl - theorem norm_mod_lt (x : gaussInt) {y : gaussInt} (hy : y ≠ 0) : (x % y).norm < y.norm := by + theorem norm_mod_lt (x : gaussInt) {y : gaussInt} (hy : y ≠ 0) : + (x % y).norm < y.norm := by have norm_y_pos : 0 < norm y := by rwa [norm_pos] - have : x % y * conj y = ⟨Int.mod' (x * conj y).re (norm y), Int.mod' (x * conj y).im (norm y)⟩ := by + have : x % y * conj y = + ⟨Int.mod' (x * conj y).re (norm y), Int.mod' (x * conj y).im (norm y)⟩ := by rw [mod_def, sub_mul, Int.mod'_eq, Int.mod'_eq, sub_eq_add_neg, div_def, norm] ext <;> simp <;> ring have : norm (x % y) * norm y ≤ norm y / 2 * norm y := by
- @@ -252,7 +255,8 @@ theorem norm_mod_lt (x : gaussInt) {y : gaussInt} (hy : y ≠ 0) : (x % y).norm
 theorem coe_natAbs_norm (x : gaussInt) : (x.norm.natAbs : ℤ) = x.norm := Int.natAbs_of_nonneg (norm_nonneg _) - theorem natAbs_norm_mod_lt (x y : gaussInt) (hy : y ≠ 0) : (x % y).norm.natAbs < y.norm.natAbs := by + 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] apply norm_mod_lt x hy
- @@ -270,7 +274,8 @@ instance : EuclideanDomain gaussInt :=
 { gaussInt.instCommRing with quotient := (· / ·) remainder := (· % ·) - quotient_mul_add_remainder_eq := fun x y => by simp only; rw [mod_def, add_comm, sub_add_cancel] + quotient_mul_add_remainder_eq := + fun x y => by simp only; rw [mod_def, add_comm, sub_add_cancel] quotient_zero := fun x => by simp [div_def, norm, Int.div'] rfl
src/C07_Topology/S01_Filters.lean
- @@ -80,9 +80,7 @@ example (u v : ℕ → ℝ) (h : u =ᶠ[atTop] v) (x₀ : ℝ) :
  tendsto_congr' h #check @eventually_of_forall - #check @Eventually.mono - #check @Eventually.and example (P Q R : ℕ → Prop) (hP : ∀ᶠ n in atTop, P n) (hQ : ∀ᶠ n in atTop, Q n)
- @@ -98,9 +96,7 @@ example (P Q R : ℕ → Prop) (hP : ∀ᶠ n in atTop, P n) (hQ : ∀ᶠ n in a
  exact h'' ⟨h, h'⟩ #check mem_closure_iff_clusterPt - #check le_principal_iff - #check neBot_of_le example (u : ℕ → ℝ) (M : Set ℝ) (x : ℝ) (hux : Tendsto u atTop (𝓝 x))
src/C07_Topology/S02_Metric_Spaces.lean
- @@ -7,27 +7,23 @@ open Topology Filter
 variable {X : Type _} [MetricSpace X] (a b c : X) #check (dist a b : ℝ) - #check (dist_nonneg : 0 ≤ dist a b) - #check (dist_eq_zero : dist a b = 0 ↔ a = b) - #check (dist_comm a b : dist a b = dist b a) - #check (dist_triangle a b c : dist a c ≤ dist a b + dist b c) -- Note the next three lines are not quoted, their purpose is to make sure those things don't get renamed while we're looking elsewhere. #check EMetricSpace - #check PseudoMetricSpace - #check PseudoEMetricSpace - example {u : ℕ → X} {a : X} : Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε := + example {u : ℕ → X} {a : X} : + Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε := Metric.tendsto_atTop example {X Y : Type _} [MetricSpace X] [MetricSpace Y] {f : X → Y} : - Continuous f ↔ ∀ x : X, ∀ ε > 0, ∃ δ > 0, ∀ x', dist x' x < δ → dist (f x') (f x) < ε := + Continuous f ↔ + ∀ x : X, ∀ ε > 0, ∃ δ > 0, ∀ x', dist x' x < δ → dist (f x') (f x) < ε := Metric.continuous_iff example {X Y : Type _} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
- @@ -85,7 +81,8 @@ example {s : Set X} (hs : IsClosed s) {u : ℕ → X} (hu : Tendsto u atTop (
 example {s : Set X} : a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, a ∈ Metric.ball b ε := Metric.mem_closure_iff - example {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a)) {s : Set X} (hs : ∀ n, u n ∈ s) : a ∈ closure s := + example {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a)) {s : Set X} (hs : ∀ n, u n ∈ s) : + a ∈ closure s := sorry example {x : X} {s : Set X} : s ∈ 𝓝 x ↔ ∃ ε > 0, Metric.ball x ε ⊆ s :=
- @@ -101,11 +98,13 @@ example {s : Set X} (hs : IsCompact s) {u : ℕ → X} (hu : ∀ n, u n ∈ s) :
 ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (u ∘ φ) atTop (𝓝 a) := hs.tendsto_subseq hu - example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ} (hfs : ContinuousOn f 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 - example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ} (hfs : ContinuousOn f s) : + 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
- @@ -118,20 +117,25 @@ example {X : Type _} [MetricSpace X] [CompactSpace X] : IsCompact (univ : Set X)
 #check IsCompact.isClosed example {X : Type _} [MetricSpace X] {Y : Type _} [MetricSpace Y] {f : X → Y} : - UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : X}, dist a b < δ → dist (f a) (f b) < ε := + UniformContinuous f ↔ + ∀ ε > 0, ∃ δ > 0, ∀ {a b : X}, dist a b < δ → dist (f a) (f b) < ε := Metric.uniformContinuous_iff - example {X : Type _} [MetricSpace X] [CompactSpace X] {Y : Type _} [MetricSpace Y] {f : X → Y} + example {X : Type _} [MetricSpace X] [CompactSpace X] + {Y : Type _} [MetricSpace Y] {f : X → Y} (hf : Continuous f) : UniformContinuous f := sorry - example (u : ℕ → X) : CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε := + example (u : ℕ → X) : + CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε := Metric.cauchySeq_iff - example (u : ℕ → X) : CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, dist (u n) (u N) < ε := + example (u : ℕ → X) : + CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, dist (u n) (u N) < ε := Metric.cauchySeq_iff' - example [CompleteSpace X] (u : ℕ → X) (hu : CauchySeq u) : ∃ x, Tendsto u atTop (𝓝 x) := + example [CompleteSpace X] (u : ℕ → X) (hu : CauchySeq u) : + ∃ x, Tendsto u atTop (𝓝 x) := cauchySeq_tendsto_of_complete hu open BigOperators
- @@ -174,18 +178,21 @@ example [CompleteSpace X] (f : ℕ → Set X) (ho : ∀ n, IsOpen (f n)) (hd :
 intro x rw [mem_closure_iff_nhds_basis nhds_basis_closedBall] intro ε εpos - /- `ε` is positive. We have to find a point in the ball of radius `ε` around `x` belonging to all - `f n`. For this, we construct inductively a sequence `F n = (c n, r n)` such that the closed ball - `closedBall (c n) (r n)` is included in the previous ball and in `f n`, and such that - `r n` is small enough to ensure that `c n` is a Cauchy sequence. Then `c n` converges to a - limit which belongs to all the `f n`. -/ + /- `ε` is positive. We have to find a point in the ball of radius `ε` around `x` + belonging to all `f n`. For this, we construct inductively a sequence + `F n = (c n, r n)` such that the closed ball `closedBall (c n) (r n)` is included + in the previous ball and in `f n`, and such that `r n` is small enough to ensure + that `c n` is a Cauchy sequence. Then `c n` converges to a limit which belongs + to all the `f n`. -/ let F : ℕ → X × ℝ := fun n => - Nat.recOn n (Prod.mk x (min ε (B 0))) fun n p => Prod.mk (center n p.1 p.2) (radius n p.1 p.2) + Nat.recOn n (Prod.mk x (min ε (B 0))) + fun n p => Prod.mk (center n p.1 p.2) (radius n p.1 p.2) let c : ℕ → X := fun n => (F n).1 let r : ℕ → ℝ := fun n => (F n).2 have rpos : ∀ n, 0 < r n := by sorry have rB : ∀ n, r n ≤ B n := by sorry - have incl : ∀ n, closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n := by sorry + have incl : ∀ n, closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n := by + sorry have cdist : ∀ n, dist (c n) (c (n + 1)) ≤ B n := by sorry have : CauchySeq c := cauchySeq_of_le_geometric_two' cdist -- as the sequence `c n` is Cauchy in a complete space, it converges to a limit `y`.
src/C07_Topology/S03_Topological_Spaces.lean
- @@ -1,9 +1,7 @@
 import Mathlib.Topology.Instances.Real import Mathlib.Analysis.NormedSpace.BanachSteinhaus - open Set Filter - - open Topology Filter + open Set Filter Topology section variable {X : Type _} [TopologicalSpace X]
- @@ -17,7 +15,8 @@ example : IsOpen (∅ : Set X) :=
 example {ι : Type _} {s : ι → Set X} (hs : ∀ i, IsOpen <| s i) : IsOpen (⋃ i, s i) := isOpen_iUnion hs - example {ι : Type _} [Fintype ι] {s : ι → Set X} (hs : ∀ i, IsOpen <| s i) : IsOpen (⋂ i, s i) := + example {ι : Type _} [Fintype ι] {s : ι → Set X} (hs : ∀ i, IsOpen <| s i) : + IsOpen (⋂ i, s i) := isOpen_iInter hs variable {Y : Type _} [TopologicalSpace Y]
- @@ -78,8 +77,10 @@ example (T_X : TopologicalSpace X) (T_Y : TopologicalSpace Y) (f : X → Y) :
 Continuous f ↔ TopologicalSpace.coinduced f T_X ≤ T_Y := continuous_iff_coinduced_le - example {Z : Type _} (f : X → Y) (T_X : TopologicalSpace X) (T_Z : TopologicalSpace Z) (g : Y → Z) : - @Continuous Y Z (TopologicalSpace.coinduced f T_X) T_Z g ↔ @Continuous X Z T_X T_Z (g ∘ f) := by + example {Z : Type _} (f : X → Y) (T_X : TopologicalSpace X) (T_Z : TopologicalSpace Z) + (g : Y → Z) : + @Continuous Y Z (TopologicalSpace.coinduced f T_X) T_Z g ↔ + @Continuous X Z T_X T_Z (g ∘ f) := by rw [continuous_iff_coinduced_le, coinduced_compose, continuous_iff_coinduced_le] example (ι : Type _) (X : ι → Type _) (T_X : ∀ i, TopologicalSpace <| X i) :
- @@ -95,11 +96,13 @@ example [TopologicalSpace X] [RegularSpace X] (a : X) :
 (𝓝 a).HasBasis (fun s : Set X => s ∈ 𝓝 a ∧ IsClosed s) id := closed_nhds_basis a - example [TopologicalSpace X] {x : X} : (𝓝 x).HasBasis (fun t : Set X => t ∈ 𝓝 x ∧ IsOpen t) id := + example [TopologicalSpace X] {x : X} : + (𝓝 x).HasBasis (fun t : Set X => t ∈ 𝓝 x ∧ IsOpen t) id := nhds_basis_opens' x - theorem aux {X Y A : Type _} [TopologicalSpace X] {c : A → X} {f : A → Y} {x : X} {F : Filter Y} - (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) : + theorem aux {X Y A : Type _} [TopologicalSpace X] {c : A → X} + {f : A → Y} {x : X} {F : Filter Y} + (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) : ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := sorry
- @@ -111,7 +114,8 @@ example [TopologicalSpace X] [TopologicalSpace Y] [RegularSpace Y] {A : Set X}
 #check @HasBasis.tendsto_right_iff - example [TopologicalSpace X] [TopologicalSpace.FirstCountableTopology X] {s : Set X} {a : X} : + example [TopologicalSpace X] [TopologicalSpace.FirstCountableTopology X] + {s : Set X} {a : X} : a ∈ closure s ↔ ∃ u : ℕ → X, (∀ n, u n ∈ s) ∧ Tendsto u atTop (𝓝 a) := mem_closure_iff_seq_limit
- @@ -120,7 +124,8 @@ variable [TopologicalSpace X]
 example {F : Filter X} {x : X} : ClusterPt x F ↔ NeBot (𝓝 x ⊓ F) := Iff.rfl - example {s : Set X} : IsCompact s ↔ ∀ (F : Filter X) [NeBot F], F ≤ 𝓟 s → ∃ a ∈ s, ClusterPt a F := + example {s : Set X} : + IsCompact s ↔ ∀ (F : Filter X) [NeBot F], F ≤ 𝓟 s → ∃ a ∈ s, ClusterPt a F := Iff.rfl example [TopologicalSpace.FirstCountableTopology X] {s : Set X} {u : ℕ → X} (hs : IsCompact s)
src/C07_Topology/solutions/Solutions_S02_Metric_Spaces.lean
- @@ -7,27 +7,23 @@ open Topology Filter
 variable {X : Type _} [MetricSpace X] (a b c : X) #check (dist a b : ℝ) - #check (dist_nonneg : 0 ≤ dist a b) - #check (dist_eq_zero : dist a b = 0 ↔ a = b) - #check (dist_comm a b : dist a b = dist b a) - #check (dist_triangle a b c : dist a c ≤ dist a b + dist b c) -- Note the next three lines are not quoted, their purpose is to make sure those things don't get renamed while we're looking elsewhere. #check EMetricSpace - #check PseudoMetricSpace - #check PseudoEMetricSpace - example {u : ℕ → X} {a : X} : Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε := + example {u : ℕ → X} {a : X} : + Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε := Metric.tendsto_atTop example {X Y : Type _} [MetricSpace X] [MetricSpace Y] {f : X → Y} : - Continuous f ↔ ∀ x : X, ∀ ε > 0, ∃ δ > 0, ∀ x', dist x' x < δ → dist (f x') (f x) < ε := + Continuous f ↔ + ∀ x : X, ∀ ε > 0, ∃ δ > 0, ∀ x', dist x' x < δ → dist (f x') (f x) < ε := Metric.continuous_iff example {X Y : Type _} [MetricSpace X] [MetricSpace Y] {f : X → Y} (hf : Continuous f) :
- @@ -88,7 +84,8 @@ example {s : Set X} (hs : IsClosed s) {u : ℕ → X} (hu : Tendsto u atTop (
 example {s : Set X} : a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, a ∈ Metric.ball b ε := Metric.mem_closure_iff - example {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a)) {s : Set X} (hs : ∀ n, u n ∈ s) : a ∈ closure s := + example {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a)) {s : Set X} (hs : ∀ n, u n ∈ s) : + a ∈ closure s := sorry example {u : ℕ → X} (hu : Tendsto u atTop (𝓝 a)) {s : Set X} (hs : ∀ n, u n ∈ s) : a ∈ closure s := by
- @@ -113,11 +110,13 @@ example {s : Set X} (hs : IsCompact s) {u : ℕ → X} (hu : ∀ n, u n ∈ s) :
 ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (u ∘ φ) atTop (𝓝 a) := hs.tendsto_subseq hu - example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ} (hfs : ContinuousOn f 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 - example {s : Set X} (hs : IsCompact s) (hs' : s.Nonempty) {f : X → ℝ} (hfs : ContinuousOn f s) : + 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
- @@ -130,10 +129,12 @@ example {X : Type _} [MetricSpace X] [CompactSpace X] : IsCompact (univ : Set X)
 #check IsCompact.isClosed example {X : Type _} [MetricSpace X] {Y : Type _} [MetricSpace Y] {f : X → Y} : - UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : X}, dist a b < δ → dist (f a) (f b) < ε := + UniformContinuous f ↔ + ∀ ε > 0, ∃ δ > 0, ∀ {a b : X}, dist a b < δ → dist (f a) (f b) < ε := Metric.uniformContinuous_iff - example {X : Type _} [MetricSpace X] [CompactSpace X] {Y : Type _} [MetricSpace Y] {f : X → Y} + example {X : Type _} [MetricSpace X] [CompactSpace X] + {Y : Type _} [MetricSpace Y] {f : X → Y} (hf : Continuous f) : UniformContinuous f := sorry
- @@ -164,13 +165,16 @@ example {X : Type _} [MetricSpace X] [CompactSpace X] {Y : Type _} [MetricSpace
 intro hxx' exact H (x, x') hxx' - example (u : ℕ → X) : CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε := + example (u : ℕ → X) : + CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε := Metric.cauchySeq_iff - example (u : ℕ → X) : CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, dist (u n) (u N) < ε := + example (u : ℕ → X) : + CauchySeq u ↔ ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, dist (u n) (u N) < ε := Metric.cauchySeq_iff' - example [CompleteSpace X] (u : ℕ → X) (hu : CauchySeq u) : ∃ x, Tendsto u atTop (𝓝 x) := + example [CompleteSpace X] (u : ℕ → X) (hu : CauchySeq u) : + ∃ x, Tendsto u atTop (𝓝 x) := cauchySeq_tendsto_of_complete hu open BigOperators
- @@ -240,18 +244,21 @@ example [CompleteSpace X] (f : ℕ → Set X) (ho : ∀ n, IsOpen (f n)) (hd :
 intro x rw [mem_closure_iff_nhds_basis nhds_basis_closedBall] intro ε εpos - /- `ε` is positive. We have to find a point in the ball of radius `ε` around `x` belonging to all - `f n`. For this, we construct inductively a sequence `F n = (c n, r n)` such that the closed ball - `closedBall (c n) (r n)` is included in the previous ball and in `f n`, and such that - `r n` is small enough to ensure that `c n` is a Cauchy sequence. Then `c n` converges to a - limit which belongs to all the `f n`. -/ + /- `ε` is positive. We have to find a point in the ball of radius `ε` around `x` + belonging to all `f n`. For this, we construct inductively a sequence + `F n = (c n, r n)` such that the closed ball `closedBall (c n) (r n)` is included + in the previous ball and in `f n`, and such that `r n` is small enough to ensure + that `c n` is a Cauchy sequence. Then `c n` converges to a limit which belongs + to all the `f n`. -/ let F : ℕ → X × ℝ := fun n => - Nat.recOn n (Prod.mk x (min ε (B 0))) fun n p => Prod.mk (center n p.1 p.2) (radius n p.1 p.2) + Nat.recOn n (Prod.mk x (min ε (B 0))) + fun n p => Prod.mk (center n p.1 p.2) (radius n p.1 p.2) let c : ℕ → X := fun n => (F n).1 let r : ℕ → ℝ := fun n => (F n).2 have rpos : ∀ n, 0 < r n := by sorry have rB : ∀ n, r n ≤ B n := by sorry - have incl : ∀ n, closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n := by sorry + have incl : ∀ n, closedBall (c (n + 1)) (r (n + 1)) ⊆ closedBall (c n) (r n) ∩ f n := by + sorry have cdist : ∀ n, dist (c n) (c (n + 1)) ≤ B n := by sorry have : CauchySeq c := cauchySeq_of_le_geometric_two' cdist -- as the sequence `c n` is Cauchy in a complete space, it converges to a limit `y`.
src/C07_Topology/solutions/Solutions_S03_Topological_Spaces.lean
- @@ -1,9 +1,7 @@
 import Mathlib.Topology.Instances.Real import Mathlib.Analysis.NormedSpace.BanachSteinhaus - open Set Filter - - open Topology Filter + open Set Filter Topology section variable {X : Type _} [TopologicalSpace X]
- @@ -17,7 +15,8 @@ example : IsOpen (∅ : Set X) :=
 example {ι : Type _} {s : ι → Set X} (hs : ∀ i, IsOpen <| s i) : IsOpen (⋃ i, s i) := isOpen_iUnion hs - example {ι : Type _} [Fintype ι] {s : ι → Set X} (hs : ∀ i, IsOpen <| s i) : IsOpen (⋂ i, s i) := + example {ι : Type _} [Fintype ι] {s : ι → Set X} (hs : ∀ i, IsOpen <| s i) : + IsOpen (⋂ i, s i) := isOpen_iInter hs variable {Y : Type _} [TopologicalSpace Y]
- @@ -86,8 +85,10 @@ example (T_X : TopologicalSpace X) (T_Y : TopologicalSpace Y) (f : X → Y) :
 Continuous f ↔ TopologicalSpace.coinduced f T_X ≤ T_Y := continuous_iff_coinduced_le - example {Z : Type _} (f : X → Y) (T_X : TopologicalSpace X) (T_Z : TopologicalSpace Z) (g : Y → Z) : - @Continuous Y Z (TopologicalSpace.coinduced f T_X) T_Z g ↔ @Continuous X Z T_X T_Z (g ∘ f) := by + example {Z : Type _} (f : X → Y) (T_X : TopologicalSpace X) (T_Z : TopologicalSpace Z) + (g : Y → Z) : + @Continuous Y Z (TopologicalSpace.coinduced f T_X) T_Z g ↔ + @Continuous X Z T_X T_Z (g ∘ f) := by rw [continuous_iff_coinduced_le, coinduced_compose, continuous_iff_coinduced_le] example (ι : Type _) (X : ι → Type _) (T_X : ∀ i, TopologicalSpace <| X i) :
- @@ -103,16 +104,19 @@ example [TopologicalSpace X] [RegularSpace X] (a : X) :
 (𝓝 a).HasBasis (fun s : Set X => s ∈ 𝓝 a ∧ IsClosed s) id := closed_nhds_basis a - example [TopologicalSpace X] {x : X} : (𝓝 x).HasBasis (fun t : Set X => t ∈ 𝓝 x ∧ IsOpen t) id := + example [TopologicalSpace X] {x : X} : + (𝓝 x).HasBasis (fun t : Set X => t ∈ 𝓝 x ∧ IsOpen t) id := nhds_basis_opens' x - theorem aux {X Y A : Type _} [TopologicalSpace X] {c : A → X} {f : A → Y} {x : X} {F : Filter Y} - (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) : + theorem aux {X Y A : Type _} [TopologicalSpace X] {c : A → X} + {f : A → Y} {x : X} {F : Filter Y} + (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) : ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := sorry - example {X Y A : Type _} [TopologicalSpace X] {c : A → X} {f : A → Y} {x : X} {F : Filter Y} - (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) : + example {X Y A : Type _} [TopologicalSpace X] {c : A → X} + {f : A → Y} {x : X} {F : Filter Y} + (h : Tendsto f (comap c (𝓝 x)) F) {V' : Set Y} (V'_in : V' ∈ F) : ∃ V ∈ 𝓝 x, IsOpen V ∧ c ⁻¹' V ⊆ f ⁻¹' V' := by simpa [and_assoc] using ((nhds_basis_opens' x).comap c).tendsto_left_iff.mp h V' V'_in
- @@ -148,7 +152,8 @@ example [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {A : Set X} (hA :
 have lim : Tendsto f (𝓝 a) (𝓝 <| φ a) := by simpa [nhds_induced] using hφ a exact tendsto_nhds_unique lim f_cont.continuousAt - example [TopologicalSpace X] [TopologicalSpace.FirstCountableTopology X] {s : Set X} {a : X} : + example [TopologicalSpace X] [TopologicalSpace.FirstCountableTopology X] + {s : Set X} {a : X} : a ∈ closure s ↔ ∃ u : ℕ → X, (∀ n, u n ∈ s) ∧ Tendsto u atTop (𝓝 a) := mem_closure_iff_seq_limit
- @@ -157,7 +162,8 @@ variable [TopologicalSpace X]
 example {F : Filter X} {x : X} : ClusterPt x F ↔ NeBot (𝓝 x ⊓ F) := Iff.rfl - example {s : Set X} : IsCompact s ↔ ∀ (F : Filter X) [NeBot F], F ≤ 𝓟 s → ∃ a ∈ s, ClusterPt a F := + example {s : Set X} : + IsCompact s ↔ ∀ (F : Filter X) [NeBot F], F ≤ 𝓟 s → ∃ a ∈ s, ClusterPt a F := Iff.rfl example [TopologicalSpace.FirstCountableTopology X] {s : Set X} {u : ℕ → X} (hs : IsCompact s)