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 "CoRN.ma".
  20
  21 include "algebra/CSetoids.ma".
  22
  23 include "algebra/CSetoidFun.ma".
  24
  25 inline "cic:/CoRN/devel/loeb/per/csetfun/ap_fun.con".
  26
  27 inline "cic:/CoRN/devel/loeb/per/csetfun/eq_fun.con".
  28
  29 inline "cic:/CoRN/devel/loeb/per/csetfun/irrefl_apfun.con".
  30
  31 inline "cic:/CoRN/devel/loeb/per/csetfun/cotrans_apfun.con".
  32
  33 inline "cic:/CoRN/devel/loeb/per/csetfun/ta_apfun.con".
  34
  35 inline "cic:/CoRN/devel/loeb/per/csetfun/sym_apfun.con".
  36
  37 inline "cic:/CoRN/devel/loeb/per/csetfun/FS_is_CSetoid.con".
  38
  39 inline "cic:/CoRN/devel/loeb/per/csetfun/FS_as_CSetoid.con".
  40
  41 (* UNEXPORTED
  42 Print associative.
  43 *)
  44
  45 inline "cic:/CoRN/devel/loeb/per/csetfun/comp.con".
  46
  47 inline "cic:/CoRN/devel/loeb/per/csetfun/comp_as_bin_op.con".
  48
  49 inline "cic:/CoRN/devel/loeb/per/csetfun/assoc_comp.con".
  50
  51 include "algebra/CSemiGroups.ma".
  52
  53 inline "cic:/CoRN/devel/loeb/per/csetfun/FS_as_CSemiGroup.con".
  54
  55 include "algebra/CMonoids.ma".
  56
  57 inline "cic:/CoRN/devel/loeb/per/csetfun/FS_id.con".
  58
  59 inline "cic:/CoRN/devel/loeb/per/csetfun/id_is_rht_unit.con".
  60
  61 inline "cic:/CoRN/devel/loeb/per/csetfun/id_is_lft_unit.con".
  62
  63 inline "cic:/CoRN/devel/loeb/per/csetfun/FS_is_CMonoid.con".
  64
  65 inline "cic:/CoRN/devel/loeb/per/csetfun/FS_as_CMonoid.con".
  66
  67 inline "cic:/CoRN/devel/loeb/per/csetfun/PS_as_CMonoid.con".
  68
  69 include "algebra/CGroups.ma".
  70
  71 inline "cic:/CoRN/devel/loeb/per/csetfun/Inv_is_bij.con".
  72
  73 (* Lemma Inv_is_bij :
  74  forall (A B : CSetoid) (f : CSetoid_fun A B) (H : bijective f),
  75  bijective (Inv f H).
  76 intros A B f.
  77 case f.
  78 unfold fun_strext in |- *.
  79 intros f0 H5.
  80 unfold bijective in |- *.
  81 intro H.
  82 elim H.
  83 clear H.
  84 unfold injective in |- *.
  85 unfold surjective in |- *.
  86 intros H0 H1.
  87 split.
  88 unfold Inv in |- *.
  89 simpl in |- *.
  90 unfold invfun in |- *.
  91 simpl in |- *.
  92 unfold sigT_rect in |- *.
  93 intros a0 a1 H2.
  94 case H1.
  95 case (H1 a1).
  96 intros x H3 y H4.
  97 simpl in H3.
  98 simpl in H4.
  99 simpl in H0.
 100 simpl in H1.
 101 apply H5.
 102 astepl a0.
 103 astepr a1.
 104 exact H2.
 105
 106 simpl in |- *.
 107 unfold invfun in |- *.
 108 simpl in |- *.
 109 unfold sigT_rect in |- *.
 110 intros b.
 111 exists (f0 b).
 112 case (H1 (f0 b)).
 113 simpl in |- *.
 114 intros x H2.
 115 simpl in H0.
 116 simpl in H1.
 117 apply not_ap_imp_eq.
 118 red in |- *.
 119 intro H3.
 120 set (H4 := H0 x b H3) in *.
 121 set (H6 := ap_imp_neq B (f0 x) (f0 b) H4) in *.
 122 intuition.
 123 Qed.*)
 124
 125 inline "cic:/CoRN/devel/loeb/per/csetfun/PS_Inv.con".
 126
 127 inline "cic:/CoRN/devel/loeb/per/csetfun/Inv_as_un_op.con".
 128
 129 inline "cic:/CoRN/devel/loeb/per/csetfun/PS_is_CGroup.con".
 130
 131 inline "cic:/CoRN/devel/loeb/per/csetfun/PS_as_CGroup.con".
 132
 133 (* In het algemeen niet Abels! *)
 134