Commit 3b6f76e6 authored by Sven Wille's avatar Sven Wille

finally doing more probability

parent 5dc6c4ff
<?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:5764.167.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?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#108.4.0:128.4.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#409.15.0:433.15.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#3825.92.0:3855.92.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#4134.108.0:4149.108.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#4743.137.0:4756.137.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#5236.149.0:5256.149.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#5508.161.0:5523.161.15"/></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: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
<?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:4112.93.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></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: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
<?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:4272.125.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#1840.54.0:1855.54.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#2366.77.0:2386.77.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#3404.106.0:3427.106.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#3710.114.0:3740.114.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: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
......@@ -6,3 +6,4 @@ Declares http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc http://mathh
Declares http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc http://mathhub.info/MitM/smglom/arithmetics?Between
Declares http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc http://mathhub.info/MitM/smglom/arithmetics?NatConversions
Declares http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc http://mathhub.info/MitM/smglom/arithmetics?INatProps
Declares http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc http://mathhub.info/MitM/smglom/arithmetics?CompDec
......@@ -2,3 +2,4 @@ document http://mathhub.info/MitM/smglom/arithmetics/reals.omdoc
Declares http://mathhub.info/MitM/smglom/arithmetics/reals.omdoc http://mathhub.info/MitM/smglom/arithmetics?RealNumbers
Declares http://mathhub.info/MitM/smglom/arithmetics/reals.omdoc http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics
Declares http://mathhub.info/MitM/smglom/arithmetics/reals.omdoc http://mathhub.info/MitM/smglom/arithmetics?ExtendedReals
Declares http://mathhub.info/MitM/smglom/arithmetics/reals.omdoc http://mathhub.info/MitM/smglom/arithmetics?RealProperties
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
datatypeconstructor http://mathhub.info/MitM/smglom/calculus?Intervals?ascendingCi
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
......@@ -102,3 +104,18 @@ DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci?definition
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci?definition http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?leq?type
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci?definition http://mathhub.info/MitM/Foundation?Logic?and?type
Declares http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci_alt
constant http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci_alt
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci_alt?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci_alt?definition http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?predAsSub?type
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?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
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?ascendingCi?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?ascendingCi?definition http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?leq?type
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
namespace http://mathhub.info/MitM/smglom ❚
import base http://mathhub.info/MitM/Foundation ❚
import lfxdat http://gl.mathhub.info/MMT/LFX/Datatypes❚
theory scratch : base:?Logic =
include http://gl.mathhub.info/MMT/LFX/Datatypes?LFLists ❙
include http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics ❙
subst : {A : type}{a : A} {b : A} {P : A ⟶ type} ⊦ a ≐ b ⟶ P a ⟶ P b ❙
x : ℕ ❙
n : ℕ ❙
y : ℕ ❙
hh : ⊦ x < n ❙
hhh : ⊦ x ≐ y ❙
test : ⊦ y < n ❘= subst ℕ x y ([v] ⊦ v < n) hhh hh ❙
namespace http://mathhub.info/MitM/smglom/Datatypes ❚
import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
theory List : base:?Logic =
list : type ⟶ type ❙
cons : {A : type} A ⟶ list A ⟶ list A ❙
nil : {A : type } list A ❙
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 ⟶ ℕ ❙
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) ❙
namespace http://mathhub.info/MitM/smglom/Datatypes ❚
import base http://mathhub.info/MitM/Foundation ❚
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 ❙
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 ) ❙
......@@ -80,6 +80,8 @@ theory NaturalArithmetics : base:?Logic =
lemma_zero_succ_lt : {n : ℕ} ⊦ 0 < `?NaturalNumbers?succ n ❘# lemma_zero_succ_lt 1 ❙
lemma_lt_succ_succ : {a : ℕ} {b : ℕ} ⊦ a < b ⟶ ⊦ `?NaturalNumbers?succ a < `?NaturalNumbers?succ b ❘# lemma_lt_succ_succ 1 2 3 ❙
lemma_le_succ_succ : {a : ℕ} {b : ℕ} ⊦ a ≤ b ⟶ ⊦ `?NaturalNumbers?succ a ≤ `?NaturalNumbers?succ b ❘ # lemma_le_succ_succ 1 2 3 ❙
lemma_succ_succ_lt : {a : ℕ} {b : ℕ} ⊦ (Succ a) < (Succ b) ⟶ ⊦ a < b ❘ # lemma_succ_succ_lt 1 2 3❙
lemma_succ_succ_le : {a : ℕ} {b : ℕ} ⊦ (Succ a) ≤ (Succ b) ⟶ ⊦ a ≤ b ❘ # lemma_succ_succ_le 1 2 3❙
// added by sw ❙
......
......@@ -92,3 +92,10 @@ theory ExtendedReals : base:?Logic =
// leq : ℝ∞ ⟶ ℝ∞ ⟶ bool ❘ # 1 ≤ 2 prec 101 ❙
// TODO neginfty : ℝ∞ ❘ = - ∞ ❘ # -∞ ❙
theory RealProperties : base:?Logic =
include ?ExtendedReals ❙
is_rat : ℝ ⟶ bool ❘ = [r] ∃ [n] ∃ [d] r ≐ fraction n d ❙
\ No newline at end of file
......@@ -52,6 +52,9 @@ theory Intervals : base:?Logic =
rightPred : ℝ ⟶ ℝ ⟶ prop := ([x,y] x ≤ y) , predicate : ℝ ⟶ prop := [x] leftPred left x ∧ rightPred x right , tp : type := pred predicate'} ❙
ascendingCi : type ❘ = ⟨ x :type_ci | ⊦ (x.left) ≤ (x.right) ⟩ ❙
theory OneCuboid : base:?Logic =
......
......@@ -29,10 +29,17 @@ theory SigmaOperatorTheorems : base:?Logic =
theory BorelExample : base:?Logic =
include base:?Vectors ❙
include arith:?NaturalNumbers ❙
include arith:?RealProperties ❙
include http://mathhub.info/MitM/smglom/calculus?Intervals ❙
include http://mathhub.info/MitM/smglom/Datatypes?ListFunctions ❙
n : ℕ ❙
// vspace = finite_vectorspace realfield n ❙ // this line crashes intellij ❙
Ω = vector ℝ n❙
ndimQuardRat = ⟨ 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 ❙
// ndimQuardRat = [ls : list ]⟨ vector ℝ n | ⟩ ❙
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