Commit f3f5797d authored by Sven Wille's avatar Sven Wille

measure theory

parent e8e36fb7
<?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:2689.90.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 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#540.15.0:555.15.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#1128.40.0:1143.40.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#1654.63.0:1674.63.20"/></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: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
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/measures/measures.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#0.0.0:5570.123.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/measures"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import ts http://mathhub.info/MitM/smglom/typedsets"/><instruction text="import lfx http://gl.mathhub.info/MMT/LFX/Sigma"/><instruction text="import exr http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import seq http://cds.omdoc.org/urtheories"/><instruction text="import desc http://mathhub.info/MitM/smglom/DescriptionOperators"/><mref name="[http://mathhub.info/MitM/smglom/measures?Additive]" target="http://mathhub.info/MitM/smglom/measures?Additive"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#377.9.0:391.9.14"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?SigmaAdditive]" target="http://mathhub.info/MitM/smglom/measures?SigmaAdditive"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#722.18.0:741.18.19"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?Measure]" target="http://mathhub.info/MitM/smglom/measures?Measure"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#1224.29.0:1237.29.13"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?PowerSigmaAlgebra]" target="http://mathhub.info/MitM/smglom/measures?PowerSigmaAlgebra"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#2344.56.0:2367.56.23"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?CountingMeasure]" target="http://mathhub.info/MitM/smglom/measures?CountingMeasure"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#3284.76.0:3305.76.21"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?NullSets]" target="http://mathhub.info/MitM/smglom/measures?NullSets"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#4500.97.0:4514.97.14"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?AlmostEverywhere]" target="http://mathhub.info/MitM/smglom/measures?AlmostEverywhere"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#4899.105.0:4921.105.22"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?BorelMeasurableSpace]" target="http://mathhub.info/MitM/smglom/measures?BorelMeasurableSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#5129.113.0:5155.113.26"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?RealBorelMeasurableSpace]" target="http://mathhub.info/MitM/smglom/measures?RealBorelMeasurableSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#5368.119.1:5398.119.31"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/MitM/smglom/measures/measures.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#0.0.0:5786.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/measures"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import ts http://mathhub.info/MitM/smglom/typedsets"/><instruction text="import lfx http://gl.mathhub.info/MMT/LFX/Sigma"/><instruction text="import exr http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import seq http://cds.omdoc.org/urtheories"/><instruction text="import desc http://mathhub.info/MitM/smglom/DescriptionOperators"/><mref name="[http://mathhub.info/MitM/smglom/measures?Additive]" target="http://mathhub.info/MitM/smglom/measures?Additive"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#377.9.0:391.9.14"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?SigmaAdditive]" target="http://mathhub.info/MitM/smglom/measures?SigmaAdditive"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#722.18.0:741.18.19"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?Measure]" target="http://mathhub.info/MitM/smglom/measures?Measure"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#1440.31.0:1453.31.13"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?PowerSigmaAlgebra]" target="http://mathhub.info/MitM/smglom/measures?PowerSigmaAlgebra"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#2560.58.0:2583.58.23"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?CountingMeasure]" target="http://mathhub.info/MitM/smglom/measures?CountingMeasure"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#3500.78.0:3521.78.21"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?NullSets]" target="http://mathhub.info/MitM/smglom/measures?NullSets"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#4716.99.0:4730.99.14"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?AlmostEverywhere]" target="http://mathhub.info/MitM/smglom/measures?AlmostEverywhere"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#5115.107.0:5137.107.22"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?BorelMeasurableSpace]" target="http://mathhub.info/MitM/smglom/measures?BorelMeasurableSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#5345.115.0:5371.115.26"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/measures?RealBorelMeasurableSpace]" target="http://mathhub.info/MitM/smglom/measures?RealBorelMeasurableSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/measures/measures.mmt#5584.121.1:5614.121.31"/></metadata></mref></omdoc>
\ No newline at end of file
......@@ -2,3 +2,5 @@ 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?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
Declares http://mathhub.info/MitM/smglom/calculus/domains.omdoc http://mathhub.info/MitM/smglom/calculus?IntervalCartesianProduct
......@@ -13,6 +13,7 @@ Includes http://mathhub.info/MitM/smglom/calculus?GeneralDomains http://cds.omdo
Includes http://mathhub.info/MitM/smglom/calculus?GeneralDomains http://cds.omdoc.org/urtheories?NatRels
Includes http://mathhub.info/MitM/smglom/calculus?GeneralDomains http://mathhub.info/MitM/Foundation?NatLiterals
Includes http://mathhub.info/MitM/smglom/calculus?GeneralDomains http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers
Includes http://mathhub.info/MitM/smglom/calculus?GeneralDomains http://mathhub.info/MitM/Foundation?NaturalDeduction
Includes http://mathhub.info/MitM/smglom/calculus?GeneralDomains http://mathhub.info/MitM/smglom/algebra?OperationProps
Includes http://mathhub.info/MitM/smglom/calculus?GeneralDomains http://gl.mathhub.info/MMT/LFX/Datatypes?ListSymbols
Includes http://mathhub.info/MitM/smglom/calculus?GeneralDomains http://gl.mathhub.info/MMT/LFX/Datatypes?ListRules
......@@ -26,7 +27,6 @@ Includes http://mathhub.info/MitM/smglom/calculus?GeneralDomains http://mathhub.
Includes http://mathhub.info/MitM/smglom/calculus?GeneralDomains http://mathhub.info/MitM/smglom/algebra?Monoid
Includes http://mathhub.info/MitM/smglom/calculus?GeneralDomains http://mathhub.info/MitM/Foundation?OptionType
Includes http://mathhub.info/MitM/smglom/calculus?GeneralDomains http://mathhub.info/MitM/Foundation?DescriptionOperator
Includes http://mathhub.info/MitM/smglom/calculus?GeneralDomains http://mathhub.info/MitM/Foundation?NaturalDeduction
Includes http://mathhub.info/MitM/smglom/calculus?GeneralDomains http://mathhub.info/MitM/smglom/algebra?Loop
Includes http://mathhub.info/MitM/smglom/calculus?GeneralDomains http://mathhub.info/MitM/Foundation?IntLiterals
Includes http://mathhub.info/MitM/smglom/calculus?GeneralDomains http://mathhub.info/MitM/Foundation?Strings
......
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
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
......@@ -25,6 +26,7 @@ Includes http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/
Includes http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/smglom/arithmetics?IntegerArithmetics
Includes http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/smglom/arithmetics?RationalArithmetics
Includes http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics
Includes http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/Foundation?NaturalDeduction
Includes http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/smglom/algebra?OperationProps
Includes http://mathhub.info/MitM/smglom/calculus?Intervals http://gl.mathhub.info/MMT/LFX/Datatypes?ListSymbols
Includes http://mathhub.info/MitM/smglom/calculus?Intervals http://gl.mathhub.info/MMT/LFX/Datatypes?ListRules
......@@ -36,7 +38,6 @@ Includes http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/
Includes http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/smglom/algebra?SemiGroup
Includes http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/smglom/algebra?Unital
Includes http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/smglom/algebra?Monoid
Includes http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/Foundation?NaturalDeduction
Includes http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/smglom/algebra?Loop
Includes http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/Foundation?Strings
Includes http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/Foundation?InformalProofs
......@@ -94,3 +95,10 @@ DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?closedInterval?defi
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?closedInterval?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?closedInterval?definition http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?leq?type
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?closedInterval?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/MitM/smglom/calculus?Intervals http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci
constant http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci?definition http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?predAsSub?type
DependsOn http://mathhub.info/MitM/smglom/calculus?Intervals?type_ci?definition http://mathhub.info/MitM/Foundation?Logic?prop?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
dataconstructor http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive
dataconstructor http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt
theory http://mathhub.info/MitM/smglom/measures?SigmaAdditive
HasMeta http://mathhub.info/MitM/smglom/measures?SigmaAdditive http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/MitM/smglom/measures?SigmaAdditive http://gl.mathhub.info/MMT/LFX/Subtyping?JudgmentSymbol
......@@ -69,3 +70,22 @@ DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAddit
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive?type http://mathhub.info/MitM/smglom/typedsets?TypedSets?set?definition
Declares http://mathhub.info/MitM/smglom/measures?SigmaAdditive http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt
constant http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt?type http://mathhub.info/MitM/Foundation?Logic?prop?type
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt?type http://mathhub.info/MitM/smglom/typedsets?TypedSets?set?type
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt?type http://mathhub.info/MitM/smglom/typedsets?TypedSets?set?definition
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt?definition http://mathhub.info/MitM/smglom/arithmetics?RealArithmetics?addition?type
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt?definition http://mathhub.info/MitM/Foundation?Logic?implies?type
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt?definition http://mathhub.info/MitM/smglom/typedsets?SetRelations?subset?type
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt?definition http://mathhub.info/MitM/Foundation?Logic?forall?type
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt?definition http://mathhub.info/MitM/smglom/typedsets?Union?union?type
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt?definition http://mathhub.info/MitM/smglom/typedsets?SetRelations?disjoint?type
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt?definition http://mathhub.info/MitM/smglom/typedsets?TypedSets?fullset?type
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
DependsOn http://mathhub.info/MitM/smglom/measures?SigmaAdditive?prop_sigmaAdditive_alt?definition http://mathhub.info/MitM/smglom/typedsets?TypedSets?set?definition
......@@ -50,5 +50,5 @@ theory FinSeqFunctions : base:?InductiveTypes =
theory FinSeqProd : base:?Logic =
// finSeqIntervalProd :
finSeqCIntervalProd = [n : INat] [fs : finSeq n type_ci] vector () ℝ
......@@ -48,6 +48,8 @@ theory Intervals : base:?Logic =
type_ci : type ❘= {' left : ℝ , right : ℝ , 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'} ❙
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'} ❙
......
......@@ -25,6 +25,8 @@ theory SigmaAdditive : base:?Logic =
prop_sigmaAdditive : {A : type}{F : collection A} (setastype F ⟶ ℝ) ⟶ bool ❘ # prop_sigmaAdditive 2 3 ❘
// = [A,F,f] ∀[S : sequence (setastype (F.coll))] pairwiseDisjoint (im S (fullset ℕ)) ⇒ f (elem (F.coll) (UNION (im S (fullset ℕ)))) ≐ SUM ([x : ℕ] f (S x)) ❙
// DM: conversion between sets and types needed to work properly ❙
prop_sigmaAdditive_alt : {O : type} (set O ⟶ ℝ) ⟶ bool ❘ = [O : type][meas : set O ⟶ ℝ] ∀ [A] ∀[B] A ⊑ fullset O ⇒ B ⊑ fullset O ⇒ disjoint A B ⇒ meas (A ∪ B) ≐ meas A + meas B ❘# prop_sigmaAdditive_alt 1 2❙
theory Measure : base:?Logic =
......
namespace http://mathhub.info/MitM/smglom/measures ❚
import base http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/smglom/typedsets ❚
import lfx http://gl.mathhub.info/MMT/LFX/Sigma ❚
import exr http://mathhub.info/MitM/smglom/arithmetics ❚
import seq http://cds.omdoc.org/urtheories ❚
import desc http://mathhub.info/MitM/smglom/DescriptionOperators❚
theory InhaltsProblem : base:?Logic =
include base:?Vectors ❙
include http://mathhub.info/MitM/smglom/typedsets?AllSets ❙
include http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics ❙
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) ❙
theory SatzVonHausdorff : base:?Logic =
\ 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