matita/contribs/dama/dama/classical_pointwise/sigma_algebra.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 include "classical_pointwise/topology.ma".
  18
  19 record is_sigma_algebra (X:Type) (A: set X) (M: set (set X)) : Prop ≝
  20  { siga_subset: ∀B.B ∈ M → B ⊆ A;
  21    siga_full: A ∈ M;
  22    siga_compl: ∀B.B ∈ M → B \sup c ∈ M;
  23    siga_enumerable_union:
  24     ∀B:seq (set X).(∀i.(B \sub i) ∈ M) → (∪ \sub i B \sub i) ∈ M
  25  }.
  26
  27 record sigma_algebra : Type ≝
  28  { siga_carrier:> Type;
  29    siga_domain:> set siga_carrier;
  30    M: set (set siga_carrier);
  31    siga_is_sigma_algebra:> is_sigma_algebra ? siga_domain M
  32  }.
  33
  34 (*definition is_measurable_map ≝
  35  λX:sigma_algebra.λY:topological_space.λf:X → Y.
  36   ∀V. V ∈ O Y → f \sup -1 V ∈ M X.*)
  37 definition is_measurable_map ≝
  38  λX:sigma_algebra.λY:topological_space.λf:X → Y.
  39   ∀V. V ∈ O Y → inverse_image ? ? f V ∈ M X.
  40