src/HOL/Library/Quotient_Product.thy
changeset 47936 756f30eac792
parent 47777 f29e7dcd7c40
child 47982 7aa35601ff65
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Wed May 16 18:16:51 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Wed May 16 19:15:45 2012 +0200
     1.3 @@ -27,6 +27,12 @@
     1.4    shows "prod_rel (op =) (op =) = (op =)"
     1.5    by (simp add: fun_eq_iff)
     1.6  
     1.7 +lemma prod_reflp [reflp_preserve]:
     1.8 +  assumes "reflp R1"
     1.9 +  assumes "reflp R2"
    1.10 +  shows "reflp (prod_rel R1 R2)"
    1.11 +using assms by (auto intro!: reflpI elim: reflpE)
    1.12 +
    1.13  lemma prod_equivp [quot_equiv]:
    1.14    assumes "equivp R1"
    1.15    assumes "equivp R2"