equal
deleted
inserted
replaced
140 by(simp add: quotient_def) |
140 by(simp add: quotient_def) |
141 |
141 |
142 lemma quotient_is_empty2 [iff]: "({} = A//r) = (A = {})" |
142 lemma quotient_is_empty2 [iff]: "({} = A//r) = (A = {})" |
143 by(simp add: quotient_def) |
143 by(simp add: quotient_def) |
144 |
144 |
|
145 |
|
146 lemma singleton_quotient: "{x}//r = {r `` {x}}" |
|
147 by(simp add:quotient_def) |
|
148 |
|
149 lemma quotient_diff1: |
|
150 "\<lbrakk> inj_on (%a. {a}//r) A; a \<in> A \<rbrakk> \<Longrightarrow> (A - {a})//r = A//r - {a}//r" |
|
151 apply(simp add:quotient_def inj_on_def) |
|
152 apply blast |
|
153 done |
145 |
154 |
146 subsection {* Defining unary operations upon equivalence classes *} |
155 subsection {* Defining unary operations upon equivalence classes *} |
147 |
156 |
148 text{*A congruence-preserving function*} |
157 text{*A congruence-preserving function*} |
149 locale congruent = |
158 locale congruent = |