Commit 3b26b595 authored by SuperDuckDuck's avatar SuperDuckDuck

started lebesgue measure

parent e0a24e7f
namespace http://mathhub.info/MitM/smglom/collections ❚
import base http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/smglom/typedsets ❚
theory Properties : base:?Logic =
include typedsets?SetCollection ❙
......@@ -33,3 +34,9 @@ theory Partition : base:?Logic =
partition = [X : type] Mod `?Partition/partition_theory , X ❙
// theory TaggedPartition : base:?Logic =
include ?Partition ❙
include ts:?TaggedCollectoin ❙
\ No newline at end of file
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❚
import calc http://mathhub.info/MitM/smglom/calculus ❚
theory RiemannIntegrable : base:?Logic =
\ No newline at end of file
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❚
import calc http://mathhub.info/MitM/smglom/calculus ❚
theory OuterMeasure : base:?Logic =
include ts:?SetCollection ❙
theory outerMeasure_theory : base:?Logic =
measure ❙
emptyIsZero
\ No newline at end of file
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❚
import calc http://mathhub.info/MitM/smglom/calculus ❚
theory RiemannIntegrable : base:?Logic =
include calc:?Intervals ❙
include ?AlmostEverywhere ❙
prop_lebesgueCriterion ❙
\ No newline at end of file
namespace http://mathhub.info/MitM/smglom/typedsets ❚
import base http://mathhub.info/MitM/Foundation ❚
import sig http://gl.mathhub.info/MMT/LFX/Sigma ❚
theory TypedSets : base:?Logic =
include base:?Lists ❙
......@@ -157,8 +158,10 @@ theory SetCollection : base:?Logic =
fullSetInType : {T, S : setColl T, fullincoll : ⊦ (fullset T) ∈ (S.coll) } S.colltype ❘ # fullt %I1 %I2 %I3 ❙
// theory TaggedSetCollection : base:?Logic =
// include ?SetCollection ❙
// taggedCollection : type ⟶ type ❘= [G] set (g × set G) ❙
theory TaggedSetCollection : base:?Logic =
include ?SetCollection ❙
include sig:?LFSigma ❙
taggedCollection : type ⟶ type ❘= [G] set (G × set G) ❙
// ❚
\ No newline at end of file
\ 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