helm/software/matita/contribs/CoRN-Decl/devel/loeb/per/csetfun.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/devel/loeb/per/csetfun".
  18
  19 (* INCLUDE
  20 CSetoids
  21 *)
  22
  23 (* INCLUDE
  24 CSetoidFun
  25 *)
  26
  27 inline cic:/CoRN/devel/loeb/per/csetfun/ap_fun.con.
  28
  29 inline cic:/CoRN/devel/loeb/per/csetfun/eq_fun.con.
  30
  31 inline cic:/CoRN/devel/loeb/per/csetfun/irrefl_apfun.con.
  32
  33 inline cic:/CoRN/devel/loeb/per/csetfun/cotrans_apfun.con.
  34
  35 inline cic:/CoRN/devel/loeb/per/csetfun/ta_apfun.con.
  36
  37 inline cic:/CoRN/devel/loeb/per/csetfun/sym_apfun.con.
  38
  39 inline cic:/CoRN/devel/loeb/per/csetfun/FS_is_CSetoid.con.
  40
  41 inline cic:/CoRN/devel/loeb/per/csetfun/FS_as_CSetoid.con.
  42
  43 (* UNEXPORTED
  44 Print associative.
  45 *)
  46
  47 inline cic:/CoRN/devel/loeb/per/csetfun/comp.con.
  48
  49 inline cic:/CoRN/devel/loeb/per/csetfun/comp_as_bin_op.con.
  50
  51 inline cic:/CoRN/devel/loeb/per/csetfun/assoc_comp.con.
  52
  53 (* INCLUDE
  54 CSemiGroups
  55 *)
  56
  57 inline cic:/CoRN/devel/loeb/per/csetfun/FS_as_CSemiGroup.con.
  58
  59 (* INCLUDE
  60 CMonoids
  61 *)
  62
  63 inline cic:/CoRN/devel/loeb/per/csetfun/FS_id.con.
  64
  65 inline cic:/CoRN/devel/loeb/per/csetfun/id_is_rht_unit.con.
  66
  67 inline cic:/CoRN/devel/loeb/per/csetfun/id_is_lft_unit.con.
  68
  69 inline cic:/CoRN/devel/loeb/per/csetfun/FS_is_CMonoid.con.
  70
  71 inline cic:/CoRN/devel/loeb/per/csetfun/FS_as_CMonoid.con.
  72
  73 inline cic:/CoRN/devel/loeb/per/csetfun/PS_as_CMonoid.con.
  74
  75 (* INCLUDE
  76 CGroups
  77 *)
  78
  79 inline cic:/CoRN/devel/loeb/per/csetfun/Inv_is_bij.con.
  80
  81 (* Lemma Inv_is_bij :
  82  forall (A B : CSetoid) (f : CSetoid_fun A B) (H : bijective f),
  83  bijective (Inv f H).
  84 intros A B f.
  85 case f.
  86 unfold fun_strext in |- *.
  87 intros f0 H5.
  88 unfold bijective in |- *.
  89 intro H.
  90 elim H.
  91 clear H.
  92 unfold injective in |- *.
  93 unfold surjective in |- *.
  94 intros H0 H1.
  95 split.
  96 unfold Inv in |- *.
  97 simpl in |- *.
  98 unfold invfun in |- *.
  99 simpl in |- *.
 100 unfold sigT_rect in |- *.
 101 intros a0 a1 H2.
 102 case H1.
 103 case (H1 a1).
 104 intros x H3 y H4.
 105 simpl in H3.
 106 simpl in H4.
 107 simpl in H0.
 108 simpl in H1.
 109 apply H5.
 110 astepl a0.
 111 astepr a1.
 112 exact H2.
 113
 114 simpl in |- *.
 115 unfold invfun in |- *.
 116 simpl in |- *.
 117 unfold sigT_rect in |- *.
 118 intros b.
 119 exists (f0 b).
 120 case (H1 (f0 b)).
 121 simpl in |- *.
 122 intros x H2.
 123 simpl in H0.
 124 simpl in H1.
 125 apply not_ap_imp_eq.
 126 red in |- *.
 127 intro H3.
 128 set (H4 := H0 x b H3) in *.
 129 set (H6 := ap_imp_neq B (f0 x) (f0 b) H4) in *.
 130 intuition.
 131 Qed.*)
 132
 133 inline cic:/CoRN/devel/loeb/per/csetfun/PS_Inv.con.
 134
 135 inline cic:/CoRN/devel/loeb/per/csetfun/Inv_as_un_op.con.
 136
 137 inline cic:/CoRN/devel/loeb/per/csetfun/PS_is_CGroup.con.
 138
 139 inline cic:/CoRN/devel/loeb/per/csetfun/PS_as_CGroup.con.
 140
 141 (* In het algemeen niet Abels! *)
 142