Attention: Maintenance on monday 19.04.2021 from 07:00 - 13:00 (Gitlab and Mattermost are offline!)

Commit 3c208e74 authored by Michael Kohlhase's avatar Michael Kohlhase

bla

parents 0301f4a2 c989e73f
<?xml version="1.0"?>
<!--This OMDoc document is generated from an sTeX-encoded one via LaTeXML, you may want to reconsider editing it.-->
<omdoc xmlns:omdoc="http://omdoc.org/ns" xmlns="http://omdoc.org/ns" xmlns:stex="http://kwarc.info/ns/sTeX" xmlns:om="http://www.openmath.org/OpenMath" xmlns:m="http://www.w3.org/1998/Math/MathML" xml:id="Document"><omdoc:metadata/>
<div xmlns="http://www.w3.org/1999/xhtml" id="p1" class="ltx_para">
<p id="p1.p1" class="ltx_p" about="#p1.p1">[creators=miko]dgraphde
[id=dgraph.de.def]
Ein [dgraph]gerichteterGraph (auch [dgraph]Digraph) ist ein
[structure]Paarstructure <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/dgraph.de.tex#textrange(from=3;36,to=4;55)"><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\structure</om:OMSTR><om:OMV name="V"/></om:OMA><om:OMV name="E"/></om:OMOBJ> aus einer Menge <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/dgraph.de.tex#textrange(from=3;11,to=4;75)"><om:OMV name="V"/></om:OMOBJ> und einer
Menge <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/dgraph.de.tex#textrange(from=4;62,to=5;31)"><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\sseteq</om:OMSTR><om:OMV name="E"/><om:OMSTR>\pair</om:OMSTR><om:OMV name="V"/><om:OMV name="V"/></om:OMA></om:OMOBJ> geordneter Paare &#x201D;uber <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/dgraph.de.tex#textrange(from=4;21,to=5;58)"><om:OMV name="V"/></om:OMOBJ>. Wir nennen <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/dgraph.de.tex#textrange(from=4;5,to=5;74)"><om:OMV name="V"/></om:OMOBJ> die
[vertex]Knoten und <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/dgraph.de.tex#textrange(from=5;39,to=6;31)"><om:OMV name="E"/></om:OMOBJ> die [edge]KantenKante (auch
[edge]B&#x201D;ogenBogen) von <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/dgraph.de.tex#textrange(from=6;2,to=7;38)"><om:OMV name="G"/></om:OMOBJ>.
</p>
</div><omdoc:bibliography files="kwarc"/><omdoc:index/></omdoc>
<?xml version="1.0"?>
<!--This OMDoc document is generated from an sTeX-encoded one via LaTeXML, you may want to reconsider editing it.-->
<omdoc xmlns:omdoc="http://omdoc.org/ns" xmlns="http://omdoc.org/ns" xmlns:stex="http://kwarc.info/ns/sTeX" xmlns:om="http://www.openmath.org/OpenMath" xmlns:m="http://www.w3.org/1998/Math/MathML" xml:id="Document"><omdoc:metadata/>
<div xmlns="http://www.w3.org/1999/xhtml" id="p1" class="ltx_para">
<p id="p1.p1" class="ltx_p" about="#p1.p1">[creators=miko]dgraphen
[id=dgraph.def]
A directedgraph (also called [directed-graph]digraph or
[directed-graph]orientedgraph) is a [structure]pairstructure
<om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/dgraph.en.tex#textrange(from=4;75,to=5;19)"><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\structure</om:OMSTR><om:OMV name="V"/></om:OMA><om:OMV name="E"/></om:OMOBJ> such that <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/dgraph.en.tex#textrange(from=4;56,to=5;33)"><om:OMV name="V"/></om:OMOBJ> is a set and <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/dgraph.en.tex#textrange(from=4;33,to=5;71)"><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\sseteq</om:OMSTR><om:OMV name="E"/><om:OMSTR>\pairs</om:OMSTR><om:OMV name="V"/><om:OMV name="V"/></om:OMA></om:OMOBJ>. We call <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/dgraph.en.tex#textrange(from=4;5,to=5;84)"><om:OMV name="V"/></om:OMOBJ> the
verticesvertex (or [vertex]nodes) and <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/dgraph.en.tex#textrange(from=5;26,to=6;60)"><om:OMV name="E"/></om:OMOBJ> the edges of <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/dgraph.en.tex#textrange(from=5;2,to=6;84)"><om:OMV name="G"/></om:OMOBJ>.
</p>
</div><omdoc:bibliography files="kwarc"/><omdoc:index/></omdoc>
<?xml version="1.0"?>
<!--This OMDoc document is generated from an sTeX-encoded one via LaTeXML, you may want to reconsider editing it.-->
<omdoc xmlns:omdoc="http://omdoc.org/ns" xmlns="http://omdoc.org/ns" xml:id="Document"><omdoc:metadata/>
<div xmlns="http://www.w3.org/1999/xhtml" id="p1" class="ltx_para">
<p id="p1.p1" class="ltx_p" about="#p1.p1">[creators=miko]dgraph
[smglom/mv]structure
[smglom/sets]pair
subsupset
*dgraph
vertex
edge
directedgraph
node
</p>
</div><omdoc:bibliography files="kwarc"/><omdoc:index/></omdoc>
<?xml version="1.0"?>
<!--This OMDoc document is generated from an sTeX-encoded one via LaTeXML, you may want to reconsider editing it.-->
<omdoc xmlns:omdoc="http://omdoc.org/ns" xmlns="http://omdoc.org/ns" xmlns:stex="http://kwarc.info/ns/sTeX" xmlns:om="http://www.openmath.org/OpenMath" xmlns:m="http://www.w3.org/1998/Math/MathML" xml:id="Document"><omdoc:metadata/>
<dl xmlns="http://www.w3.org/1999/xhtml" id="I1" class="ltx_description">
<dt id="I1.ix1" class="ltx_item"><span class=" ltx_tag_description">branch</span></dt>
<dd class="ltx_item">
<div id="I1.ix1.p1" class="ltx_para">
<br class="ltx_break"/>
<ol id="I1.I1" class="ltx_enumerate">
<li id="I1.I1.i1" class="ltx_item" style="list-style-type:none;"><span class=" ltx_tag_enumerate">(a)</span>
<div id="I1.I1.i1.p1" class="ltx_para">
<p id="I1.I1.i1.p1.p1" class="ltx_p" about="#I1.I1.i1.p1.p1">Module <span class="ltx_text ltx_font_typewriter">graph</span>
<br class="ltx_break"/><span class="ltx_text" style="border:1px solid black;">syno-</span> <span class="ltx_text" style="border:1px solid black;">hyper-</span> <span class="ltx_text" style="border:1px solid black;">hypo-</span> <span class="ltx_text" style="border:1px solid black;">mero-</span>nyms
<span class="ltx_text" style="border:1px solid black;">de</span> <span class="ltx_text" style="border:1px solid black;">ro</span> <span class="ltx_text" style="border:1px solid black;">zh</span>
<br class="ltx_break"/>A graph is a <span class="ltx_text" style="color:blue;text-decoration:underline;">structure</span> <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/glossary-entry.tex#textrange(from=7;32,to=8;65)"><om:OMV name="V"/><om:OMV name="E"/></om:OMOBJ> such that <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/glossary-entry.tex#textrange(from=7;6,to=8;79)"><om:OMV name="V"/></om:OMOBJ> is a
<span class="ltx_text" style="color:blue;text-decoration:underline;">set</span> and <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/glossary-entry.tex#textrange(from=8;69,to=9;41)"><om:OMA><om:OMS cd="latexml" name="subset-of-or-equals"/><om:OMV name="E"/><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMV name="V"/><om:OMV name="V"/></om:OMA></om:OMA></om:OMOBJ> is a subset of the set of <span class="ltx_text" style="color:blue;text-decoration:underline;">pairs</span> from <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/glossary-entry.tex#textrange(from=8;2,to=9;89)"><om:OMV name="V"/></om:OMOBJ>.
We call <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/glossary-entry.tex#textrange(from=9;60,to=10;15)"><om:OMV name="V"/></om:OMOBJ> the <span class="ltx_text" style="color:blue;text-decoration:underline;">vertices</span> (or nodes, points,
junctions) and <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/glossary-entry.tex#textrange(from=10;42,to=11;32)"><om:OMV name="E"/></om:OMOBJ> the edges (or lines,
branches, arcs) of <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/glossary-entry.tex#textrange(from=11;2,to=12;46)"><om:OMV name="G"/></om:OMOBJ>.</p>
</div></li>
<li id="I1.I1.i2" class="ltx_item" style="list-style-type:none;"><span class=" ltx_tag_enumerate">(b)</span>
<div id="I1.I1.i2.p1" class="ltx_para">
<p id="I1.I1.i2.p1.p1" class="ltx_p" about="#I1.I1.i2.p1.p1">Module <span class="ltx_text ltx_font_typewriter">inverse function
<br class="ltx_break"/><span class="ltx_text ltx_font_serif" style="border:1px solid black;">syno-</span></span> <span class="ltx_text" style="border:1px solid black;">hyper-</span> <span class="ltx_text" style="border:1px solid black;">hypo-</span> <span class="ltx_text" style="border:1px solid black;">mero-</span>nyms
<span class="ltx_text" style="border:1px solid black;">de</span> <span class="ltx_text" style="border:1px solid black;">ro</span> <span class="ltx_text" style="border:1px solid black;">zh</span>
<br class="ltx_break"/>A branch of a <span class="ltx_text" style="color:blue;text-decoration:underline;">multivalued function</span> <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/glossary-entry.tex#textrange(from=15;23,to=16;59)"><om:OMV name="f"/></om:OMOBJ> is a <span class="ltx_text" style="color:blue;text-decoration:underline;">univalent</span>
sub-relation <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/glossary-entry.tex#textrange(from=16;13,to=17;31)"><om:OMA><om:OMS cd="latexml" name="subset-of-or-equals"/><om:OMV name="b"/><om:OMV name="f"/></om:OMA></om:OMOBJ>.</p>
</div></li>
<li id="I1.I1.i3" class="ltx_item" style="list-style-type:none;"><span class=" ltx_tag_enumerate">(c)</span>
<div id="I1.I1.i3.p1" class="ltx_para">
<p id="I1.I1.i3.p1.p1" class="ltx_p" about="#I1.I1.i3.p1.p1">&#x2026;</p>
</div></li>
</ol>
</div></dd>
<dt id="I1.ix2" class="ltx_item"><span class=" ltx_tag_description">branch curve</span></dt>
<dd class="ltx_item"/>
</dl><omdoc:bibliography files="kwarc"/><omdoc:index/></omdoc>
<?xml version="1.0"?>
<!--This OMDoc document is generated from an sTeX-encoded one via LaTeXML, you may want to reconsider editing it.-->
<omdoc xmlns:omdoc="http://omdoc.org/ns" xmlns="http://omdoc.org/ns" xmlns:stex="http://kwarc.info/ns/sTeX" xmlns:om="http://www.openmath.org/OpenMath" xmlns:m="http://www.w3.org/1998/Math/MathML" xml:id="Document"><omdoc:metadata/>
<div xmlns="http://www.w3.org/1999/xhtml" id="p1" class="ltx_para">
<p id="p1.p1" class="ltx_p" about="#p1.p1">[creators=miko]norm-metricennormmetric-space
<omdoc:obligation assertion="obl.norm-metric.en" induced-by="metric-space"/></p>
</div>
<div xmlns="http://www.w3.org/1999/xhtml" id="p2" class="ltx_para">
<p id="p2.p1" class="ltx_p" about="#p2.p1">[type=obligation,id=obl.norm-metric.en]
<om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms-nvs.en.tex#textrange(from=4;68,to=5;30)"><om:OMA><om:OMS cd="arithmetics" name="minus"/><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\defeq</om:OMSTR><om:OMV name="d"/><om:OMA><om:OMS cd="latexml" name="open-interval"/><om:OMV name="x"/><om:OMV name="y"/></om:OMA><om:OMSTR>\norm</om:OMSTR><om:OMV name="x"/></om:OMA><om:OMV name="y"/></om:OMA></om:OMOBJ> is a [metric-space]distancefunction
[for=obl.norm-metric.en]we prove the three conditions for a distance function:
<om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms-nvs.en.tex#textrange(from=8;85,to=9;12)"><om:OMA><om:OMS cd="equal" name="eq"/><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMV name="d"/><om:OMA><om:OMS cd="latexml" name="open-interval"/><om:OMV name="x"/><om:OMV name="y"/></om:OMA></om:OMA><om:OMI>0</om:OMI></om:OMA></om:OMOBJ>, iff <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms-nvs.en.tex#textrange(from=8;65,to=9;32)"><om:OMA><om:OMS cd="equal" name="eq"/><om:OMA><om:OMS cd="arithmetics" name="minus"/><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\norm</om:OMSTR><om:OMV name="x"/></om:OMA><om:OMV name="y"/></om:OMA><om:OMI>0</om:OMI></om:OMA></om:OMOBJ>, iff <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms-nvs.en.tex#textrange(from=8;49,to=9;45)"><om:OMA><om:OMS cd="equal" name="eq"/><om:OMA><om:OMS cd="arithmetics" name="minus"/><om:OMV name="x"/><om:OMV name="y"/></om:OMA><om:OMI>0</om:OMI></om:OMA></om:OMOBJ> (as <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms-nvs.en.tex#textrange(from=8;31,to=9;59)"><om:OMSTR>\normOp</om:OMSTR></om:OMOBJ> separates points), iff <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms-nvs.en.tex#textrange(from=8;4,to=9;88)"><om:OMA><om:OMS cd="equal" name="eq"/><om:OMV name="x"/><om:OMV name="y"/></om:OMA></om:OMOBJ>.
<om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms-nvs.en.tex#textrange(from=11;73,to=12;39)"><om:OMA><om:OMS cd="multirel" name="multirelation"/><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMV name="d"/><om:OMA><om:OMS cd="latexml" name="open-interval"/><om:OMV name="x"/><om:OMV name="y"/></om:OMA></om:OMA><om:OMS cd="equal" name="eq"/><om:OMA><om:OMS cd="arithmetics" name="minus"/><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\norm</om:OMSTR><om:OMV name="x"/></om:OMA><om:OMV name="y"/></om:OMA><om:OMS cd="equal" name="eq"/><om:OMA><om:OMS cd="arithmetics" name="minus"/><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\norm</om:OMSTR><om:OMV name="y"/></om:OMA><om:OMV name="x"/></om:OMA><om:OMS cd="equal" name="eq"/><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMV name="d"/><om:OMA><om:OMS cd="latexml" name="open-interval"/><om:OMV name="y"/><om:OMV name="x"/></om:OMA></om:OMA></om:OMA></om:OMOBJ> by absolute homogeneity of <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms-nvs.en.tex#textrange(from=11;2,to=12;76)"><om:OMSTR>\normOp</om:OMSTR></om:OMOBJ>.
the triangle inequality for <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms-nvs.en.tex#textrange(from=14;34,to=15;33)"><om:OMV name="d"/></om:OMOBJ> follows from that for <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms-nvs.en.tex#textrange(from=14;2,to=15;65)"><om:OMSTR>\normOp</om:OMSTR></om:OMOBJ>.</p>
</div><omdoc:bibliography files="kwarc"/><omdoc:index/></omdoc>
<?xml version="1.0"?>
<!--This OMDoc document is generated from an sTeX-encoded one via LaTeXML, you may want to reconsider editing it.-->
<omdoc xmlns:omdoc="http://omdoc.org/ns" xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath" xmlns:stex="http://kwarc.info/ns/sTeX" xmlns:m="http://www.w3.org/1998/Math/MathML" xml:id="Document"><omdoc:metadata/>
<div xmlns="http://www.w3.org/1999/xhtml" id="p1" class="ltx_para">
<p id="p1.p1" class="ltx_p" about="#p1.p1">[creators=miko]norm-metricnormmetric-space
<omdoc:requation><om:OMOBJ><om:OMS name="base-set"/></om:OMOBJ><span class="ltx_text ltx_markedasmath">base-set</span></omdoc:requation>
<omdoc:requation><om:OMOBJ><om:OMS name="metric"/></om:OMOBJ><om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms-nvs.tex#textrange(from=3;0,to=3;45)"><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\funcdot</om:OMSTR><om:OMSTR><om:OME><om:OMS cd="moreerrors" name="unexpected"/><om:OMS>Text node: x,y</om:OMS></om:OME><om:OMSTR>\normx-y</om:OMSTR></om:OMSTR></om:OMA></om:OMOBJ></omdoc:requation>
[by=norm-metric]metric-spacenormed-vector-space
[by=norm-metric]distance-functionnorm</p>
</div><omdoc:bibliography files="kwarc"/><omdoc:index/></omdoc>
<?xml version="1.0"?>
<!--This OMDoc document is generated from an sTeX-encoded one via LaTeXML, you may want to reconsider editing it.-->
<omdoc xmlns:omdoc="http://omdoc.org/ns" xmlns="http://omdoc.org/ns" xmlns:stex="http://kwarc.info/ns/sTeX" xmlns:om="http://www.openmath.org/OpenMath" xmlns:m="http://www.w3.org/1998/Math/MathML" xml:id="Document"><omdoc:metadata/>
<div xmlns="http://www.w3.org/1999/xhtml" id="p1" class="ltx_para">
<p id="p1.p1" class="ltx_p" about="#p1.p1">[creators=miko]metric-space
[smglom/numberfields]realnumbers
[smglom/numberfields]numbers-orders
[smglom/sets]functions</p>
</div>
<div xmlns="http://www.w3.org/1999/xhtml" id="p2" class="ltx_para">
<p id="p2.p1" class="ltx_p" about="#p2.p1">[creators=miko]metric-spaceen
Let <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms.tex#textrange(from=8;71,to=9;11)"><om:OMV name="M"/></om:OMOBJ> be a set, then we call a function <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms.tex#textrange(from=8;30,to=9;79)"><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\fun</om:OMSTR><om:OMV name="d"/><om:OMSTR>\pairs</om:OMSTR><om:OMV name="M"/><om:OMV name="M"/><om:OMSTR>\RealNumbers</om:OMSTR></om:OMA></om:OMOBJ> a
distancefunction (or [distance-function]metric) on <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms.tex#textrange(from=9;14,to=10;76)"><om:OMV name="M"/></om:OMOBJ>, iff for all
<om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms.tex#textrange(from=10;46,to=11;21)"><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\minset</om:OMSTR><om:OMV name="x"/></om:OMA><om:OMV name="y"/><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMV name="z"/><om:OMV name="M"/></om:OMA></om:OMOBJ> the following three identities hold:</p>
<ol id="I1" class="ltx_enumerate">
<li id="I1.i1" class="ltx_item" style="list-style-type:none;"><span class=" ltx_tag_enumerate">1.</span>
<div id="I1.i1.p1" class="ltx_para">
<p id="I1.i1.p1.p1" class="ltx_p" about="#I1.i1.p1.p1"><om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms.tex#textrange(from=12;63,to=13;22)"><om:OMA><om:OMS cd="equal" name="eq"/><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMV name="d"/><om:OMA><om:OMS cd="latexml" name="open-interval"/><om:OMV name="x"/><om:OMV name="y"/></om:OMA></om:OMA><om:OMI>0</om:OMI></om:OMA></om:OMOBJ> iff <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms.tex#textrange(from=12;46,to=13;34)"><om:OMA><om:OMS cd="equal" name="eq"/><om:OMV name="x"/><om:OMV name="y"/></om:OMA></om:OMOBJ> (identityofindiscernibles),</p>
</div></li>
<li id="I1.i2" class="ltx_item" style="list-style-type:none;"><span class=" ltx_tag_enumerate">2.</span>
<div id="I1.i2.p1" class="ltx_para">
<p id="I1.i2.p1.p1" class="ltx_p" about="#I1.i2.p1.p1"><om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms.tex#textrange(from=13;38,to=14;27)"><om:OMA><om:OMS cd="equal" name="eq"/><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMV name="d"/><om:OMA><om:OMS cd="latexml" name="open-interval"/><om:OMV name="x"/><om:OMV name="y"/></om:OMA></om:OMA><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMV name="d"/><om:OMA><om:OMS cd="latexml" name="open-interval"/><om:OMV name="y"/><om:OMV name="x"/></om:OMA></om:OMA></om:OMA></om:OMOBJ> (symmetry), and</p>
</div></li>
<li id="I1.i3" class="ltx_item" style="list-style-type:none;"><span class=" ltx_tag_enumerate">3.</span>
<div id="I1.i3.p1" class="ltx_para">
<p id="I1.i3.p1.p1" class="ltx_p" about="#I1.i3.p1.p1"><om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms.tex#textrange(from=14;58,to=15;44)"><om:OMA><om:OMS cd="arithmetics" name="plus"/><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\lethan</om:OMSTR><om:OMV name="d"/><om:OMA><om:OMS cd="latexml" name="open-interval"/><om:OMV name="x"/><om:OMV name="z"/></om:OMA><om:OMV name="d"/><om:OMA><om:OMS cd="latexml" name="open-interval"/><om:OMV name="x"/><om:OMV name="y"/></om:OMA></om:OMA><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMV name="d"/><om:OMA><om:OMS cd="latexml" name="open-interval"/><om:OMV name="y"/><om:OMV name="z"/></om:OMA></om:OMA></om:OMA></om:OMOBJ> (triangleinequality).</p>
</div></li>
</ol>
<p id="p2.p3" class="ltx_p" about="#p2.p3">We call <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms.tex#textrange(from=16;61,to=17;29)"><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\structure</om:OMSTR><om:OMV name="M"/></om:OMA><om:OMV name="d"/></om:OMOBJ> a metricspace with baseset <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms.tex#textrange(from=16;5,to=17;80)"><om:OMV name="M"/></om:OMOBJ> and
metric <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/ms.tex#textrange(from=17;2,to=18;21)"><om:OMV name="d"/></om:OMOBJ>.
</p>
</div><omdoc:bibliography files="kwarc"/><omdoc:index/></omdoc>
<?xml version="1.0"?>
<!--This OMDoc document is generated from an sTeX-encoded one via LaTeXML, you may want to reconsider editing it.-->
<omdoc xmlns:omdoc="http://omdoc.org/ns" xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath" xmlns:stex="http://kwarc.info/ns/sTeX" xmlns:m="http://www.w3.org/1998/Math/MathML" xml:id="Document"><omdoc:metadata/>
<div xmlns="http://www.w3.org/1999/xhtml" id="p1" class="ltx_para">
<p id="p1.p1" class="ltx_p" about="#p1.p1">[creators=miko]norm
[smglom/numberfields]complexnumbers
[smglom/linear-algebra]vector-space
[smglom/numberfields]absolutevalue
[smglom/numberfields]numbers-orders
[smglom/sets]functions</p>
</div><omdoc:symbol name="norm" xml:id="norm.sym"/><omdoc:notation macro_name="normOp" name="norm" nargs="0"><omdoc:prototype><om:OMS name="norm"/></omdoc:prototype><omdoc:rendering><m:mrow><m:mo>|</m:mo><m:mo>&#x22C5;</m:mo><m:mo>|</m:mo></m:mrow></omdoc:rendering><omdoc:rendering ic="variant:double"><m:mrow><m:mo>|</m:mo><m:mo>&#x22C5;</m:mo><m:mo>|</m:mo></m:mrow></omdoc:rendering><omdoc:rendering ic="variant:double"><m:mo cr="fun">|</m:mo><omdoc:render name="arg1" precedence="neginfty"/><m:mo cr="fun">|</m:mo></omdoc:rendering></omdoc:notation><omdoc:notation macro_name="norm" name="norm" nargs="1"><omdoc:prototype><om:OMA><om:OMS cr="fun" name="norm"/><omdoc:expr name="arg1"/></om:OMA></omdoc:prototype><omdoc:rendering><m:mo cr="fun">|</m:mo><omdoc:render name="arg1" precedence="neginfty"/><m:mo cr="fun">|</m:mo></omdoc:rendering></omdoc:notation>
<div xmlns="http://www.w3.org/1999/xhtml" id="p2" class="ltx_para">
<p id="p2.p1" class="ltx_p" about="#p2.p1">[creators=miko]normen
Given a [vector-space]vectorspace <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/nvs.tex#textrange(from=17;39,to=18;52)"><om:OMV name="V"/></om:OMOBJ> over a [subfield]subfield <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/nvs.tex#textrange(from=17;1,to=18;90)"><om:OMV name="F"/></om:OMOBJ>
of the [complexnumbers]complexnumbers, a norm on <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/nvs.tex#textrange(from=18;15,to=19;74)"><om:OMV name="V"/></om:OMOBJ> is a function
<om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/nvs.tex#textrange(from=19;74,to=20;32)"><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\fun</om:OMSTR><om:OMSTR>\normOp</om:OMSTR><om:OMV name="V"/><om:OMSTR>\RealNumbers</om:OMSTR></om:OMA></om:OMOBJ> such that for all <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/nvs.tex#textrange(from=19;25,to=20;63)"><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\inset</om:OMSTR><om:OMV name="a"/><om:OMV name="F"/></om:OMA></om:OMOBJ> and <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/nvs.tex#textrange(from=19;7,to=20;83)"><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\minset</om:OMSTR><om:OMV name="u"/></om:OMA><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMV name="v"/><om:OMV name="V"/></om:OMA></om:OMOBJ></p>
<ol id="I1" class="ltx_enumerate">
<li id="I1.i1" class="ltx_item" style="list-style-type:none;"><span class=" ltx_tag_enumerate">1.</span>
<div id="I1.i1.p1" class="ltx_para">
<p id="I1.i1.p1.p1" class="ltx_p" about="#I1.i1.p1.p1"><om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/nvs.tex#textrange(from=21;75,to=22;57)"><om:OMA><om:OMS cd="equal" name="equal"/><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\norm</om:OMSTR><om:OMV name="a"/><om:OMV name="v"/></om:OMA><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\atimes</om:OMSTR><om:OMSTR>\absolutevalue</om:OMSTR><om:OMV name="a"/></om:OMA><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\norm</om:OMSTR><om:OMV name="v"/></om:OMA></om:OMA></om:OMOBJ> (absolutehomogeneity or
[absolute-homogeneity]absolutescalability).</p>
</div></li>
<li id="I1.i2" class="ltx_item" style="list-style-type:none;"><span class=" ltx_tag_enumerate">2.</span>
<div id="I1.i2.p1" class="ltx_para">
<p id="I1.i2.p1.p1" class="ltx_p" about="#I1.i2.p1.p1"><om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/nvs.tex#textrange(from=23;65,to=24;50)"><om:OMA><om:OMS cd="arithmetics" name="plus"/><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\lethan</om:OMSTR><om:OMSTR>\norm</om:OMSTR><om:OMV name="u"/></om:OMA><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMV name="v"/><om:OMSTR>\norm</om:OMSTR><om:OMV name="u"/></om:OMA><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\norm</om:OMSTR><om:OMV name="v"/></om:OMA></om:OMA></om:OMOBJ> (triangleinequality or
[triangle-inequality]subadditivity).</p>
</div></li>
<li id="I1.i3" class="ltx_item" style="list-style-type:none;"><span class=" ltx_tag_enumerate">3.</span>
<div id="I1.i3.p1" class="ltx_para">
<p id="I1.i3.p1.p1" class="ltx_p" about="#I1.i3.p1.p1">If <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/nvs.tex#textrange(from=25;64,to=26;25)"><om:OMA><om:OMS cd="equal" name="equal"/><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\norm</om:OMSTR><om:OMV name="v"/></om:OMA><om:OMI>0</om:OMI></om:OMA></om:OMOBJ>, then <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/nvs.tex#textrange(from=25;49,to=26;35)"><om:OMV name="v"/></om:OMOBJ> is the zero vector (separatespoints).</p>
</div></li>
</ol>
<p id="p2.p3" class="ltx_p" about="#p2.p3">We call the pair <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/nvs.tex#textrange(from=27;50,to=28;44)"><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\structure</om:OMSTR><om:OMV name="V"/></om:OMA><om:OMSTR>\normOp</om:OMSTR></om:OMOBJ> a normedvectorspace with
norm <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/nvs.tex#textrange(from=28;1,to=29;25)"><om:OMSTR>\normOp</om:OMSTR></om:OMOBJ>
</p>
</div><omdoc:bibliography files="kwarc"/><omdoc:index/></omdoc>
<omdoc:notation>
<omdoc:prototype>
<om:OMA>
<om:OMS cd="slg" cr="fun" name="SLG"/>
<omdoc:expr name="arg1"/>
<omdoc:expr name="arg2"/>
</om:OMA>
</omdoc:prototype>
<omdoc:rendering>
<m:mrow>
<m:mo cr="fun">SL</m:mo>
<m:mo egroup="fence" fence="true">(</m:mo>
<render name="arg1" precedence="500"/>
<m:mo separator="true">,</m:mo>
<render name="arg2" precedence="500"/>
<m:mo egroup="fence" fence="true">)</m:mo>
</m:mrow>
</omdoc:rendering>
</omdoc:notation>
<omdoc:notation>
<omdoc:prototype>
<om:OMA>
<om:OMS cd="slg" cr="fun" name="SLG"/>
<omdoc:expr name="arg1"/>
<omdoc:expr name="arg2"/>
</om:OMA>
</omdoc:prototype>
<omdoc:rendering>
<omdoc:phrase>
<omdoc:phrase cr="fun">special linear group</omdoc:phrase>
<omdoc:phrase>of order <verbalize name="arg1"/></omdoc:phrase>
<omdoc:phrase>over <verbalize name="arg2"/></omdoc:phrase>
</omdoc:phrase>
</omdoc:rendering>
</omdoc:notation>
<?xml version="1.0"?>
<!--This OMDoc document is generated from an sTeX-encoded one via LaTeXML, you may want to reconsider editing it.-->
<omdoc xmlns:omdoc="http://omdoc.org/ns" xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath" xmlns:stex="http://kwarc.info/ns/sTeX" xmlns:m="http://www.w3.org/1998/Math/MathML" xml:id="Document"><omdoc:metadata/>
<div xmlns="http://www.w3.org/1999/xhtml" id="p1" class="ltx_para">
<p id="p1.p1" class="ltx_p" about="#p1.p1">[creators=miko]special-linear-groupen</p>
</div><omdoc:symbol name="SLG" xml:id="SLG.sym"/><omdoc:notation macro_name="SLG" name="SLG" nargs="2"><omdoc:prototype><om:OMA><om:OMS cr="fun" name="SLG"/><omdoc:expr name="arg1"/><omdoc:expr name="arg2"/></om:OMA></omdoc:prototype><omdoc:rendering><m:mrow><m:mtext>special linear group of order&#xA0;</m:mtext><m:mo>&#x2062;</m:mo><omdoc:render name="arg1"/><m:mo>&#x2062;</m:mo><m:mtext>&#xA0;over&#xA0;</m:mtext><m:mo>&#x2062;</m:mo><omdoc:render name="arg2"/></m:mrow></omdoc:rendering></omdoc:notation>
<div xmlns="http://www.w3.org/1999/xhtml" id="p2" class="ltx_para">
<p id="p2.p1" class="ltx_p" about="#p2.p1">The speciallineargroup <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/special-linear-group.en.tex#textrange(from=3;29,to=4;67)"><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMSTR>\SLgroup</om:OMSTR><om:OMV name="n"/><om:OMV name="F"/></om:OMA></om:OMOBJ> of degree <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/special-linear-group.en.tex#textrange(from=3;8,to=4;82)"><om:OMV name="n"/></om:OMOBJ> over a
[field]field <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/special-linear-group.en.tex#textrange(from=4;41,to=5;26)"><om:OMV name="F"/></om:OMOBJ> is the set of <om:OMOBJ stex:srcref="/Users/kohlhase/localmh/MathHub/smglom/smglom-doc/source/blue/datamdl/ex/special-linear-group.en.tex#textrange(from=4;23,to=5;52)"><om:OMA><om:OMS cd="arithmetics" name="times"/><om:OMV name="n"/><om:OMV name="n"/></om:OMA></om:OMOBJ> matrices with
[determinant]determinant 1, with the [group]groupoperations of
ordinary [matrix]matrixmultiplication and [matrix]matrixinversion.
</p>
</div><omdoc:bibliography files="kwarc"/><omdoc:index/></omdoc>
<?xml version="1.0"?>
<!--This OMDoc document is generated from an sTeX-encoded one via LaTeXML, you may want to reconsider editing it.-->
<omdoc xmlns:omdoc="http://omdoc.org/ns" xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath" xmlns:stex="http://kwarc.info/ns/sTeX" xmlns:m="http://www.w3.org/1998/Math/MathML" xml:id="Document"><omdoc:metadata/>
<div xmlns="http://www.w3.org/1999/xhtml" id="p1" class="ltx_para">
<p id="p1.p1" class="ltx_p" about="#p1.p1">[creators=miko]special-linear-group
[smglom/linear-algebra]determinant
[smglom/algebra]field
18F25,20Gxx
speciallineargroup</p>
</div><omdoc:symbol name="special-linear-group" xml:id="special-linear-group.sym"/><omdoc:notation macro_name="SLgroupOp" name="special-linear-group" nargs="0"><omdoc:prototype><om:OMS name="special-linear-group"/></omdoc:prototype><omdoc:rendering><omdoc:text>SL</omdoc:text></omdoc:rendering></omdoc:notation><omdoc:notation macro_name="SLgroup" name="special-linear-group" nargs="2"><omdoc:prototype><om:OMA><om:OMS cr="fun" name="special-linear-group"/><omdoc:expr name="arg1"/><omdoc:expr name="arg2"/></om:OMA></omdoc:prototype><omdoc:rendering><m:merror class="ltx_ERROR undefined undefined" cr="fun"><m:mtext>\SLgroupOp</m:mtext></m:merror><m:mrow><m:mo fence="true">(</m:mo><m:mrow><omdoc:render name="arg1"/><m:mo>,</m:mo><omdoc:render name="arg2"/></m:mrow><m:mo fence="true">)</m:mo></m:mrow></omdoc:rendering></omdoc:notation><omdoc:bibliography files="kwarc"/><omdoc:index/></omdoc>
No preview for this file type
......@@ -78,7 +78,7 @@
\input{intro}
\input{preliminaries}
\input{datamodel}
%\input{implementation} missing files
\input{implementation}% missing files
\ednote{\texttt{implementation.tex} has missing files, commit them from the old laptop}
\input{encoding}
\input{concl}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment