added a few thms
authornipkow
Wed Aug 04 19:09:41 2004 +0200 (2004-08-04)
changeset 15108492e5f3a8571
parent 15107 f233706d9fce
child 15109 bba563cdd997
added a few thms
src/HOL/Integ/Equiv.thy
     1.1 --- a/src/HOL/Integ/Equiv.thy	Wed Aug 04 17:43:55 2004 +0200
     1.2 +++ b/src/HOL/Integ/Equiv.thy	Wed Aug 04 19:09:41 2004 +0200
     1.3 @@ -132,6 +132,16 @@
     1.4    done
     1.5  
     1.6  
     1.7 +lemma quotient_empty [simp]: "{}//r = {}"
     1.8 +by(simp add: quotient_def)
     1.9 +
    1.10 +lemma quotient_is_empty [iff]: "(A//r = {}) = (A = {})"
    1.11 +by(simp add: quotient_def)
    1.12 +
    1.13 +lemma quotient_is_empty2 [iff]: "({} = A//r) = (A = {})"
    1.14 +by(simp add: quotient_def)
    1.15 +
    1.16 +
    1.17  subsection {* Defining unary operations upon equivalence classes *}
    1.18  
    1.19  text{*A congruence-preserving function*}