Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-08 23:00:34 -0700 (Mon, 08 Apr 2002)
Revision: 3571
Log message:

      Defined cosets for subgroups:
        Let H be a subgroup of a group G. aH = {ah | h in H} is the left
        coset of H containing a, while Ha = {ha | h in H} is the right
        coset of H containing a.
      
      The cosets of H are subsets of G.
      
      Suppose f: G1 -> G2 is a group homomorphism of G1 into G2; H is the
      kernel of f. For any a in G1, aH = Ha = { x in G1 | f(x) = f(a) }.
      (This is proved in Czf_itt_hom.)
      

Changes	Path
Added	metaprl/theories/czf/czf_itt_coset.ml
Properties	metaprl/theories/czf/czf_itt_coset.ml
Added	metaprl/theories/czf/czf_itt_coset.mli
Properties	metaprl/theories/czf/czf_itt_coset.mli
Added	metaprl/theories/czf/czf_itt_coset.prla
Properties	metaprl/theories/czf/czf_itt_coset.prla