Theory Sigma_Algebra

(*  Title:      HOL/Induct/Sigma_Algebra.thy
    Author:     Markus Wenzel, TU Muenchen
*)

section ‹Sigma algebras›

theory Sigma_Algebra
imports Main
begin

text ‹
  This is just a tiny example demonstrating the use of inductive
  definitions in classical mathematics.  We define the least σ›-algebra over a given set of sets.
›

inductive_set σ_algebra :: "'a set set  'a set set" for A :: "'a set set"
where
  basic: "a  σ_algebra A" if "a  A" for a
| UNIV: "UNIV  σ_algebra A"
| complement: "- a  σ_algebra A" if "a  σ_algebra A" for a
| Union: "(i. a i)  σ_algebra A" if "i::nat. a i  σ_algebra A" for a

text ‹
  The following basic facts are consequences of the closure properties
  of any σ›-algebra, merely using the introduction rules, but
  no induction nor cases.
›

theorem sigma_algebra_empty: "{}  σ_algebra A"
proof -
  have "UNIV  σ_algebra A" by (rule σ_algebra.UNIV)
  then have "-UNIV  σ_algebra A" by (rule σ_algebra.complement)
  also have "-UNIV = {}" by simp
  finally show ?thesis .
qed

theorem sigma_algebra_Inter:
  "(i::nat. a i  σ_algebra A)  (i. a i)  σ_algebra A"
proof -
  assume "i::nat. a i  σ_algebra A"
  then have "i::nat. -(a i)  σ_algebra A" by (rule σ_algebra.complement)
  then have "(i. -(a i))  σ_algebra A" by (rule σ_algebra.Union)
  then have "-(i. -(a i))  σ_algebra A" by (rule σ_algebra.complement)
  also have "-(i. -(a i)) = (i. a i)" by simp
  finally show ?thesis .
qed

end