set "baseuri" "cic:/matita/algebra/groups/".
include "algebra/monoids.ma".
+include "nat/le_arith.ma".
record isGroup (M:Monoid) (opp: M -> M) : Prop ≝
{ opp_is_left_inverse: is_left_inverse M opp;
interpretation "Group inverse" 'gopp x =
(cic:/matita/algebra/groups/opp.con _ x).
-definition left_cancellable :=
- \lambda T:Type. \lambda op: T -> T -> T.
- \forall x,y,z. op x y = op x z -> y = z.
+definition left_cancellable ≝
+ λT:Type. λop: T -> T -> T.
+ ∀x. injective ? ? (op x).
-definition right_cancellable :=
- \lambda T:Type. \lambda op: T -> T -> T.
- \forall x,y,z. op y x = op z x -> y = z.
+definition right_cancellable ≝
+ λT:Type. λop: T -> T -> T.
+ ∀x. injective ? ? (λz.op z x).
theorem eq_op_x_y_op_x_z_to_eq:
- \forall G:Group. left_cancellable G (op G).
+ ∀G:Group. left_cancellable G (op G).
intros;
unfold left_cancellable;
-intros;
+unfold injective;
+intros (x y z);
rewrite < (e_is_left_unit ? ? (monoid_properties G));
-fold simplify (e G);
rewrite < (e_is_left_unit ? ? (monoid_properties G) z);
-fold simplify (e G);
rewrite < (opp_is_left_inverse ? ? (group_properties G) x);
-fold simplify (opp G);
rewrite > (semigroup_properties G);
-fold simplify (op G);
rewrite > (semigroup_properties G);
-fold simplify (op G);
apply eq_f;
assumption.
qed.
-(*
+
theorem eq_op_x_y_op_z_y_to_eq:
- \forall G:Group. right_cancellable G (op G).
+ ∀G:Group. right_cancellable G (op G).
+intros;
+unfold right_cancellable;
+unfold injective;
+simplify;fold simplify (op G);
+intros (x y z);
+rewrite < (e_is_right_unit ? ? (monoid_properties G));
+rewrite < (e_is_right_unit ? ? (monoid_properties G) z);
+rewrite < (opp_is_right_inverse ? ? (group_properties G) x);
+rewrite < (semigroup_properties G);
+rewrite < (semigroup_properties G);
+rewrite > H;
+reflexivity.
qed.
-definition has_cardinality :=
- \lambda T:Type. \lambda n:nat.
- \exists f. injective T nat f.
+(*
+record enumerable (T:Type) : Type ≝
+ { order: nat;
+ repr: nat → T;
+ repr_inj: ∀n,n'. n≤order → n'≤order → repr n ≠ repr n';
+ repr_sur: ∀x.∃n.n≤order ∧ repr n = x
+ }.
+
-definition finite :=
- \lambda T:Type.
- \exists f: T -> {n|n<
-*)
+theorem foo:
+ ∀G:SemiGroup.
+ enumerable (carrier G) →
+ left_cancellable (carrier G) (op G) →
+ right_cancellable (carrier G) (op G) →
+ ∃e:G. is_left_unit ? e.
+intros (G H);
+unfold left_cancellable in H1;
+letin x ≝ (repr ? H O);
+letin f ≝ (λy.x·(repr ? H y));
+generalize in match (H1 x);
+intro;
+*)
\ No newline at end of file