Skip to content

Commit

Permalink
More tweaks.
Browse files Browse the repository at this point in the history
  • Loading branch information
@kenmonks
kenmonks committed Aug 30, 2024
1 parent b9a4085 commit 6914ce4
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 14 deletions.
16 changes: 3 additions & 13 deletions math/Linear-Rules.lurch
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
</script>
</div>

<div id="metadata" style="display: none;"><div data-category="settings" data-key="shell style" data-value-type="json">"boxed"</div><div data-category="main" data-key="header" data-value-type="html"><div class="lurch-atom" contenteditable="false" data-metadata_type="&quot;dependency&quot;" data-metadata_description="&quot;none&quot;" data-metadata_filename="&quot;math/Reals-Rules.lurch&quot;" data-metadata_source="&quot;the web&quot;" data-metadata_auto-refresh="true" style="border: 1px solid gray; padding: 0px 1em;"><div class="lurch-atom-metadata" style="display: none;"><div data-key="content">
<div id="metadata" style="display: none;"><div data-category="main" data-key="header" data-value-type="html"><div class="lurch-atom" contenteditable="false" data-metadata_type="&quot;dependency&quot;" data-metadata_description="&quot;none&quot;" data-metadata_filename="&quot;math/Reals-Rules.lurch&quot;" data-metadata_source="&quot;the web&quot;" data-metadata_auto-refresh="true" style="border: 1px solid gray; padding: 0px 1em;"><div class="lurch-atom-metadata" style="display: none;"><div data-key="content">
<div id="loadlink">
<p><a>Open this file in the Lurch web app</a></p>

