Update dim. 30 mars 2025 16:36:01 CEST

Author: PatrickMassot

C10_Topology.html

@@ -676,7 +676,7 @@ <h3><span class="section-number">10.2.2. </span>Balls, open sets and closed sets
 </div>
 <p>Do the next exercise without using <cite>mem_closure_iff_seq_limit</cite></p>
 <div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">u</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">X</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hu</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Tendsto</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="n">atTop</span><span class="w"> </span><span class="o">(</span><span class="n">&#120029;</span><span class="w"> </span><span class="n">a</span><span class="o">))</span><span class="w"> </span><span class="o">{</span><span class="n">s</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">X</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hs</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">n</span><span class="o">,</span><span class="w"> </span><span class="n">u</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">s</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
-<span class="w">    </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">closure</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:=</span>
+<span class="w">    </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">closure</span><span class="w"> </span><span class="n">s</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
 <span class="w">  </span><span class="gr">sorry</span>
 </pre></div>
 </div>
@@ -762,7 +762,7 @@ <h3><span class="section-number">10.2.4. </span>Uniformly continuous functions<a
 of the distance function on <code class="docutils literal notranslate"><span class="pre">K</span></code>. We can then set <code class="docutils literal notranslate"><span class="pre">&#948;</span> <span class="pre">=</span> <span class="pre">dist</span> <span class="pre">x&#8320;</span> <span class="pre">x&#8321;</span></code> and check everything works.</p>
 <div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">MetricSpace</span><span class="w"> </span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">CompactSpace</span><span class="w"> </span><span class="n">X</span><span class="o">]</span>
 <span class="w">      </span><span class="o">{</span><span class="n">Y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">MetricSpace</span><span class="w"> </span><span class="n">Y</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Y</span><span class="o">}</span>
-<span class="w">    </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Continuous</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">UniformContinuous</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:=</span>
+<span class="w">    </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Continuous</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">UniformContinuous</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
 <span class="w">  </span><span class="gr">sorry</span>
 </pre></div>
 </div>