diff --git a/MIL.lean b/MIL.lean index d46cd4c3..5b403c87 100644 --- a/MIL.lean +++ b/MIL.lean @@ -17,20 +17,23 @@ import MIL.C04_Sets_and_Functions.S03_The_Schroeder_Bernstein_Theorem import MIL.C05_Elementary_Number_Theory.S01_Irrational_Roots import MIL.C05_Elementary_Number_Theory.S02_Induction_and_Recursion import MIL.C05_Elementary_Number_Theory.S03_Infinitely_Many_Primes -import MIL.C06_Structures.S01_Structures -import MIL.C06_Structures.S02_Algebraic_Structures -import MIL.C06_Structures.S03_Building_the_Gaussian_Integers -import MIL.C07_Hierarchies.S01_Basics -import MIL.C07_Hierarchies.S02_Morphisms -import MIL.C07_Hierarchies.S03_Subobjects -import MIL.C08_Groups_and_Rings.S01_Groups -import MIL.C08_Groups_and_Rings.S02_Rings -import MIL.C09_Topology.S01_Filters -import MIL.C09_Topology.S02_Metric_Spaces -import MIL.C09_Topology.S03_Topological_Spaces -import MIL.C10_Differential_Calculus.S01_Elementary_Differential_Calculus -import MIL.C10_Differential_Calculus.S02_Differential_Calculus_in_Normed_Spaces -import MIL.C11_Integration_and_Measure_Theory.S01_Elementary_Integration -import MIL.C11_Integration_and_Measure_Theory.S02_Measure_Theory -import MIL.C11_Integration_and_Measure_Theory.S03_Integration +import MIL.C06_Discrete_Mathematics.S01_More_Induction +import MIL.C06_Discrete_Mathematics.S02_Finsets_and_Fintypes +import MIL.C06_Discrete_Mathematics.S03_Counting_Arguments +import MIL.C07_Structures.S01_Structures +import MIL.C07_Structures.S02_Algebraic_Structures +import MIL.C07_Structures.S03_Building_the_Gaussian_Integers +import MIL.C08_Hierarchies.S01_Basics +import MIL.C08_Hierarchies.S02_Morphisms +import MIL.C08_Hierarchies.S03_Subobjects +import MIL.C09_Groups_and_Rings.S01_Groups +import MIL.C09_Groups_and_Rings.S02_Rings +import MIL.C10_Topology.S01_Filters +import MIL.C10_Topology.S02_Metric_Spaces +import MIL.C10_Topology.S03_Topological_Spaces +import MIL.C11_Differential_Calculus.S01_Elementary_Differential_Calculus +import MIL.C11_Differential_Calculus.S02_Differential_Calculus_in_Normed_Spaces +import MIL.C12_Integration_and_Measure_Theory.S01_Elementary_Integration +import MIL.C12_Integration_and_Measure_Theory.S02_Measure_Theory +import MIL.C12_Integration_and_Measure_Theory.S03_Integration import MIL.Common diff --git a/MIL/C06_Discrete_Mathematics/S01_More_Induction.lean b/MIL/C06_Discrete_Mathematics/S01_More_Induction.lean index 03daee92..e148b72c 100644 --- a/MIL/C06_Discrete_Mathematics/S01_More_Induction.lean +++ b/MIL/C06_Discrete_Mathematics/S01_More_Induction.lean @@ -11,7 +11,7 @@ namespace more_induction More Induction -------------- -In :numref:`induction_and_recursion` we saw how to define the factorial function by recursion on +In :numref:`section_induction_and_recursion` we saw how to define the factorial function by recursion on the natural numbers. EXAMPLES: -/ -- QUOTE: @@ -94,7 +94,7 @@ EXAMPLES: -/ The ``@[simp]`` annotation means that the simplifier will use the defining equations. You can also apply them by writing ``rw [fib]``. Below it will be helpful to give a name to the ``n+2`` case. -EXAMPLES:-/ +EXAMPLES: -/ -- QUOTE: theorem fib_add_two (n : ℕ) : fib (n+2) = fib n + fib (n+1) := rfl @@ -105,7 +105,7 @@ example (n : ℕ) : fib (n+2) = fib n + fib (n+1) := by rw [fib] Using Lean's notation for recursive functions, you can carry out proofs by induction on the natural numbers that mirror the recursive definition of ``fib``. The following example provides an explicit formula for the nth Fibonacci number in terms of -the golden mean, ``φ``, and its conjugate, ``φ '``. +the golden mean, ``φ``, and its conjugate, ``φ'``. We have to tell Lean that we don't expect our definitions to generate code because the arithmetic operations on the real numbers are not computable. EXAMPLES: -/ @@ -229,6 +229,7 @@ example (n : ℕ): (fib n)^2 + (fib (n + 1))^2 = fib (2 * n + 1) := sorry EXAMPLES: -/ by rw [two_mul, fib_add, pow_two, pow_two] +-- QUOTE. -- BOTH: /- TEXT: diff --git a/MIL/C06_Discrete_Mathematics/S02_Finsets_and_Fintypes.lean b/MIL/C06_Discrete_Mathematics/S02_Finsets_and_Fintypes.lean index d4762fa8..c4d1a950 100644 --- a/MIL/C06_Discrete_Mathematics/S02_Finsets_and_Fintypes.lean +++ b/MIL/C06_Discrete_Mathematics/S02_Finsets_and_Fintypes.lean @@ -74,7 +74,7 @@ If you step through the last example below, you will see applying ``ext`` followed by ``simp`` reduces the identity to a problem in propositional logic. As an exercise, you can try proving some of set identities from -:numref:`Chapter %s `, transported to finsets. +:numref:`Chapter %s `, transported to finsets. You have already seen the notation ``Finset.range n`` for the finite set of natural numbers :math:`\{ 0, 1, \ldots, n-1 \}`. @@ -136,7 +136,7 @@ set_option pp.notation false in Unfortunately, we cannot use set-builder notation with finsets: we can't write an expression like ``{ x : ℕ | Even x ∧ x < 5 }`` because Lean can't straightforwardly infer that such a set is finite. However, you can start with a finset and separate the elements you want using ``Finset.filter``. -TEXT.-/ +EXAMPLES: -/ -- QUOTE: #check (range n).filter Even #check (range n).filter (fun x ↦ Even x ∧ x ≠ 3) @@ -204,7 +204,7 @@ has a property, show that the empty set has the property and that the property i preserved when we add one new element to a finset. (The ``@`` in ``@insert`` is need in the induction step to give names to the parameters ``a`` and ``s`` because they have been marked implicit. ) -EXAMPLE: -/ +EXAMPLES: -/ -- QUOTE: #check Finset.induction @@ -309,7 +309,7 @@ end We have already seen a prototypical example of a fintype, namely, the types ``Fin n`` for each ``n``. But Lean also recognizes that the fintypes are closed under operations like the product operation. --/ +EXAMPLES: -/ -- QUOTE: example : Fintype.card (Fin 5) = 5 := by simp example : Fintype.card ((Fin 5) × (Fin 3)) = 15 := by simp diff --git a/MIL/C06_Discrete_Mathematics/S03_Counting_Arguments.lean b/MIL/C06_Discrete_Mathematics/S03_Counting_Arguments.lean index cde987c8..eae0bc37 100644 --- a/MIL/C06_Discrete_Mathematics/S03_Counting_Arguments.lean +++ b/MIL/C06_Discrete_Mathematics/S03_Counting_Arguments.lean @@ -97,6 +97,7 @@ theorem doubleCounting {α β : Type*} (s : Finset α) (t : Finset β) -- congr; ext b; apply h_right apply Finset.sum_congr rfl h_right _ ≤ t.card := by simp +-- QUOTE. /- TEXT: An exercise from Bhavik. Also: replace = by ≤ in the previous theorem. diff --git a/sphinx_source/unixode.sty b/sphinx_source/unixode.sty index f909a83e..075b375f 100644 --- a/sphinx_source/unixode.sty +++ b/sphinx_source/unixode.sty @@ -81,7 +81,7 @@ \newunicodechar{⊞}{\ensuremath{\boxplus}} \newunicodechar{∇}{\ensuremath{\nabla}} -\newunicodechar{√}{\ensuremath{\sqrt}} +\newunicodechar{√}{\ensuremath{\surd}} \newunicodechar{⬝}{\ensuremath{\cdot}} \newunicodechar{•}{\ensuremath{\cdot}}