Update Thu Dec 7 10:02:33 EST 2023

Homework.html

@@ -70,6 +70,7 @@
 <li class="toctree-l2"><a class="reference internal" href="#homework-7">Homework 7</a></li>
 <li class="toctree-l2"><a class="reference internal" href="#homework-8">Homework 8</a></li>
 <li class="toctree-l2"><a class="reference internal" href="#homework-9">Homework 9</a></li>
+<li class="toctree-l2"><a class="reference internal" href="#homework-10">Homework 10</a></li>
 </ul>
 </li>
 </ul>
@@ -698,6 +699,103 @@
 </li>
 </ol>
 </section>
+<section id="homework-10">
+<span id="hw10"></span><h2>Homework 10<a class="headerlink" href="#homework-10" title="Permalink to this headline">&#61633;</a></h2>
+<ol class="arabic">
+<li><p>Prove or disprove that
+<span class="math notranslate nohighlight">\(\{m:\mathbb{Z} \mid m\ge 10\}\subseteq \{n:\mathbb{Z} \mid n^3-7n^2\geq 4n\}\)</span>.</p>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[autograded 4]</span>
+<span class="kd">theorem</span> <span class="n">problem1a</span> <span class="o">:</span> <span class="o">{</span> <span class="n">m</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">m</span> <span class="bp">&#8805;</span> <span class="mi">10</span> <span class="o">}</span> <span class="bp">&#8838;</span> <span class="o">{</span> <span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">-</span> <span class="mi">7</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8805;</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">n</span> <span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+
+<span class="kd">@[autograded 4]</span>
+<span class="kd">theorem</span> <span class="n">problem1b</span> <span class="o">:</span> <span class="o">{</span> <span class="n">m</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">m</span> <span class="bp">&#8805;</span> <span class="mi">10</span> <span class="o">}</span> <span class="bp">&#8840;</span> <span class="o">{</span> <span class="n">n</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">3</span> <span class="bp">-</span> <span class="mi">7</span> <span class="bp">*</span> <span class="n">n</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">&#8805;</span> <span class="mi">4</span> <span class="bp">*</span> <span class="n">n</span> <span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+</pre></div>
+</div>
+</li>
+<li><p>Prove or disprove that
+<span class="math notranslate nohighlight">\(\{t:\mathbb{R} \mid t^2-5t+4=0\}=\{s:\mathbb{R} \mid s=4\}\)</span>.</p>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[autograded 4]</span>
+<span class="kd">theorem</span> <span class="n">problem2a</span> <span class="o">:</span> <span class="o">{</span> <span class="n">t</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">|</span> <span class="n">t</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">t</span> <span class="bp">+</span> <span class="mi">4</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">}</span> <span class="bp">=</span> <span class="o">{</span> <span class="n">s</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">|</span> <span class="n">s</span> <span class="bp">=</span> <span class="mi">4</span> <span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+
+<span class="kd">@[autograded 4]</span>
+<span class="kd">theorem</span> <span class="n">problem2b</span> <span class="o">:</span> <span class="o">{</span> <span class="n">t</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">|</span> <span class="n">t</span> <span class="bp">^</span> <span class="mi">2</span> <span class="bp">-</span> <span class="mi">5</span> <span class="bp">*</span> <span class="n">t</span> <span class="bp">+</span> <span class="mi">4</span> <span class="bp">=</span> <span class="mi">0</span> <span class="o">}</span> <span class="bp">&#8800;</span> <span class="o">{</span> <span class="n">s</span> <span class="o">:</span> <span class="n">&#8477;</span> <span class="bp">|</span> <span class="n">s</span> <span class="bp">=</span> <span class="mi">4</span> <span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+</pre></div>
+</div>
+</li>
+<li><p>Prove or disprove that <span class="math notranslate nohighlight">\(\{1,2,3\}=\{1,2\}\)</span>.</p>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[autograded 4]</span>
+<span class="kd">theorem</span> <span class="n">problem3a</span> <span class="o">:</span> <span class="o">{</span><span class="mi">1</span><span class="o">,</span> <span class="mi">2</span><span class="o">,</span> <span class="mi">3</span><span class="o">}</span> <span class="bp">=</span> <span class="o">{</span><span class="mi">1</span><span class="o">,</span> <span class="mi">2</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+
+<span class="kd">@[autograded 4]</span>
+<span class="kd">theorem</span> <span class="n">problem3b</span> <span class="o">:</span> <span class="o">{</span><span class="mi">1</span><span class="o">,</span> <span class="mi">2</span><span class="o">,</span> <span class="mi">3</span><span class="o">}</span> <span class="bp">&#8800;</span> <span class="o">{</span><span class="mi">1</span><span class="o">,</span> <span class="mi">2</span><span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+</pre></div>
+</div>
+</li>
+<li><p>Prove that
+<span class="math notranslate nohighlight">\(\{r:\mathbb{Z}\mid r\equiv 7\mod 10\}\subseteq \{s:\mathbb{Z}\mid s\equiv 1\mod 2\}\cap\{t:\mathbb{Z}\mid t\equiv 2\mod 5\}\)</span>.</p>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">@[autograded 4]</span>
+<span class="kd">theorem</span> <span class="n">problem4</span> <span class="o">:</span> <span class="o">{</span> <span class="n">r</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">r</span> <span class="bp">&#8801;</span> <span class="mi">7</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">10</span><span class="o">]</span> <span class="o">}</span>
+    <span class="bp">&#8838;</span> <span class="o">{</span> <span class="n">s</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">s</span> <span class="bp">&#8801;</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">2</span><span class="o">]</span> <span class="o">}</span> <span class="bp">&#8745;</span> <span class="o">{</span> <span class="n">t</span> <span class="o">:</span> <span class="n">&#8484;</span> <span class="bp">|</span> <span class="n">t</span> <span class="bp">&#8801;</span> <span class="mi">2</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span> <span class="o">}</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+</pre></div>
+</div>
+</li>
+<li><p>Determine which of these properties hold for the relation <span class="math notranslate nohighlight">\(\sim\)</span> on <span class="math notranslate nohighlight">\(\mathbb{Z}\)</span>,
+defined by, <span class="math notranslate nohighlight">\(x\sim y\)</span> if <span class="math notranslate nohighlight">\(y\equiv x+1\mod 5\)</span>:</p>
+<ol class="arabic simple">
+<li><p>reflexive</p></li>
+<li><p>symmetric</p></li>
+<li><p>antisymmetric</p></li>
+<li><p>transitive</p></li>
+</ol>
+<p>Also (for submission only on paper, not in Lean)</p>
+<ol class="arabic simple" start="5">
+<li><p>Sketch (a representative portion of) this relation as a directed graph.</p></li>
+</ol>
+<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">local</span> <span class="kd">infix</span><span class="o">:</span><span class="mi">50</span> <span class="s2">&quot;&#8764;&quot;</span> <span class="bp">=&gt;</span> <span class="k">fun</span> <span class="o">(</span><span class="n">x</span> <span class="n">y</span> <span class="o">:</span> <span class="n">&#8484;</span><span class="o">)</span> <span class="bp">&#8614;</span> <span class="n">y</span> <span class="bp">&#8801;</span> <span class="n">x</span> <span class="bp">+</span> <span class="mi">1</span> <span class="o">[</span><span class="n">ZMOD</span> <span class="mi">5</span><span class="o">]</span>
+
+<span class="kd">@[autograded 2]</span>
+<span class="kd">theorem</span> <span class="n">problem51a</span> <span class="o">:</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+
+<span class="kd">@[autograded 2]</span>
+<span class="kd">theorem</span> <span class="n">problem51b</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Reflexive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+
+<span class="kd">@[autograded 2]</span>
+<span class="kd">theorem</span> <span class="n">problem52a</span> <span class="o">:</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+
+<span class="kd">@[autograded 2]</span>
+<span class="kd">theorem</span> <span class="n">problem52b</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Symmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+
+<span class="kd">@[autograded 3]</span>
+<span class="kd">theorem</span> <span class="n">problem53a</span> <span class="o">:</span> <span class="n">AntiSymmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+
+<span class="kd">@[autograded 3]</span>
+<span class="kd">theorem</span> <span class="n">problem53b</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">AntiSymmetric</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+
+<span class="kd">@[autograded 2]</span>
+<span class="kd">theorem</span> <span class="n">problem54a</span> <span class="o">:</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+
+<span class="kd">@[autograded 2]</span>
+<span class="kd">theorem</span> <span class="n">problem54b</span> <span class="o">:</span> <span class="bp">&#172;</span> <span class="n">Transitive</span> <span class="o">(</span><span class="bp">&#183;</span> <span class="bp">&#8764;</span> <span class="bp">&#183;</span><span class="o">)</span> <span class="o">:=</span> <span class="kd">by</span>
+  <span class="gr">sorry</span>
+</pre></div>
+</div>
+</li>
+</ol>
+</section>
 </section>
 
 

_sources/Homework.rst.txt

@@ -13,3 +13,4 @@ Homework
 .. include:: Homework/hw7.inc
 .. include:: Homework/hw8.inc
 .. include:: Homework/hw9.inc
+.. include:: Homework/hw10.inc

index.html

@@ -202,6 +202,7 @@ <h1>The mechanics of proof<a class="headerlink" href="#the-mechanics-of-proof" t
 <li class="toctree-l2"><a class="reference internal" href="Homework.html#homework-7">Homework 7</a></li>
 <li class="toctree-l2"><a class="reference internal" href="Homework.html#homework-8">Homework 8</a></li>
 <li class="toctree-l2"><a class="reference internal" href="Homework.html#homework-9">Homework 9</a></li>
+<li class="toctree-l2"><a class="reference internal" href="Homework.html#homework-10">Homework 10</a></li>
 </ul>
 </li>
 </ul>