(* Title: HOL/Induct/Sigma_Algebra.thy Author: Markus Wenzel, TU Muenchen
*)
section \<open>Sigma algebras\<close>
theory Sigma_Algebra imports Main begin
text\<open>
This is just a tiny example demonstrating the use of inductive
definitions in classical mathematics. We define the least \<open>\<sigma>\<close>-algebra over a given set of sets. \<close>
inductive_set\<sigma>_algebra :: "'a set set \<Rightarrow> '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\<open>
The following basic facts are consequences of the closure properties
of any \<open>\<sigma>\<close>-algebra, merely using the introduction rules, but
no induction nor cases. \<close>
theorem sigma_algebra_empty: "{} \ \_algebra A" proof - have"UNIV \ \_algebra A" by (rule \_algebra.UNIV) thenhave"-UNIV \ \_algebra A" by (rule \_algebra.complement) alsohave"-UNIV = {}"by simp finallyshow ?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" thenhave"\i::nat. -(a i) \ \_algebra A" by (rule \_algebra.complement) thenhave"(\i. -(a i)) \ \_algebra A" by (rule \_algebra.Union) thenhave"-(\i. -(a i)) \ \_algebra A" by (rule \_algebra.complement) alsohave"-(\i. -(a i)) = (\i. a i)" by simp finallyshow ?thesis . qed
end
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
