Commit 6df94c50 authored by Sven Wille's avatar Sven Wille

sigma nonesense

parent 18b26ad2
......@@ -121,6 +121,6 @@ theory RealVectorspace : base:?Logic =
realVec1 : realVec ❘ = asVectorspace realField ❘ # ℝ1 ❙
realVec2 : realVec ❘ // = productspace realField ℝ1 ℝ1 ❘ # ℝ2 ❙
realVec3 : realVec ❘ // = productspace realField ℝ1 ℝ2 ❘ # ℝ3 ❙ // takes forever ❙
finite_real_vectorspace : pos_lit ⟶ realVec ❙ // uncommented and changed by sw : why was this one commented out
// finite_real_vectorspace : pos_lit ⟶ realVec
......@@ -2,9 +2,7 @@ namespace http://mathhub.info/MitM/smglom/measures ❚
import base http://mathhub.info/MitM/Foundation ❚
import ts http://mathhub.info/MitM/smglom/typedsets ❚
import top http://mathhub.info/MitM/smglom/topology ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
import alg http://mathhub.info/MitM/smglom/algebra ❚
theory SigmaOperator : base:?Logic =
......@@ -18,21 +16,19 @@ theory SigmaOperator : base:?Logic =
theory SigmaOperatorTheorems : base:?Logic =
include ?SigmaOperator ❙
/T ofthen O is enforced to be nonempty. An empty set of events usually results in trivialities (f.ex. the trivial measure)❙
theorem_sigmaOperator_1 : {A : type} {O : set A} {M : set (set A)} {h : ⊦ M ⊑ ℘ O} ⊦ M ⊑ σ O M h ❙
theorem_sigmaOperator_2 : {A : type} {O : set A} {O0 : set A} {M : set (set A)} {N : set (set A)} {h : ⊦ M ⊑ ℘ O} {h0 : ⊦ N ⊑ ℘ O0} ⊦ M ⊑ N ⟶ ⊦ σ O M h ⊑ σ O0 N h0❙
theorem_sigmaOperator_3 : {A : type} {O : set A} {M : set (set A)} {h : ⊦ M ⊑ ℘ O} ⊦ σ O M h ⊑ ℘ O ❙
theorem_sigmaOperator_4 : {A : type} {O : set A} {M : set (set A)} {h : ⊦ M ⊑ ℘ O} ⊦ σ O (σ O M h) (theorem_sigmaOperator_3 A O M h) ≐ σ O M h
theorem_sigmaOperator_5 ❙
theorem_sigmaOperator_3 : {A : type} {O : set A} {M : set (set A)} {h : ⊦ M ⊑ ℘ O} ⊦ σ O M h ⊑ ℘ O ❘ # theorem_sigmaOperator_3 1 2 3 4
theorem_sigmaOperator_4 : {A : type} {O : set A} {M : set (set A)} {h : ⊦ M ⊑ ℘ O} ⊦ σ O (σ O M h) (theorem_sigmaOperator_3 A O M h) ≐ σ O M h❙
theorem_sigmaOperator_5 : {A : type} {O : set A} {M : set (set A)} {h : ⊦ M ⊑ ℘ O} ⊦ ∀ [y] isSigmaAlgebra y ⇒ M ⊑ y ⇒ σ O M h ⊑ y
theory BorelExample : base:?Logic =
theory bla : base:?Logic =
include alg:?Productspace ❙
n : nat ❙
Ω = ❙
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