Expand Down Expand Up @@ -758,18 +758,8 @@
<h3>&nbsp;</h3>
</div></div>
</div></div><div class="lurch-atom-body"><table><colgroup><col><col></colgroup><tbody><tr><td colspan="2"><b>Imported dependency document</b></td></tr><tr><td>Description:</td><td><tt>none</tt></td></tr><tr><td>Filename:</td><td><tt>math/Reals-Rules.lurch</tt></td></tr><tr><td>Source:</td><td>the web</td></tr><tr><td>Auto-refresh:</td><td>yes</td></tr></tbody></table></div></div></div></div>
<div id="document"><h1>Linear</h1>
<div id="document"><h1>Linear Functions</h1>
<div class="lurch-atom" data-metadata_type="&quot;rule&quot;" data-shell_title="Rule:">
<p><strong>Definition of Linear:&nbsp;</strong><span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;If f is linear&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__text">If </span><span class="ML__mathit" style="margin-right: 0.11em;">f</span><span class="ML__text"> is linear</span></span></span></span></span> then <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;f(a*x+b*y)=a*f(x)+b*f(y)&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__mathit" style="margin-right: 0.11em;">f</span><span class="ML__left-right" style="margin-top: -0.19444em; height: 0.8888799999999999em;"><span class="ML__small-delim ML__open">(</span><span class="ML__mathit">a</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit">x</span><span class="ML__cmr">+</span><span class="ML__mathit">b</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.04em;">y</span><span class="ML__small-delim ML__close">)</span></span><span class="ML__cmr">=</span><span class="ML__mathit">a</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.11em;">f</span><span class="ML__left-right" style="margin-top: 0em; height: 0.43056em;"><span class="ML__small-delim ML__open">(</span><span class="ML__mathit">x</span><span class="ML__small-delim ML__close">)</span></span><span class="ML__cmr">+</span><span class="ML__mathit">b</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.11em;">f</span><span class="ML__left-right" style="margin-top: -0.19444em; height: 0.625em;"><span class="ML__small-delim ML__open">(</span><span class="ML__mathit" style="margin-right: 0.04em;">y</span><span class="ML__small-delim ML__close">)</span></span></span></span></span></span>.&nbsp;</p>
</div>
<div class="lurch-atom" data-metadata_type="&quot;rule&quot;" data-shell_title="Rule:">
<p><strong>Definition of Linear:&nbsp;</strong></p>
<div class="lurch-atom" data-metadata_type="&quot;premise&quot;" data-shell_title="">
<p><em>Given</em></p>
<div class="lurch-atom" data-metadata_type="&quot;subproof&quot;" data-shell_title="">
<p><span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;Let a,b,x,y&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__text">Let </span><span class="ML__mathit">a</span><span class="ML__text">, </span><span class="ML__mathit">b</span><span class="ML__text">, </span><span class="ML__mathit">x</span><span class="ML__text">, and </span><span class="ML__mathit" style="margin-right: 0.04em;">y</span></span></span></span></span> be arbitrary and show that<span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;f(a*x+b*y)=a*f(x)+b*f(y)&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__mathit" style="margin-right: 0.11em;">f</span><span class="ML__left-right" style="margin-top: -0.19444em; height: 0.8888799999999999em;"><span class="ML__small-delim ML__open">(</span><span class="ML__mathit">a</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit">x</span><span class="ML__cmr">+</span><span class="ML__mathit">b</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.04em;">y</span><span class="ML__small-delim ML__close">)</span></span><span class="ML__cmr">=</span><span class="ML__mathit">a</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.11em;">f</span><span class="ML__left-right" style="margin-top: 0em; height: 0.43056em;"><span class="ML__small-delim ML__open">(</span><span class="ML__mathit">x</span><span class="ML__small-delim ML__close">)</span></span><span class="ML__cmr">+</span><span class="ML__mathit">b</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.11em;">f</span><span class="ML__left-right" style="margin-top: -0.19444em; height: 0.625em;"><span class="ML__small-delim ML__open">(</span><span class="ML__mathit" style="margin-right: 0.04em;">y</span><span class="ML__small-delim ML__close">)</span></span></span></span></span></span>.</p>
</div>
</div>
<p><em>Conclude&nbsp;<span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;f is linear&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__mathit" style="margin-right: 0.11em;">f</span><span class="ML__text"> is linear</span></span></span></span></span></em></p>
<p><strong>Definition of Linear:&nbsp;</strong><span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;If f is linear&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__text">If </span><span class="ML__mathit" style="margin-right: 0.11em;">f</span><span class="ML__text"> is linear</span></span></span></span></span> then <span class="lurch-atom" contenteditable="false" data-metadata_type="&quot;expression&quot;" data-metadata_lurch-notation="&quot;f(a*x+b*y)=a*f(x)+b*f(y)&quot;"><span class="lurch-atom-body"><span class="ML__latex"><span class="ML__base"><span class="ML__mathit" style="margin-right: 0.11em;">f</span><span class="ML__left-right" style="margin-top: -0.19444em; height: 0.8888799999999999em;"><span class="ML__small-delim ML__open">(</span><span class="ML__mathit">a</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit">x</span><span class="ML__cmr">+</span><span class="ML__mathit">b</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.04em;">y</span><span class="ML__small-delim ML__close">)</span></span><span class="ML__cmr">=</span><span class="ML__mathit">a</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.11em;">f</span><span class="ML__left-right" style="margin-top: 0em; height: 0.43056em;"><span class="ML__small-delim ML__open">(</span><span class="ML__mathit">x</span><span class="ML__small-delim ML__close">)</span></span><span class="ML__cmr">+</span><span class="ML__mathit">b</span><span class="ML__cmr">&sdot;</span><span class="ML__mathit" style="margin-right: 0.11em;">f</span><span class="ML__left-right" style="margin-top: -0.19444em; height: 0.625em;"><span class="ML__small-delim ML__open">(</span><span class="ML__mathit" style="margin-right: 0.04em;">y</span><span class="ML__small-delim ML__close">)</span></span></span></span></span></span>.</p>
</div></div>

2 changes: 1 addition & 1 deletion math/examples/theory.lurch
View file

Large diffs are not rendered by default.

0 comments on commit 6914ce4

Please sign in to comment.