\import Algebra.Pointed
\import Arith.Real
\import Order.Lattice
\import Order.PartialOrder
\import Set
\import Set.Filter
\import Set.Subset

{-
\class MeasurableSpace \extends BaseSet
  | isMeasurable : Set E -> \Prop
  | isFull : SetFilter E
  --  | measurable-meet {U V : Set E} -> isMeasurable U -> isMeasurable V -> isMeasurable (U ∧ V)
  --  (or diff): | measurable-Compl {U : Set E} -> isMeasurable U -> isMeasurable (Compl U)
  --  | measurable-full {U : Set E} -> isMeasurable U -> isFull (Comp U ∨ U)
  --  | full-measurable {U : Set E} -> isFull U -> isMeasurable U

\class MeasureSpace \extends MeasurableSpace
  | measure (U : Set E) : isMeasurable U -> Real
-}

\class MeasurableSpace \extends BaseSet
  | isMeasurable : Set E -> \Prop
  | measurable-empty : isMeasurable bottom

\class MeasureSpace \extends MeasurableSpace
  | measure {U : Set E} : isMeasurable U -> Real
  | measure-empty : measure measurable-empty = 
  | measure-<= {U V : Set E} {Um : isMeasurable U} {Vm : isMeasurable V} : U ⊆ V -> measure Um <= measure Vm

-- TODO: Какая связь между мерами в нашем смысле, мерами как у Бишопа в 1.7, и мерами у него же в более привычном смысле?