Commit db116d0e authored by Sven Wille's avatar Sven Wille

no message

parent 3b6f76e6
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/algebra/ringsfields.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/ringsfields.mmt#0.0.0:3370.113.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/smglom/algebra"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import arith http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import sets http://mathhub.info/MitM/smglom/typedsets"/><mref name="[http://mathhub.info/MitM/smglom/algebra?Ringoid]" target="http://mathhub.info/MitM/smglom/algebra?Ringoid"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/ringsfields.mmt#219.6.0:232.6.13"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/ringsfields.mmt#625.23.0:661.23.36"/></metadata>MiKo: refactor this with Ringoid</opaque><mref name="[http://mathhub.info/MitM/smglom/algebra?Rig]" target="http://mathhub.info/MitM/smglom/algebra?Rig"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/ringsfields.mmt#663.24.0:672.24.9"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?Ring]" target="http://mathhub.info/MitM/smglom/algebra?Ring"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/ringsfields.mmt#2047.65.0:2057.65.10"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?Field]" target="http://mathhub.info/MitM/smglom/algebra?Field"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/ringsfields.mmt#2658.88.0:2669.88.11"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/MitM/smglom/algebra/ringsfields.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/ringsfields.mmt#0.0.0:3391.113.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/smglom/algebra"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import arith http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import sets http://mathhub.info/MitM/smglom/typedsets"/><mref name="[http://mathhub.info/MitM/smglom/algebra?Ringoid]" target="http://mathhub.info/MitM/smglom/algebra?Ringoid"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/ringsfields.mmt#219.6.0:232.6.13"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/ringsfields.mmt#625.23.0:661.23.36"/></metadata>MiKo: refactor this with Ringoid</opaque><mref name="[http://mathhub.info/MitM/smglom/algebra?Rig]" target="http://mathhub.info/MitM/smglom/algebra?Rig"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/ringsfields.mmt#663.24.0:672.24.9"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?Ring]" target="http://mathhub.info/MitM/smglom/algebra?Ring"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/ringsfields.mmt#2047.65.0:2057.65.10"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/algebra?Field]" target="http://mathhub.info/MitM/smglom/algebra?Field"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/algebra/ringsfields.mmt#2658.88.0:2669.88.11"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#0.0.0:7564.192.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import lfxcop http://gl.mathhub.info/MMT/LFX/Coproducts"/><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#165.5.0:185.5.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#466.16.0:490.16.24"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?InductiveNaturalNumbers]" target="http://mathhub.info/MitM/smglom/arithmetics?InductiveNaturalNumbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#4608.102.0:4638.102.30"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?INatArith]" target="http://mathhub.info/MitM/smglom/arithmetics?INatArith"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#4925.118.0:4940.118.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?Between]" target="http://mathhub.info/MitM/smglom/arithmetics?Between"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#5534.147.0:5547.147.13"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NatConversions]" target="http://mathhub.info/MitM/smglom/arithmetics?NatConversions"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#6027.159.0:6047.159.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?INatProps]" target="http://mathhub.info/MitM/smglom/arithmetics?INatProps"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#6299.171.0:6314.171.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?CompDec]" target="http://mathhub.info/MitM/smglom/arithmetics?CompDec"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#6559.180.0:6572.180.13"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#0.0.0:7753.196.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import lfxcop http://gl.mathhub.info/MMT/LFX/Coproducts"/><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#165.5.0:185.5.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#466.16.0:490.16.24"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?InductiveNaturalNumbers]" target="http://mathhub.info/MitM/smglom/arithmetics?InductiveNaturalNumbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#4797.106.0:4827.106.30"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?INatArith]" target="http://mathhub.info/MitM/smglom/arithmetics?INatArith"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#5114.122.0:5129.122.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?Between]" target="http://mathhub.info/MitM/smglom/arithmetics?Between"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#5723.151.0:5736.151.13"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NatConversions]" target="http://mathhub.info/MitM/smglom/arithmetics?NatConversions"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#6216.163.0:6236.163.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?INatProps]" target="http://mathhub.info/MitM/smglom/arithmetics?INatProps"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#6488.175.0:6503.175.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?CompDec]" target="http://mathhub.info/MitM/smglom/arithmetics?CompDec"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#6748.184.0:6761.184.13"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/arithmetics/reals.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/reals.mmt#0.0.0:4245.100.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><mref name="[http://mathhub.info/MitM/smglom/arithmetics?RealNumbers]" target="http://mathhub.info/MitM/smglom/arithmetics?RealNumbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/reals.mmt#108.4.0:125.4.17"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics]" target="http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/reals.mmt#369.15.0:390.15.21"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?ExtendedReals]" target="http://mathhub.info/MitM/smglom/arithmetics?ExtendedReals"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/reals.mmt#3863.86.0:3882.86.19"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?RealProperties]" target="http://mathhub.info/MitM/smglom/arithmetics?RealProperties"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/reals.mmt#4116.96.0:4136.96.20"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/MitM/smglom/arithmetics/reals.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/reals.mmt#0.0.0:4421.104.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><mref name="[http://mathhub.info/MitM/smglom/arithmetics?RealNumbers]" target="http://mathhub.info/MitM/smglom/arithmetics?RealNumbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/reals.mmt#108.4.0:125.4.17"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics]" target="http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/reals.mmt#369.15.0:390.15.21"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?ExtendedReals]" target="http://mathhub.info/MitM/smglom/arithmetics?ExtendedReals"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/reals.mmt#4039.90.0:4058.90.19"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?RealProperties]" target="http://mathhub.info/MitM/smglom/arithmetics?RealProperties"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/reals.mmt#4292.100.0:4312.100.20"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/calculus/domains.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/domains.mmt#0.0.0:4608.130.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/smglom/calculus"/><instruction text="import top http://mathhub.info/MitM/smglom"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import ts http://mathhub.info/MitM/smglom/typedsets"/><instruction text="import arith http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import fnd http://mathhub.info/MitM/Foundation"/><instruction text="import lfx http://gl.mathhub.info/MMT/LFX/Sigma"/><instruction text="import meta http://cds.omdoc.org/mmt"/><mref name="[http://mathhub.info/MitM/smglom/calculus?Intervals]" target="http://mathhub.info/MitM/smglom/calculus?Intervals"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/domains.mmt#756.21.0:771.21.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/calculus?OneCuboid]" target="http://mathhub.info/MitM/smglom/calculus?OneCuboid"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/domains.mmt#2176.59.0:2191.59.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/calculus?GeneralDomains]" target="http://mathhub.info/MitM/smglom/calculus?GeneralDomains"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/domains.mmt#2702.82.0:2722.82.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/calculus?IntervalPartition]" target="http://mathhub.info/MitM/smglom/calculus?IntervalPartition"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/domains.mmt#3740.111.0:3763.111.23"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/calculus?IntervalCartesianProduct]" target="http://mathhub.info/MitM/smglom/calculus?IntervalCartesianProduct"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/domains.mmt#4046.119.0:4076.119.30"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/MitM/smglom/calculus/domains.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/domains.mmt#0.0.0:5773.151.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/smglom/calculus"/><instruction text="import top http://mathhub.info/MitM/smglom"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import ts http://mathhub.info/MitM/smglom/typedsets"/><instruction text="import arith http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import fnd http://mathhub.info/MitM/Foundation"/><instruction text="import lfx http://gl.mathhub.info/MMT/LFX/Sigma"/><instruction text="import meta http://cds.omdoc.org/mmt"/><mref name="[http://mathhub.info/MitM/smglom/calculus?Intervals]" target="http://mathhub.info/MitM/smglom/calculus?Intervals"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/domains.mmt#756.21.0:771.21.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/calculus?closedIntervalMult]" target="http://mathhub.info/MitM/smglom/calculus?closedIntervalMult"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/domains.mmt#2329.63.0:2353.63.24"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/calculus?OneCuboid]" target="http://mathhub.info/MitM/smglom/calculus?OneCuboid"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/domains.mmt#3341.80.0:3356.80.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/calculus?GeneralDomains]" target="http://mathhub.info/MitM/smglom/calculus?GeneralDomains"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/domains.mmt#3867.103.0:3887.103.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/calculus?IntervalPartition]" target="http://mathhub.info/MitM/smglom/calculus?IntervalPartition"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/domains.mmt#4905.132.0:4928.132.23"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/calculus?IntervalCartesianProduct]" target="http://mathhub.info/MitM/smglom/calculus?IntervalCartesianProduct"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/calculus/domains.mmt#5211.140.0:5241.140.30"/></metadata></mref></omdoc>
\ No newline at end of file
document http://mathhub.info/MitM/smglom/calculus/domains.omdoc
Declares http://mathhub.info/MitM/smglom/calculus/domains.omdoc http://mathhub.info/MitM/smglom/calculus?Intervals
Declares http://mathhub.info/MitM/smglom/calculus/domains.omdoc http://mathhub.info/MitM/smglom/calculus?closedIntervalMult
Declares http://mathhub.info/MitM/smglom/calculus/domains.omdoc http://mathhub.info/MitM/smglom/calculus?OneCuboid
Declares http://mathhub.info/MitM/smglom/calculus/domains.omdoc http://mathhub.info/MitM/smglom/calculus?GeneralDomains
Declares http://mathhub.info/MitM/smglom/calculus/domains.omdoc http://mathhub.info/MitM/smglom/calculus?IntervalPartition
......
highuniverse http://mathhub.info/MitM/smglom/algebra?Field?field
highuniverse http://mathhub.info/MitM/smglom/algebra?Field?koerper
theory http://mathhub.info/MitM/smglom/algebra?Field
HasMeta http://mathhub.info/MitM/smglom/algebra?Field http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/algebra?Field http://mathhub.info/MitM/smglom/algebra?OperationProps
......@@ -71,3 +72,6 @@ Declares http://mathhub.info/MitM/smglom/algebra?Field http://mathhub.info/MitM/
constant http://mathhub.info/MitM/smglom/algebra?Field?field
Declares http://mathhub.info/MitM/smglom/algebra?Field http://mathhub.info/MitM/smglom/algebra?Field?field/abbreviation
constant http://mathhub.info/MitM/smglom/algebra?Field?field/abbreviation
Declares http://mathhub.info/MitM/smglom/algebra?Field http://mathhub.info/MitM/smglom/algebra?Field?koerper
constant http://mathhub.info/MitM/smglom/algebra?Field?koerper
DependsOn http://mathhub.info/MitM/smglom/algebra?Field?koerper?definition http://mathhub.info/MitM/smglom/algebra?Field?field?type
......@@ -17,6 +17,8 @@ dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?l
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?geq
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lessthan
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?morethan
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?leqN
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lessthanN
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?max
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?min
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?mod
......@@ -265,6 +267,20 @@ DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?moretha
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?morethan?definition http://cds.omdoc.org/urtheories?NatSymbols?NAT?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?morethan?definition http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?geq?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?morethan?definition http://mathhub.info/MitM/Foundation?Logic?and?type
Declares http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?leqN
constant http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?leqN
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?leqN?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?leqN?type http://mathhub.info/MitM/Foundation?Logic?prop?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?leqN?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?leqN?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?leqN?definition http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?leq?type
Declares http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lessthanN
constant http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lessthanN
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lessthanN?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lessthanN?type http://mathhub.info/MitM/Foundation?Logic?prop?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lessthanN?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lessthanN?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lessthanN?definition http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?lessthan?type
Declares http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?max
constant http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?max
DependsOn http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics?max?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition
......
......@@ -23,6 +23,7 @@ dataconstructor http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?more
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?max
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?min
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?axiom_realLeqIsRatLeq
dataconstructor http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?leqR
datatypeconstructor http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?NonNegativeRealNumbers
datatypeconstructor http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?PositiveRealNumbers
datatypeconstructor http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?predAsSub
......@@ -268,6 +269,12 @@ DependsOn http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?axiom_real
DependsOn http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?axiom_realLeqIsRatLeq?type http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?leq?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?axiom_realLeqIsRatLeq?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?axiom_realLeqIsRatLeq?type http://mathhub.info/MitM/Foundation?Logic?eq?type
Declares http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?leqR
constant http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?leqR
DependsOn http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?leqR?type http://mathhub.info/MitM/Foundation?Logic?prop?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?leqR?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?leqR?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?leqR?definition http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?leq?type
Declares http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?NonNegativeRealNumbers
constant http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?NonNegativeRealNumbers
DependsOn http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?NonNegativeRealNumbers?definition http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?geq?definition
......
......@@ -2,7 +2,9 @@ datatypeconstructor http://mathhub.info/MitM/smglom/calculus?Intervals?interval
dataconstructor http://mathhub.info/MitM/smglom/calculus?Intervals?closedInterval
datatypeconstructor http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci
datatypeconstructor http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci_alt
dataconstructor http://mathhub.info/MitM/smglom/calculus?Intervals?is_ascending
datatypeconstructor http://mathhub.info/MitM/smglom/calculus?Intervals?ascendingCi
dataconstructor http://mathhub.info/MitM/smglom/calculus?Intervals?isInCi
theory http://mathhub.info/MitM/smglom/calculus?Intervals
HasMeta http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/Foundation?RealLiterals
......@@ -111,6 +113,15 @@ DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci_alt?definit
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci_alt?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci_alt?definition http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?leq?type
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci_alt?definition http://mathhub.info/MitM/Foundation?Logic?and?type
Declares http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/smglom/calculus?Intervals?is_ascending
constant http://mathhub.info/MitM/smglom/calculus?Intervals?is_ascending
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?is_ascending?type http://mathhub.info/MitM/Foundation?Logic?prop?type
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?is_ascending?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?is_ascending?type http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci?type
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?is_ascending?type http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci?definition
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?is_ascending?definition http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?leqR?type
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?is_ascending?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?is_ascending?definition http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci?definition
Declares http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/smglom/calculus?Intervals?ascendingCi
constant http://mathhub.info/MitM/smglom/calculus?Intervals?ascendingCi
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?ascendingCi?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
......@@ -119,3 +130,14 @@ DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?ascendingCi?definit
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?ascendingCi?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?ascendingCi?definition http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci?type
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?ascendingCi?definition http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci?definition
Declares http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/smglom/calculus?Intervals?isInCi
constant http://mathhub.info/MitM/smglom/calculus?Intervals?isInCi
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?isInCi?type http://mathhub.info/MitM/Foundation?Logic?prop?type
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?isInCi?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?isInCi?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?isInCi?type http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci?type
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?isInCi?type http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci?definition
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?isInCi?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?isInCi?definition http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?leq?type
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?isInCi?definition http://mathhub.info/MitM/Foundation?Logic?and?type
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?isInCi?definition http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci?definition
......@@ -15,14 +15,17 @@ theory ListFunctions : base:?Logic =
include http://mathhub.info/MitM/smglom/Datatypes?List ❙
include http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics ❙
length : {A : type} list A ⟶ ℕ ❙
length : {A : type} list A ⟶ ℕ ❘# lengthA 2
lenghtB : {A : type} ⊦ length A (nil A) ≐ 0 ❙
lengthS : {A : type}{a : A}{ls : list A} ⊦ length A (cons A a ls) ≐ Succ (length A ls)❙
lemma_succ_cons : {A : type}{n : ℕ} {a : A}{ls : list A} ⊦ ((Succ n) < length A (cons A a ls)) ⟶ ⊦ n < length A ls ❘# lemma_succ_cons 1 2 3 4 5 ❙
listAt : {A : type}{n : ℕ }{ls : list A} ⊦ n < length A ls ⟶ A
listAtB : {A : type } {a : A} {ls : list A}{h : ⊦ 0 < length A (cons A a ls)} ⊦ listAt A 0 (cons A a ls) h ≐ a ❙
listAtS : {A : type}{n : ℕ} {a : A} {ls : list A} {h : ⊦ (Succ n) < length A (cons A a ls)} ⊦ listAt A (Succ n) (cons A a ls) h ≐ listAt A n ls (lemma_succ_cons A n a ls h) ❙
listAt : {A : type}{n : ℕ }{ls : list A} ⊦ lessthanN n (length A ls) ⟶ A ❘ # listAtA 2 3 4
// listAtB : {A : type } {a : A} {ls : list A}{h : ⊦ 0 < length A (cons A a ls)} ⊦ listAt A 0 (cons A a ls) h ≐ a ❙
// listAtS : {A : type}{n : ℕ} {a : A} {ls : list A} {h : ⊦ (Succ n) < length A (cons A a ls)} ⊦ listAt A (Succ n) (cons A a ls) h ≐ listAt A n ls (lemma_succ_cons A n a ls h) ❙
inList : {a : type} a ⟶ list a ⟶ bool ❘ # inListA 2 3❙
inListB : {a : type} {x : a} ⊦ inList a x (nil a) ≐ false ❙
inListS : {a : type} {x : a} {l : a }{lss : list a} ⊦ inList a x (cons a l lss) ≐ (x ≐ l ∧ inList a x lss) ❙
......@@ -7,9 +7,115 @@ import arith http://mathhub.info/MitM/smglom/arithmetics ❚
theory vectorFunctions : base:?Logic =
include http://mathhub.info/MitM/Foundation?Vectors ❙
include http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics ❙
include http://mathhub.info/MitM/smglom/algebra?Field ❙
include http://mathhub.info/MitM/smglom/algebra?Ring ❙
atVecc : {A : type}{n : ℕ} {i : ℕ} vector A n ⟶ ⊦ (lessthanN i n) ⟶ A ❙
// atVecB : {A : type} {n : ℕ} {a : A} {vs : vector A n}⊦ atVec A (Succ n) (0) (a ; vs) (lemma_zero_succ_lt n) ≐ a ❙
// atVecS : {A : type} {n : ℕ} {i : ℕ} {a : A} {vs : vector A n} {h : ⊦ (Succ i) < (Succ n)}⊦ atVec A (Succ n) (Succ i) (a ; vs) h ≐ atVec A n i vs (lemma_succ_succ_lt i n h ) ❙
replicate : {A : type}{n : ℕ} A ⟶ vector A n ❙
theory fieldVectorFunction : base:?Logic > f:ring ❘ =
addVecc : {n: ℕ}vector (f.universe) n ⟶ vector (f.universe) n ⟶ vector (f.universe) n ❙
subVecc : {n: ℕ}vector (f.universe) n ⟶ vector (f.universe) n ⟶ vector (f.universe) n ❙
// scalarMultiplication : {n : ℕ}(f.universe) ⟶ vector (f.universe) n ⟶ vector (f.universe) n ❙
// ones : {n :ℕ} vector (f.universe) n❙
// zeros : {n : ℕ} vector (f.universe) n ❙
// neg : {n : ℕ} vector (f.universe) n ⟶ vector (f.universe) n ❙
theory realVectorFunctions : base:?Logic =
include http://mathhub.info/MitM/smglom/Datatypes?vectorFunctions ❙
raddVecc : {n: ℕ} vector ℝ n ⟶ vector ℝ n ⟶ vector ℝ n ❙
rminusVecc : {n: ℕ} vector ℝ n ⟶ vector ℝ n ⟶ vector ℝ n ❙
rscalarMultiplication : {n : ℕ} ℝ ⟶ vector ℝ n ⟶ vector ℝ n ❙
rreplicate : {n : ℕ} ℝ ⟶ vector ℝ n ❙
rones : {n :ℕ} vector ℕ n❙
rzeros : {n : ℕ} vector ℝ n ❙
rneg : {n : ℕ} vector ℝ n ⟶ vector ℝ n ❙
theory realVectorTheorems : base:?Logic =
include http://mathhub.info/MitM/smglom/algebra?OperationProps ❙
include http://mathhub.info/MitM/smglom/Datatypes?realVectorFunctions ❙
include http://mathhub.info/MitM/smglom/algebra?Module ❙
include http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics ❙
lemma_real_vector_addition_assoc : {n } ⊦ prop_associative (raddVecc n) ❘# lemma_real_vector_addition_assoc 1❙
lemma_real_vector_leftUnital : {n} ⊦ prop_leftUnital (raddVecc n) (rzeros n) ❘ # lemma_real_vector_leftUnital 1❙
lemma_real_vector_rightUnital : {n} ⊦ prop_rightUnital (raddVecc n) (rzeros n) ❘# lemma_real_vector_rightUnital 1❙
lemma_real_vector_inverse : {n} ⊦ prop_inverse (raddVecc n) (rneg n) (rzeros n) ❘# lemma_real_vector_inverse 1 ❙
lemma_real_vector_comm : {n} ⊦ prop_commutative (raddVecc n) ❘# lemma_real_vector_comm 1 ❙
lemma_real_vector_dist1 : {n} ⊦ prop_dist1 (rscalarMultiplication n) (raddVecc n) ❘# lemma_real_vector_dist1 1❙
lemma_real_vector_dist2 : {n} ⊦ prop_dist2 (rscalarMultiplication n) (plus_real_lit) (raddVecc n) ❘# lemma_real_vector_dist2 1❙
lemma_assoc_scalars : {n} ⊦ prop_associative_scalars (rscalarMultiplication n) (times_real_lit) ❘# lemma_assoc_scalars 1 ❙
lemma_unit_scalars : {n} ⊦ prop_unit_scalars (rscalarMultiplication n) (1 : ℝ) ❘# lemma_unit_scalars 1 ❙
// theory generalizedVectorTheorems : base:?Logic =
include http://mathhub.info/MitM/smglom/algebra?Ring ❙
include http://mathhub.info/MitM/smglom/algebra?OperationProps ❙
include http://mathhub.info/MitM/smglom/Datatypes?realVectorFunctions ❙
include http://mathhub.info/MitM/smglom/algebra?Module ❙
include http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics ❙
lemma_real_vector_addition_assoc : {n }{r : ring} ⊦ prop_associative (raddVecc n) ❘# lemma_real_vector_addition_assoc 1❙
lemma_real_vector_leftUnital : {n} ⊦ prop_leftUnital (raddVecc n) (rzeros n) ❘ # lemma_real_vector_leftUnital 1❙
lemma_real_vector_rightUnital : {n} ⊦ prop_rightUnital (raddVecc n) (rzeros n) ❘# lemma_real_vector_rightUnital 1❙
lemma_real_vector_inverse : {n} ⊦ prop_inverse (raddVecc n) (rneg n) (rzeros n) ❘# lemma_real_vector_inverse 1 ❙
lemma_real_vector_comm : {n} ⊦ prop_commutative (raddVecc n) ❘# lemma_real_vector_comm 1 ❙
lemma_real_vector_dist1 : {n} ⊦ prop_dist1 (rscalarMultiplication n) (raddVecc n) ❘# lemma_real_vector_dist1 1❙
lemma_real_vector_dist2 : {n} ⊦ prop_dist2 (rscalarMultiplication n) (plus_real_lit) (raddVecc n) ❘# lemma_real_vector_dist2 1❙
lemma_assoc_scalars : {n} ⊦ prop_associative_scalars (rscalarMultiplication n) (times_real_lit) ❘# lemma_assoc_scalars 1 ❙
lemma_unit_scalars : {n} ⊦ prop_unit_scalars (rscalarMultiplication n) (1 : ℝ) ❘# lemma_unit_scalars 1 ❙
// theory vectorRing : base:?Logic =
include http://mathhub.info/MitM/smglom/Datatypes?realVectorTheorems ❙
include http://mathhub.info/MitM/smglom/algebra?Ring ❙
vectorNRing : ℕ ⟶ ring ⟶ ring ❘ = [n,r]
['
universe := vector (r.universe) n,
axiom_rightUnital :=
']❙
theory CoordinateSpace : base:?Logic =
include http://mathhub.info/MitM/smglom/Datatypes?realVectorTheorems ❙
include http://mathhub.info/MitM/smglom/algebra?Vectorspace ❙
include http://mathhub.info/MitM/smglom/algebra?RealField ❙
realCoordinateSpace : ℕ ⟶ vectorspace (realField) ❘ // = [n : ℕ] not working ! hence commented
['
universe := vector ℝ n,
op := raddVecc n ,
axiom_associative := lemma_real_vector_addition_assoc n,
unit := rzeros n,
axiom_leftUnital := lemma_real_vector_leftUnital n,
axiom_rightUnital := lemma_real_vector_rightUnital n,
inverse := rneg n,
axiom_inverse := lemma_real_vector_inverse n,
axiom_commutative := lemma_real_vector_comm n,
scalarmult := rscalarMultiplication n ,
axiom_unit_scalars := lemma_unit_scalars n,
axiom_associative_scalars := lemma_assoc_scalars n ,
axiom_dist2 := lemma_real_vector_dist2 n ,
axiom_dist1 := lemma_real_vector_dist1 n
']
atVec : {A : type}{n : ℕ} {i : ℕ} vector A n ⟶ ⊦ i < n ⟶ A ❙
atVecB : {A : type} {n : ℕ} {a : A} {vs : vector A n}⊦ atVec A (Succ n) (0) (a ; vs) (lemma_zero_succ_lt n) ≐ a ❙
atVecS : {A : type} {n : ℕ} {i : ℕ} {a : A} {vs : vector A n} {h : ⊦ (Succ i) < (Succ n)}⊦ atVec A (Succ n) (Succ i) (a ; vs) h ≐ atVec A n i vs (lemma_succ_succ_lt i n h ) ❙
namespace http://mathhub.info/MitM/smglom/algebra ❚
import top http://mathhub.info/MitM/interfaces❚
import base http://mathhub.info/MitM/Foundation ❚
import num http://mathhub.info/MitM/smglom/arithmetics ❚
import sets http://mathhub.info/MitM/smglom/typedsets ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
theory vectorFunctions : base:?Logic =
include base:?Vectors ❙
include arith:?NaturalArithmetics❙
vector_at : {A : type} {n : ℕ} {m : ℕ } vector A n ⟶ ⊦ m < n ⟶ A ❘# vector_at 3 4 5❙
vector_add : {n : ℕ} vector ℝ n ⟶ vector ℝ n ⟶ vector ℝ n❙
theory realcoordinatespace : base:Logic =
prop_implements_vectorspace ❙
\ No newline at end of file
......@@ -98,7 +98,7 @@ theory Field : base:?Logic =
axiom_commutative : ⊦ ∀[x : U]∀[y] (x ⋅ y) ≐ (y ⋅ x) ❙
field : kind ❘ = Mod `?Field/field_theory ❘ role abbreviation ❙
koerper = field ❙
// multiplicative_group : field ⟶ abeliangroup ❘ = [r] ['
universe := r.unitset,
......
......@@ -55,7 +55,11 @@ theory NaturalArithmetics : base:?Logic =
geq : ℕ ⟶ ℕ ⟶ bool ❘ = [n,m] m ≤ n ❘ # 1 ≥ 2 prec 105 ❙
lessthan : ℕ ⟶ ℕ ⟶ bool ❘ = [n,m] n ≤ m ∧ n ≠ m ❘ # 1 < 2 prec 105 ❙
morethan : ℕ ⟶ ℕ ⟶ bool ❘ = [n,m] n ≥ m ∧ n ≠ m ❘ # 1 > 2 prec 105 ❙
// Sven Wille : I introduced these aliases because mmt gets stuck all the time on ``abiguous'' notation/functions ❙
leqN : ℕ ⟶ ℕ ⟶ bool ❘ = leq ❙
lessthanN : ℕ ⟶ ℕ ⟶ bool ❘ = lessthan ❙
/T Others ❙
max : ℕ ⟶ ℕ ⟶ ℕ ❘ # max 1 2 ❙
min : ℕ ⟶ ℕ ⟶ ℕ ❘ # min 1 2 ❙
......
......@@ -60,6 +60,9 @@ theory RationalArithmetics : base:?Logic =
min : ℚ ⟶ ℚ ⟶ ℚ ❘ # min 1 2 ❙
axiom_ratLeqIsIntLeq : {x : ℤ, y : ℤ} ⊦ arithmetics?RationalArithmetics?leq x y ≐ arithmetics?IntegerArithmetics?leq x y ❙
leqQ : ℚ ⟶ ℚ ⟶ bool ❘ = arithmetics?RationalArithmetics?leq ❙
lessthanQ : ℚ ⟶ ℚ ⟶ bool ❘ = arithmetics?RationalArithmetics?lessthan ❙
/T Others ❙
absolute : ℚ ⟶ ℚ ❘ = [q] case q < 0 ⟹ -q . q ❘ # | 1 | prec 9 ❙
......
......@@ -57,7 +57,11 @@ theory RealArithmetics : base:?Logic =
max : ℝ ⟶ ℝ ⟶ ℝ ❘ # max 1 2 ❙
min : ℝ ⟶ ℝ ⟶ ℝ ❘ # min 1 2 ❙
axiom_realLeqIsRatLeq : {x : ℚ, y : ℚ} ⊦ arithmetics?RealArithmetics?leq x y ≐ arithmetics?RationalArithmetics?leq x y ❙
// Sven Wille : I introduced these aliases because mmt gets stuck all the time on ``abiguous'' notation/functions ❙
leqR : ℝ ⟶ ℝ ⟶ bool ❘= arithmetics?RealArithmetics?leq ❙
/T Subtypes ❙
NonNegativeRealNumbers : type ❘ # ℝ^+ ❘ = ⟨ x : ℝ | ⊦ x ≥ 0 ⟩❙
PositiveRealNumbers : type ❘ # ℝ+ ❘ = ⟨ x : ℝ | ⊦ x > 0 ⟩❙
......
......@@ -51,12 +51,33 @@ theory Intervals : base:?Logic =
type_ci_alt : ℝ ⟶ ℝ ⟶ type ❘= [l,h] {' left : ℝ := l , right : ℝ := h , leftPred : ℝ ⟶ ℝ ⟶ prop := ([x,y] x ≤ y) ,
rightPred : ℝ ⟶ ℝ ⟶ prop := ([x,y] x ≤ y) , predicate : ℝ ⟶ prop := [x] leftPred left x ∧ rightPred x right , tp : type := pred predicate'} ❙
is_ascending : type_ci ⟶ bool ❘= [ci] leqR (ci.left) (ci.right)❙
ascendingCi : type ❘ = ⟨ x :type_ci | ⊦ (x.left) ≤ (x.right) ⟩ ❙
ascendingCi : type ❘ = ⟨ x :type_ci | ⊦ (x.left) ≤ (x.right) ⟩ ❘# aci
isInCi : ℝ ⟶ type_ci ⟶ bool ❘ = [r , ci] ci.left ≤ r ∧ r ≤ ci.right ❙
theory closedIntervalMult : base:?Logic =
include http://mathhub.info/MitM/smglom/calculus?Intervals ❙
include http://mathhub.info/MitM/smglom/Datatypes?vectorFunctions ❙
include http://mathhub.info/MitM/smglom/Datatypes?ListFunctions ❙
include http://mathhub.info/MitM/smglom/typedsets?TypedSets ❙
vectorInIntervals : {n : ℕ} vector ℝ n ⟶ {lss : list type_ci} ⊦ (∀[x] inList type_ci x lss ⇒ is_ascending x) ⟶ ⊦ n ≐ lengthA lss ⟶ bool ❘
= [n, v, lss , h, h0 ] ∀[x] ∀[h1 : ⊦ lessthanN x n]
leqR ((listAtA x lss (substA n (lengthA lss) ([vv] ⊦ lessthanN x vv) h0 h1)).left) (atVecc ℝ n x v h1) ∧
leqR (atVecc ℝ n x v h1)((listAtA x lss (substA n (lengthA lss) ([vv] ⊦ lessthanN x vv) h0 h1)).right)❙
ci_mult : {lss : list type_ci} ⊦ (∀[x] inList type_ci x lss ⇒ is_ascending x) ⟶ set (vector ℝ (lengthA lss )) ❘
= [lss, h ] bsetst (vector ℝ (lengthA lss)) (fullset (vector ℝ lengthA lss)) ([x] vectorInIntervals (lengthA lss) x lss h (eq_refl (lengthA lss )) )❙
theory OneCuboid : base:?Logic =
include top:/arithmetics?RealArithmetics ❙
......
namespace http://mathhub.info/MitM/Geometry ❚
import fnd http://mathhub.info/MitM/Foundation ❚
import algebra http://mathhub.info/MitM/smglom/algebra ❚
theory AffineSpace : base:?Logic =
namespace http://mathhub.info/MitM/Geometry ❚
import algebra http://mathhub.info/MitM/smglom/algebra ❚
import base http://mathhub.info/MitM/Foundation ❚
theory Motion : base:?Logic =
include http://mathhub.info/MitM/smglom/calculus?MetricSpace ❙
is_isometry : {m1 : metricSpace}{m2 : metricSpace} (m1.universe ⟶ m2.universe) ⟶ prop ❘ = [m1, m2 , f] ∀ [x] ∀[y] ((m1.d) x y) ≐ ((m2.d) (f x) (f y)) ❙
is_motion = is_isometry ❙
......@@ -17,10 +17,30 @@ theory InhaltsProblem : base:?Logic =
include http://mathhub.info/MitM/smglom/arithmetics?ExtendedReals ❙
include http://mathhub.info/MitM/smglom/measures?SigmaAdditive ❙
inhaltsproblem = [n : ℕ ] ∃ [m : set (vector ℝ n) ⟶ ⟨ x : ℝ | ⊦ 0 ≤ x ∧ x ≤ ∞ ⟩] (prop_sigmaAdditive_alt (vector ℝ n) m)
inhaltsproblemProp = [n : ℕ ] [m : set (vector ℝ n) ⟶ ⟨ x : ℝ | ⊦ 0 ≤ x ∧ x ≤ ∞ ⟩] (prop_sigmaAdditive_alt (vector ℝ n) m) ❙
inhaltsproblem = [n : ℕ ] ∃ [m : set (vector ℝ n) ⟶ ⟨ x : ℝ | ⊦ 0 ≤ x ∧ x ≤ ∞ ⟩] inhaltsproblemProp n m
theory SatzVonHausdorff : base:?Logic =
include ?InhaltsProblem ❙
include http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics ❙
satz_Hausdorff : ⊦ ∀ [p] leqN 3 p ⇒ ¬ inhaltsproblem p ❙
theory SatzBanach : base:?Logic =
include ?InhaltsProblem ❙
include http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics ❙
satz_Banach : ⊦ ∀ [n] n ≐ 1 ∨ n ≐ 2 ⇒ inhaltsproblem n ∧ ∃[a] ∃[b] inhaltsproblemProp n a ∧ inhaltsproblemProp n b ∧ a ≠ b ❙
theory SatzBanachTarski : base:?Logic =
include http://mathhub.info/MitM/Geometry?Motion ❙
include http://mathhub.info/MitM/smglom/calculus?RealMetricSpace ❙
\ No newline at end of file
......@@ -27,19 +27,38 @@ theory SigmaOperatorTheorems : base:?Logic =
theory BorelExample : base:?Logic =
include base:?Vectors ❙
theory BorelSet : base:?Logic =
include http://mathhub.info/MitM/smglom/Datatypes?vectorFunctions ❙
include arith:?RealProperties ❙
include http://mathhub.info/MitM/smglom/calculus?Intervals
include http://mathhub.info/MitM/smglom/calculus?closedIntervalMult
include http://mathhub.info/MitM/smglom/Datatypes?ListFunctions ❙
include http://mathhub.info/MitM/smglom/measures?SigmaOperator ❙
n : ℕ ❙
// vspace = finite_vectorspace realfield n ❙ // this line crashes intellij ❙
Ω = vector ℝ n
Ω : set (vector ℝ n) ❘ = fullset (vector ℝ n)
vectorInIntervals : vector ℝ n ⟶ {lss : list ascendingCi} ⊦ (n ≐ length ascendingCi lss) ⟶ bool ❘ = [v , lss , h ] ∀ [x : ℕ ] ∀ [h : ⊦ x < n] listAt ascendingCi x (subst ) ≤ atVec ℝ n x v h ❙
ndimensinalQuarderWithRatEndpoints :
{lss : list type_ci} ⊦ (∀ [x] inList type_ci x lss ⇒ is_ascending x) ⟶ ⊦ (∀ [x] inList type_ci x lss ⇒ is_rat (x.left) ∧ is_rat(x.right)) ⟶ ⊦ n ≐ lengthA lss ⟶ set (vector ℝ n)
❘ = [lss , h , h0 , h1] substA (lengthA lss) n ([t : ℕ] set (vector ℝ t)) (eq_symA h1) (ci_mult lss h)❙
// ndimQuardRat = [ls : list ]⟨ vector ℝ n | ⟩ ❙
allNdimensionalQuaderWithRatEndpoints : set (set (vector ℝ n)) ❘ = [s : set (vector ℝ n)] ∃ [lss] ∃ [h] ∃ [h0] ∃ [h1] ndimensinalQuarderWithRatEndpoints lss h h0 h1 ≐ s ❙
lemma_borelSigma_helper : ⊦ allNdimensionalQuaderWithRatEndpoints ⊑ ℘ Ω ❘# lemma_borelSigma_helper ❙
borelSigma : set (set (vector ℝ n)) ❘ = σ Ω allNdimensionalQuaderWithRatEndpoints lemma_borelSigma_helper ❙
// this is a simplified version on ℝ. one can define this for any topological space ❙
isBorelSet : set (vector ℝ n) ⟶ bool ❘ = [s] s ∈ borelSigma❙
theory ExamplesOfBorelSets : base:?Logic =
include ?BorelSet ❙
include http://mathhub.info/MitM/smglom/topology?OpenSetTopology ❙
include http://mathhub.info/MitM/smglom/topology?RealTopology ❙
example_openSetIsBorel : ⊦ isOpen (realTopologicalSpace) set ()❙
namespace http://mathhub.info/MitM/smglom/typedsets ❚
import base http://mathhub.info/MitM/Foundation ❚
import natt http://mathhub.info/MitM/smglom/arithmetics ❚
// there is also a less general formalization of open sets with regars to topologies ❚
theory OpenSet : base:?Logic =
include http://mathhub.info/MitM/smglom/typedsets?TypedSets ❙
is_openset : {a} set a ⟶ bool ❘= [a,s] ❙
namespace http://mathhub.info/MitM/smglom/typedsets ❚
import base http://mathhub.info/MitM/Foundation ❚
import natt http://mathhub.info/MitM/smglom/arithmetics ❚
theory BoundedSet : base:?InductiveTypes =
is_boundedSet : ⊦ {a : type} set a ⟶ bool ❙
\ No newline at end of file
......@@ -10,4 +10,10 @@ theory RealTopology : base:?Logic =
realTopology = metricAsTopology realmetricspace ❘ : topology ℝ❙
realTopologicalSpace = [' universe := ℝ , topology := realTopology '] ❘: topologicalSpace ❙
theory RealVectorTopology : base:?Logic =
include http://mathhub.info/MitM/smglom/Datatypes?vectorFunctions ❙
\ No newline at end of file
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