src/HOL/Library/Indicator_Function.thy
changeset 54408 67dec4ccaabd
parent 45425 7fee7d7abf2f
child 56993 e5366291d6aa
     1.1 --- a/src/HOL/Library/Indicator_Function.thy	Tue Nov 12 14:24:34 2013 +0100
     1.2 +++ b/src/HOL/Library/Indicator_Function.thy	Tue Nov 12 19:28:50 2013 +0100
     1.3 @@ -22,6 +22,12 @@
     1.4  lemma indicator_abs_le_1: "\<bar>indicator S x\<bar> \<le> (1::'a::linordered_idom)"
     1.5    unfolding indicator_def by auto
     1.6  
     1.7 +lemma indicator_eq_0_iff: "indicator A x = (0::_::zero_neq_one) \<longleftrightarrow> x \<notin> A"
     1.8 +  by (auto simp: indicator_def)
     1.9 +
    1.10 +lemma indicator_eq_1_iff: "indicator A x = (1::_::zero_neq_one) \<longleftrightarrow> x \<in> A"
    1.11 +  by (auto simp: indicator_def)
    1.12 +
    1.13  lemma split_indicator:
    1.14    "P (indicator S x) \<longleftrightarrow> ((x \<in> S \<longrightarrow> P 1) \<and> (x \<notin> S \<longrightarrow> P 0))"
    1.15    unfolding indicator_def by auto