Definition: monoid_p
(compound):: IsMonoid(T;op;id) == Assoc(T;op) ∧ Ident(T;op;id)
Lemma: monoid_p_wf
∀[T:Type]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T]. (IsMonoid(T;op;id) ∈ ℙ)
Lemma: sq_stable__monoid_p
∀[T:Type]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T]. SqStable(IsMonoid(T;op;id))
Definition: group_p
(compound):: IsGroup(T;op;id;inv) == IsMonoid(T;op;id) ∧ Inverse(T;op;id;inv)
Lemma: group_p_wf
∀[T:Type]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T]. ∀[inv:T ⟶ T]. (IsGroup(T;op;id;inv) ∈ ℙ)
Lemma: sq_stable__group_p
∀[T:Type]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T]. ∀[inv:T ⟶ T]. SqStable(IsGroup(T;op;id;inv))
Definition: grp_sig
GrpSig == car:Type × eq:car ⟶ car ⟶ 𝔹 × le:car ⟶ car ⟶ 𝔹 × op:car ⟶ car ⟶ car × id:car × (car ⟶ car)
Lemma: grp_sig_wf
GrpSig ∈ 𝕌'
Definition: grp_car
|g| == fst(g)
Lemma: grp_car_wf
∀[g:GrpSig]. (|g| ∈ Type)
Definition: grp_eq
=b == fst(snd(g))
Lemma: grp_eq_wf
∀[g:GrpSig]. (=b ∈ |g| ⟶ |g| ⟶ 𝔹)
Definition: grp_le
≤b == fst(snd(snd(g)))
Lemma: grp_le_wf
∀[g:GrpSig]. (≤b ∈ |g| ⟶ |g| ⟶ 𝔹)
Definition: grp_op
* == fst(snd(snd(snd(g))))
Lemma: grp_op_wf
∀[g:GrpSig]. (* ∈ |g| ⟶ |g| ⟶ |g|)
Definition: grp_id
e == fst(snd(snd(snd(snd(g)))))
Lemma: grp_id_wf
∀[g:GrpSig]. (e ∈ |g|)
Definition: grp_inv
~ == snd(snd(snd(snd(snd(g)))))
Lemma: grp_inv_wf
∀[g:GrpSig]. (~ ∈ |g| ⟶ |g|)
Lemma: subtype_rel_grp
GrpSig ⊆r GrpSig{[i | j]}
Lemma: grp_sig_inc
GrpSig ⊆r GrpSig{[i | j]}
Lemma: comb_for_grp_car_wf
λg,z. |g| ∈ g:GrpSig ⟶ (↓True) ⟶ Type
Lemma: grp_op_l
∀[g:GrpSig]. ∀[a,b,c:|g|]. (a * b) = (a * c) ∈ |g| supposing b = c ∈ |g|
Lemma: grp_op_r
∀[g:GrpSig]. ∀[a,b,c:|g|]. (a * c) = (b * c) ∈ |g| supposing a = b ∈ |g|
Definition: imon
IMonoid == {g:GrpSig| IsMonoid(|g|;*;e)}
Lemma: imon_wf
IMonoid ∈ 𝕌'
Lemma: imon_subtype_grp_sig
IMonoid ⊆r GrpSig
Lemma: mk_imon
∀[T:Type]. ∀[eq,le:T ⟶ T ⟶ 𝔹]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T]. ∀[inv:T ⟶ T].
(<T, eq, le, op, id, inv> ∈ IMonoid) supposing (Ident(T;op;id) and Assoc(T;op))
Lemma: imon_properties
∀[g:IMonoid]. IsMonoid(|g|;*;e)
Lemma: imon_all_properties
∀[g:IMonoid]. (Assoc(|g|;*) ∧ Ident(|g|;*;e))
Lemma: mon_ident
∀[g:IMonoid]. ∀[a:|g|]. (((a * e) = a ∈ |g|) ∧ ((e * a) = a ∈ |g|))
Lemma: mon_assoc
∀[g:IMonoid]. ∀[a,b,c:|g|]. ((a * (b * c)) = ((a * b) * c) ∈ |g|)
Definition: mon
Mon == {g:GrpSig| IsMonoid(|g|;*;e)}
Definition: dmon
DMon == {g:Mon| IsEqFun(|g|;=b)}
Lemma: mon_wf
Mon ∈ 𝕌'
Lemma: mon_subtype_grp_sig
Mon ⊆r GrpSig
Lemma: dmon_wf
DMon ∈ 𝕌'
Lemma: dmon_subtype_mon
DMon ⊆r Mon
Lemma: mk_mon
∀[T:Type]. ∀[eq,le:T ⟶ T ⟶ 𝔹]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T]. ∀[inv:T ⟶ T].
(<T, eq, le, op, id, inv> ∈ Mon) supposing (Ident(T;op;id) and Assoc(T;op))
Lemma: mk_dmon
∀[T:Type]. ∀[eq,le:T ⟶ T ⟶ 𝔹]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T]. ∀[inv:T ⟶ T].
(<T, eq, le, op, id, inv> ∈ DMon) supposing (Ident(T;op;id) and Assoc(T;op) and IsEqFun(T;eq))
Lemma: mon_properties
∀[g:Mon]. IsMonoid(|g|;*;e)
Lemma: dmon_properties
∀[g:DMon]. IsEqFun(|g|;=b)
Lemma: assert_of_mon_eq
∀[s:DMon]. ∀[a,b:|s|]. uiff(↑(a =b b);a = b ∈ |s|)
Lemma: decidable__mon_eq
∀g:DMon. ∀a,b:|g|. Dec(a = b ∈ |g|)
Lemma: grp_eq_sym
∀[g:DMon]. ∀[a,b:|g|]. a =b b = b =b a
Definition: iabmonoid
IAbMonoid == {g:IMonoid| Comm(|g|;*)}
Lemma: iabmonoid_wf
IAbMonoid ∈ 𝕌'
Lemma: iabmonoid_subtype_imon
IAbMonoid ⊆r IMonoid
Lemma: iabmonoid_properties
∀[g:IAbMonoid]. Comm(|g|;*)
Lemma: abmonoid_comm
∀[g:IAbMonoid]. ∀[a,b:|g|]. ((a * b) = (b * a) ∈ |g|)
Lemma: abmonoid_ac_1
∀[g:IAbMonoid]. ∀[a,b,c:|g|]. ((a * (b * c)) = (b * (a * c)) ∈ |g|)
Definition: abmonoid
AbMon == {g:Mon| Comm(|g|;*)}
Lemma: abmonoid_wf
AbMon ∈ 𝕌'
Lemma: abmonoid_subtype_mon
AbMon ⊆r Mon
Lemma: abmonoid_subtype_iabmonoid
AbMon ⊆r IAbMonoid
Lemma: mk_abmonoid
∀[T:Type]. ∀[eq,le:T ⟶ T ⟶ 𝔹]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T]. ∀[inv:T ⟶ T].
(<T, eq, le, op, id, inv> ∈ AbMon) supposing (Comm(T;op) and Ident(T;op;id) and Assoc(T;op))
Lemma: abmonoid_inc
AbMon ⊆r AbMon{[i | j]}
Lemma: abmonoid_cumulative
AbMon ⊆r AbMon{[i | j]}
Lemma: abmonoid_properties
∀[g:AbMon]. Comm(|g|;*)
Definition: abdmonoid
AbDMon == {g:DMon| Comm(|g|;*)}
Lemma: abdmonoid_wf
AbDMon ∈ 𝕌'
Lemma: abdmonoid_dmon
AbDMon ⊆r DMon
Lemma: abdmonoid_abmonoid
AbDMon ⊆r AbMon
Lemma: mk_abdmonoid
∀[T:Type]. ∀[eq,le:T ⟶ T ⟶ 𝔹]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T]. ∀[inv:T ⟶ T].
(<T, eq, le, op, id, inv> ∈ AbDMon) supposing (Comm(T;op) and Ident(T;op;id) and Assoc(T;op) and IsEqFun(T;eq))
Lemma: abdmonoid_inc
AbDMon ⊆r AbDMon{[i | j]}
Lemma: abdmonoid_properties
∀[g:AbDMon]. Comm(|g|;*)
Definition: igrp
IGroup == {g:IMonoid| Inverse(|g|;*;e;~)}
Lemma: igrp_wf
IGroup ∈ 𝕌'
Lemma: igrp_properties
∀[g:IGroup]. Inverse(|g|;*;e;~)
Definition: mk_igrp
mk_igrp(T;op;id;inv) == <T, λx,y. tt, λx,y. tt, op, id, inv>
Lemma: mk_igrp_wf
∀[T:Type]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T]. ∀[inv:T ⟶ T].
(mk_igrp(T;op;id;inv) ∈ IGroup) supposing (Inverse(T;op;id;inv) and Ident(T;op;id) and Assoc(T;op))
Lemma: grp_inverse
∀[g:IGroup]. ∀[a:|g|]. (((a * (~ a)) = e ∈ |g|) ∧ (((~ a) * a) = e ∈ |g|))
Lemma: grp_op_cancel_l
∀[g:IGroup]. ∀[a,b,c:|g|]. b = c ∈ |g| supposing (a * b) = (a * c) ∈ |g|
Lemma: grp_op_cancel_r
∀[g:IGroup]. ∀[a,b,c:|g|]. a = b ∈ |g| supposing (a * c) = (b * c) ∈ |g|
Lemma: grp_inv_id
∀[g:IGroup]. ((~ e) = e ∈ |g|)
Lemma: grp_inv_inv
∀[g:IGroup]. ∀[a:|g|]. ((~ (~ a)) = a ∈ |g|)
Lemma: grp_inv_assoc
∀[g:IGroup]. ∀[a,b:|g|]. (((a * ((~ a) * b)) = b ∈ |g|) ∧ (((~ a) * (a * b)) = b ∈ |g|))
Lemma: grp_inv_thru_op
∀[g:IGroup]. ∀[a,b:|g|]. ((~ (a * b)) = ((~ b) * (~ a)) ∈ |g|)
Lemma: grp_eq_op_l
∀[g:IGroup]. ∀[a,b,c:|g|]. uiff(a = b ∈ |g|;(c * a) = (c * b) ∈ |g|)
Lemma: grp_eq_op_r
∀[g:IGroup]. ∀[a,b,c:|g|]. uiff(a = b ∈ |g|;(a * c) = (b * c) ∈ |g|)
Lemma: grp_eq_shift_right
∀[g:IGroup]. ∀[a,b:|g|]. uiff(a = b ∈ |g|;e = (b * (~ a)) ∈ |g|)
Lemma: grp_inv_diff
∀[g:IGroup]. ∀[a,b:|g|]. ((~ (a * (~ b))) = (b * (~ a)) ∈ |g|)
Definition: grp
Group{i} == {g:Mon| Inverse(|g|;*;e;~)}
Lemma: grp_wf
Group{i} ∈ 𝕌'
Lemma: grp_subtype_mon
Group{i} ⊆r Mon
Lemma: grp_subtype_igrp
Group{i} ⊆r IGroup
Lemma: grp_subtype_grp_sig
Group{i} ⊆r GrpSig
Lemma: mk_grp
∀[T:Type]. ∀[eq,le:T ⟶ T ⟶ 𝔹]. ∀[op:T ⟶ T ⟶ T]. ∀[id:T]. ∀[inv:T ⟶ T].
(<T, eq, le, op, id, inv> ∈ Group{i}) supposing (Inverse(T;op;id;inv) and Ident(T;op;id) and Assoc(T;op))
Lemma: grp_properties
∀[g:Group{i}]. Inverse(|g|;*;e;~)
Definition: subgrp_p
s SubGrp of g == (s e) ∧ (∀a:|g|. ((s a) ⇒ (s (~ a)))) ∧ (∀a,b:|g|. ((s a) ⇒ (s b) ⇒ (s (a * b))))
Lemma: subgrp_p_wf
∀[g:GrpSig]. ∀[s:|g| ⟶ ℙ]. (s SubGrp of g ∈ ℙ)
Definition: norm_subset_p
norm_subset_p(g;s) == ∀a,b:|g|. ((s b) ⇒ (s ((~ a) * (b * a))))
Lemma: norm_subset_p_wf
∀[g:GrpSig]. ∀[s:|g| ⟶ ℙ]. (norm_subset_p(g;s) ∈ ℙ)
Definition: norm_subgrp
NormSubGrp{i}(g) == {s:|g| ⟶ ℙ| s SubGrp of g ∧ norm_subset_p(g;s)}
Lemma: norm_subgrp_wf
∀[g:GrpSig]. (NormSubGrp{i}(g) ∈ 𝕌')
Definition: eqv_mod_subset
a ≡ b (mod s in g) == s (a * (~ b))
Lemma: eqv_mod_subset_wf
∀[g:GrpSig]. ∀[s:|g| ⟶ ℙ]. ∀[a,b:|g|]. (a ≡ b (mod s in g) ∈ ℙ)
Lemma: eqv_mod_subset_is_eqv
∀g:IGroup
∀[s:|g| ⟶ ℙ]
((s e)
⇒ (∀a:|g|. ((s a) ⇒ (s (~ a))))
⇒ (∀a,b:|g|. ((s a) ⇒ (s b) ⇒ (s (a * b))))
⇒ EquivRel(|g|;x,y.x ≡ y (mod s in g)))
Definition: iabgrp
IAbGrp{i} == {g:IGroup| Comm(|g|;*)}
Lemma: iabgrp_wf
IAbGrp{i} ∈ 𝕌'
Lemma: iabgrp_op_inv_assoc
∀[g:IAbGrp{i}]. ∀[a,b:|g|]. (((a * ((~ a) * b)) = b ∈ |g|) ∧ (((~ a) * (a * b)) = b ∈ |g|))
Lemma: iabgrp_properties
∀[g:IAbGrp{i}]. Comm(|g|;*)
Definition: quot_grp_car
|g//h| == a,b:|g|//a ≡ b (mod h in g)
Lemma: quot_grp_car_wf
∀g:IGroup. ∀h:NormSubGrp{i}(g). (|g//h| ∈ Type)
Lemma: quot_grp_inv_wf
∀g:IGroup. ∀h:NormSubGrp{i}(g). (~ ∈ |g//h| ⟶ |g//h|)
Definition: abgrp
AbGrp == {g:Group{i}| Comm(|g|;*)}
Definition: abdgrp
AbDGrp == {g:AbGrp| IsEqFun(|g|;=b)}
Lemma: abgrp_wf
AbGrp ∈ 𝕌'
Lemma: abgrp_subtype_grp
AbGrp ⊆r Group{i}
Lemma: abdgrp_wf
AbDGrp ∈ 𝕌'
Lemma: abdgrp_subtype_abgrp
AbDGrp ⊆r AbGrp
Lemma: abgrp_properties
∀[g:AbGrp]. Comm(|g|;*)
Lemma: abdgrp_properties
∀[g:AbDGrp]. IsEqFun(|g|;=b)
Definition: monoid_hom_p
(compound):: IsMonHom{M1,M2}(f) == FunThru2op(|M1|;|M2|;*;*;f) ∧ ((f e) = e ∈ |M2|)
Lemma: monoid_hom_p_wf
∀[a,b:GrpSig]. ∀[f:|a| ⟶ |b|]. (IsMonHom{a,b}(f) ∈ ℙ)
Definition: mon_hom_inj_p
(compound):: IsMonHomInj(g;h;f) == IsMonHom{g,h}(f) ∧ Inj(|g|;|h|;f)
Lemma: mon_hom_inj_p_wf
∀[g,h:GrpSig]. ∀[f:|g| ⟶ |h|]. (IsMonHomInj(g;h;f) ∈ ℙ)
Definition: monoid_hom
MonHom(M1,M2) == {f:|M1| ⟶ |M2|| IsMonHom{M1,M2}(f)}
Lemma: monoid_hom_wf
∀[A,B:GrpSig]. (MonHom(A,B) ∈ Type)
Lemma: sq_stable__monoid_hom_p
∀[a,b:GrpSig]. ∀[f:|a| ⟶ |b|]. SqStable(IsMonHom{a,b}(f))
Lemma: monoid_hom_properties
∀[g,h:GrpSig]. ∀[f:MonHom(g,h)]. IsMonHom{g,h}(f)
Lemma: monoid_hom_id
∀[g,h:GrpSig]. ∀[f:MonHom(g,h)]. ((f e) = e ∈ |h|)
Lemma: monoid_hom_op
∀[g,h:GrpSig]. ∀[f:MonHom(g,h)]. ∀[u,v:|g|]. ((f (u * v)) = ((f u) * (f v)) ∈ |h|)
Lemma: id-is-monoid_hom
∀[A:GrpSig]. (λx.x ∈ MonHom(A,A))
Lemma: grp_hom_formation
∀[g,h:IGroup]. ∀[f:|g| ⟶ |h|]. IsMonHom{g,h}(f) supposing ∀a,b:|g|. ((f (a * b)) = ((f a) * (f b)) ∈ |h|)
Lemma: grp_hom_inv
∀[g,h:IGroup]. ∀[f:MonHom(g,h)]. ∀[a:|g|]. ((f (~ a)) = (~ (f a)) ∈ |h|)
Definition: inj_mon_hom
InjMonHom(g;h) == {f:MonHom(g,h)| Inj(|g|;|h|;f)}
Lemma: inj_mon_hom_wf
∀[g,h:GrpSig]. (InjMonHom(g;h) ∈ Type)
Lemma: inj_mon_hom_properties
∀[g,h:GrpSig]. ∀[f:InjMonHom(g;h)]. Inj(|g|;|h|;f)
Lemma: ident_mon_hom_shift
∀[g,h:GrpSig]. ∀[f:MonHom(g,h)]. (Ident(|g|;*;e)) supposing (Ident(|h|;*;e) and Inj(|g|;|h|;f))
Lemma: inverse_grp_sig_hom_shift
∀[g,h:GrpSig]. ∀[f:MonHom(g,h)].
(Inverse(|g|;*;e;~)) supposing (Inverse(|h|;*;e;~) and Inj(|g|;|h|;f) and fun_thru_1op(|g|;|h|;~;~;f))
Lemma: mon_hom_p_id
∀[g:GrpSig]. IsMonHom{g,g}(Id{|g|})
Lemma: mon_hom_p_comp
∀[g,h,k:GrpSig]. ∀[r:|g| ⟶ |h|]. ∀[s:|h| ⟶ |k|].
(IsMonHom{g,k}(s o r)) supposing (IsMonHom{h,k}(s) and IsMonHom{g,h}(r))
Lemma: tidentity_wf_for_mon_hom
∀[g:IMonoid]. (Id{|g|} ∈ MonHom(g,g))
Lemma: compose_wf_for_mon_hom
∀[A,B,C:IMonoid]. ∀[f:MonHom(A,B)]. ∀[g:MonHom(B,C)]. (g o f ∈ MonHom(A,C))
Lemma: comb_for_compose_wf_for_mon_hom
λA,B,C,f,g,z. (g o f) ∈ A:IMonoid ⟶ B:IMonoid ⟶ C:IMonoid ⟶ f:MonHom(A,B) ⟶ g:MonHom(B,C) ⟶ (↓True) ⟶ MonHom(A,C)
Definition: dset_of_mon
g↓set == <|g|, =b, ≤b>
Lemma: dset_of_mon_wf0
∀[g:GrpSig]. (g↓set ∈ PosetSig)
Lemma: dset_of_mon_wf
∀[g:DMon]. (g↓set ∈ DSet)
Definition: omon
OMon == {g:AbMon| UniformLinorder(|g|;x,y.↑(x ≤b y)) ∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|g| ⟶ |g| ⟶ 𝔹))}
Lemma: omon_wf
OMon ∈ 𝕌'
Lemma: omon_properties
∀g:OMon. (UniformLinorder(|g|;x,y.↑(x ≤b y)) ∧ IsEqFun(|g|;=b))
Lemma: omon_subtype
OMon ⊆r AbDMon
Lemma: omon_inc
∀x:OMon. (x ∈ AbDMon)
Definition: ocmon
OCMon ==
{g:AbMon|
(UniformLinorder(|g|;x,y.↑(x ≤b y)) ∧ (=b = (λx,y. ((x ≤b y) ∧b (y ≤b x))) ∈ (|g| ⟶ |g| ⟶ 𝔹)))
∧ Cancel(|g|;|g|;*)
∧ (∀[z:|g|]. monot(|g|;x,y.↑(x ≤b y);λw.(z * w)))}
Lemma: ocmon_wf
OCMon ∈ 𝕌'
Lemma: ocmon_subtype_abdmonoid
OCMon ⊆r AbDMon
Lemma: ocmon_subtype_omon
OCMon ⊆r OMon
Lemma: ocmon_properties
∀g:OCMon
(UniformLinorder(|g|;x,y.↑(x ≤b y))
∧ Cancel(|g|;|g|;*)
∧ (∀[z:|g|]. monot(|g|;x,y.↑(x ≤b y);λw.(z * w)))
∧ IsEqFun(|g|;=b))
Lemma: ocmon_refl
∀[g:OCMon]. ∀[a:|g|]. (↑(a ≤b a))
Lemma: ocmon_trans
∀[g:OCMon]. ∀[a,b,c:|g|]. (↑(a ≤b c)) supposing ((↑(b ≤b c)) and (↑(a ≤b b)))
Lemma: ocmon_anti_sym
∀[g:OCMon]. ∀[x,y:|g|]. (x = y ∈ |g|) supposing ((↑(y ≤b x)) and (↑(x ≤b y)))
Lemma: ocmon_connex
∀g:OCMon. ∀x,y:|g|. ((↑(x ≤b y)) ∨ (↑(y ≤b x)))
Lemma: ocmon_cancel
∀[g:OCMon]. ∀[u,v,w:|g|]. u = v ∈ |g| supposing (w * u) = (w * v) ∈ |g|
Lemma: ocmon_6
∀[g:OCMon]. ∀[z:|g|]. monot(|g|;x,y.↑(x ≤b y);λw.(z * w))
Definition: oset_of_ocmon
g↓oset == g↓set
Lemma: oset_of_ocmon_wf0
∀[g:GrpSig]. (g↓oset ∈ PosetSig)
Lemma: oset_of_ocmon_wf
∀[g:OMon]. (g↓oset ∈ LOSet)
Lemma: dset_of_mon_wf2
∀[g:OMon]. (g↓set ∈ LOSet)
Definition: grp_leq
a ≤ b == ↑(a ≤b b)
Lemma: grp_leq_wf
∀[g:GrpSig]. ∀[a,b:|g|]. (a ≤ b ∈ ℙ)
Lemma: comb_for_grp_leq_wf
λg,a,b,z. (a ≤ b) ∈ g:GrpSig ⟶ a:|g| ⟶ b:|g| ⟶ (↓True) ⟶ ℙ
Lemma: sq_stable__grp_leq
∀[g:GrpSig]. ∀[a,b:|g|]. SqStable(a ≤ b)
Definition: grp_lt
a < b == a <(g↓oset) b
Lemma: grp_lt_wf
∀[g:GrpSig]. ∀[a,b:|g|]. (a < b ∈ ℙ)
Lemma: comb_for_grp_lt_wf
λg,a,b,z. (a < b) ∈ g:GrpSig ⟶ a:|g| ⟶ b:|g| ⟶ (↓True) ⟶ ℙ
Lemma: grp_leq_iff_lt_or_eq
∀g:OMon. ∀a,b:|g|. (a ≤ b ⇐⇒ (a < b) ∨ (a = b ∈ |g|))
Lemma: decidable__grp_lt
∀g:OCMon. ∀a,b:|g|. Dec(a < b)
Lemma: grp_lt_is_sp_of_leq_a
∀[g:OMon]. ∀[a,b:|g|]. uiff(a < b;(a ≤ b) ∧ (¬(b ≤ a)))
Lemma: grp_lt_trans
∀[g:OCMon]. ∀[a,b,c:|g|]. (a < c) supposing ((b < c) and (a < b))
Lemma: grp_lt_irreflexivity
∀[g:OCMon]. ∀[a:|g|]. False supposing a < a
Lemma: grp_lt_transitivity_2
∀[g:OCMon]. ∀[a,b,c:|g|]. (a < c) supposing ((b ≤ c) and (a < b))
Lemma: grp_lt_transitivity_1
∀[g:OCMon]. ∀[a,b,c:|g|]. (a < c) supposing ((b < c) and (a ≤ b))
Lemma: grp_leq_weakening_eq
∀[g:OMon]. ∀[a,b:|g|]. a ≤ b supposing a = b ∈ |g|
Lemma: grp_leq_weakening_lt
∀[g:OMon]. ∀[a,b:|g|]. a ≤ b supposing a < b
Lemma: grp_leq_transitivity
∀[g:OCMon]. ∀[a,b,c:|g|]. (a ≤ c) supposing ((b ≤ c) and (a ≤ b))
Lemma: omon_lt_mono_imp_leq_mono
∀[g:OMon]. {∀[a:|g|]. monot(|g|;x,y.x ≤ y;λz.(a * z))} supposing ∀a:|g|. monot(|g|;x,y.x < y;λz.(a * z))
Lemma: grp_leq_antisymmetry
∀[g:OCMon]. ∀[a,b:|g|]. (a = b ∈ |g|) supposing ((b ≤ a) and (a ≤ b))
Lemma: grp_leq_complement
∀[g:OCMon]. ∀[a,b:|g|]. uiff(¬(a ≤ b);b < a)
Lemma: grp_lt_complement
∀[g:OCMon]. ∀[a,b:|g|]. uiff(¬(b < a);a ≤ b)
Lemma: grp_lt_trichot
∀g:OCMon. ∀a,b:|g|. ((a < b) ∨ (a = b ∈ |g|) ∨ (b < a))
Lemma: grp_op_preserves_le
∀[g:OCMon]. ∀[x,y,z:|g|]. (x * y) ≤ (x * z) supposing y ≤ z
Lemma: grp_op_preserves_lt
∀[g:OCMon]. ∀[u,v,w:|g|]. (u * v) < (u * w) supposing v < w
Definition: ocgrp
OGrp == {g:OCMon| Inverse(|g|;*;e;~)}
Lemma: ocgrp_wf
OGrp ∈ 𝕌'
Lemma: ocgrp_subtype_ocmon
OGrp ⊆r OCMon
Lemma: ocgrp_subtype_abgrp
OGrp ⊆r AbGrp
Lemma: ocgrp_subtype_abdgrp
OGrp ⊆r AbDGrp
Lemma: ocgrp_properties
∀[g:OGrp]. Inverse(|g|;*;e;~)
Lemma: ocgrp_inverse
∀[g:OGrp]. ∀[x:|g|]. (((x * (~ x)) = e ∈ |g|) ∧ (((~ x) * x) = e ∈ |g|))
Lemma: ocgrp_abdgrp
∀[g:OGrp]. (g ∈ AbDGrp)
Lemma: grp_leq_op_l
∀[g:OGrp]. ∀[a,b,c:|g|]. uiff(a ≤ b;(c * a) ≤ (c * b))
Lemma: grp_lt_op_l
∀[g:OGrp]. ∀[a,b,c:|g|]. uiff(a < b;(c * a) < (c * b))
Lemma: grp_op_polarity
∀[g:OGrp]. ∀[a,b:|g|]. (e ≤ (a * b)) supposing ((e ≤ b) and (e ≤ a))
Definition: grp_blt
a <b b == a <b b
Lemma: grp_blt_wf
∀[g:GrpSig]. ∀[a,b:|g|]. (a <b b ∈ 𝔹)
Lemma: assert_of_grp_blt
∀[g:OCMon]. ∀[a,b:|g|]. uiff(↑(a <b b);a < b)
Lemma: grp_lt_shift_right
∀[g:OGrp]. ∀[a,b:|g|]. uiff(a < b;e < (b * (~ a)))
Lemma: grp_leq_shift_right
∀[g:OGrp]. ∀[a,b:|g|]. uiff(a ≤ b;e ≤ (b * (~ a)))
Lemma: inj_into_ocmon
∀[g:GrpSig]
g ∈ OCMon
supposing ∃h:OCMon
∃f:|g| ⟶ |h|
(IsMonHomInj(g;h;f)
∧ RelsIso(|g|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
∧ RelsIso(|g|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f))
Definition: hgrp_car
|g|+ == {x:|g|| e ≤ x}
Lemma: hgrp_car_wf
∀[g:GrpSig]. (|g|+ ∈ Type)
Lemma: hgrp_car_properties
∀[g:GrpSig]. ∀[x:|g|+]. (e ≤ x)
Lemma: grp_op_wf2
∀[g:OGrp]. (* ∈ |g|+ ⟶ |g|+ ⟶ |g|+)
Lemma: grp_id_wf2
∀[g:OGrp]. (e ∈ |g|+)
Definition: hgrp_of_ocgrp
g↓hgrp == <|g|+, =b, ≤b, *, e, λx.x>
Lemma: hgrp_of_ocgrp_wf
∀[g:OGrp]. (g↓hgrp ∈ GrpSig)
Lemma: hgrp_of_ocgrp_wf2
∀[g:OGrp]. (g↓hgrp ∈ OCMon)
Definition: itop
Π(op,id) lb ≤ i < ub. E[i] == Y (λitop,ub. if lb <z ub then (itop (ub - 1)) op E[ub - 1] else id fi ) ub
Lemma: itop_wf
∀[A:Type]. ∀[op:A ⟶ A ⟶ A]. ∀[id:A]. ∀[p,q:ℤ]. ∀[E:{p..q-} ⟶ A]. (Π(op,id) p ≤ i < q. E[i] ∈ A)
Lemma: comb_for_itop_wf
λA,op,id,p,q,E,z. Π(op,id) p ≤ i < q. E[i] ∈ A:Type ⟶ op:(A ⟶ A ⟶ A) ⟶ id:A ⟶ p:ℤ ⟶ q:ℤ ⟶ E:({p..q-} ⟶ A) ⟶ (↓T\000Crue) ⟶ A
Lemma: itop_aux_wf
∀[A:Type]. ∀[op:A ⟶ A ⟶ A]. ∀[id:A]. ∀[p:ℤ]. ∀[q:{p...}]. ∀[E:{p..q-} ⟶ A]. (Π(op,id) p ≤ i < q. E[i] ∈ A)
Lemma: itop_unroll_empty
∀[g:IMonoid]. ∀[i,j:ℤ]. ∀[E:{i..j-} ⟶ |g|]. (Π(*,e) i ≤ k < j. E[k] = e ∈ |g|) supposing j ≤ i
Lemma: itop_unroll_base
∀[g:IMonoid]. ∀[i,j:ℤ]. ∀[E:{i..j-} ⟶ |g|]. (Π(*,e) i ≤ k < j. E[k] = e ∈ |g|) supposing i = j ∈ ℤ
Lemma: itop_unroll_hi
∀[g:IMonoid]. ∀[i,j:ℤ].
∀[E:{i..j-} ⟶ |g|]. (Π(*,e) i ≤ k < j. E[k] = (Π(*,e) i ≤ k < j - 1. E[k] * E[j - 1]) ∈ |g|) supposing i < j
Lemma: itop_unroll_unit
∀[g:IMonoid]. ∀[i,j:ℤ]. ∀[E:{i..j-} ⟶ |g|]. (Π(*,e) i ≤ k < j. E[k] = E[i] ∈ |g|) supposing (i + 1) = j ∈ ℤ
Lemma: itop_unroll_lo
∀[g:IMonoid]. ∀[i,j:ℤ].
∀[E:{i..j-} ⟶ |g|]. (Π(*,e) i ≤ k < j. E[k] = (E[i] * Π(*,e) i + 1 ≤ k < j. E[k]) ∈ |g|) supposing i < j
Lemma: itop_shift
∀[g:IMonoid]. ∀[a,b:ℤ].
∀[E:{a..b-} ⟶ |g|]. ∀[k:ℤ]. (Π(*,e) a ≤ j < b. E[j] = Π(*,e) a + k ≤ j < b + k. E[j - k] ∈ |g|) supposing a ≤ b
Lemma: itop_split
∀[g:IMonoid]. ∀[a,b,c:ℤ].
(∀[E:{a..c-} ⟶ |g|]. (Π(*,e) a ≤ j < c. E[j] = (Π(*,e) a ≤ j < b. E[j] * Π(*,e) b ≤ j < c. E[j]) ∈ |g|)) supposing
((b ≤ c) and
(a ≤ b))
Definition: nat_op
n x(op;id) e == Π(op,id) 0 ≤ i < n. e
Lemma: nat_op_wf
∀[g:IMonoid]. ∀[n:ℕ]. ∀[e:|g|]. (n x(*;e) e ∈ |g|)
Lemma: comb_for_nat_op_wf
λg,n,e,z. n x(*;e) e ∈ g:IMonoid ⟶ n:ℕ ⟶ e:|g| ⟶ (↓True) ⟶ |g|
Lemma: nat_op_zero
∀[g:IMonoid]. ∀[e:|g|]. (0 x(*;e) e = e ∈ |g|)
Lemma: nat_op_add
∀[g:IMonoid]. ∀[e:|g|]. ∀[a,b:ℕ]. (a + b x(*;e) e = (a x(*;e) e * b x(*;e) e) ∈ |g|)
Definition: int_op
i x(op;id;inv) e == if 0 ≤z i then i x(op;id) e else inv -i x(op;id) e fi
Lemma: int_op_wf
∀[g:Group{i}]. ∀[a:ℤ]. ∀[e:|g|]. (a x(*;e;~) e ∈ |g|)
Lemma: comb_for_int_op_wf
λg,a,e,z. a x(*;e;~) e ∈ g:Group{i} ⟶ a:ℤ ⟶ e:|g| ⟶ (↓True) ⟶ |g|
Lemma: int_op_minus
∀[g:Group{i}]. ∀[e:|g|]. ∀[a:ℤ]. (-a x(*;e;~) e = (~ a x(*;e;~) e) ∈ |g|)
Definition: mon_itop
Π lb ≤ i < ub. E[i] == Π(*,e) lb ≤ i < ub. E[i]
Lemma: mon_itop_wf
∀[g:IMonoid]. ∀[p,q:ℤ]. ∀[E:{p..q-} ⟶ |g|]. (Π p ≤ i < q. E[i] ∈ |g|)
Lemma: comb_for_mon_itop_wf
λg,p,q,E,z. (Π p ≤ i < q. E[i]) ∈ g:IMonoid ⟶ p:ℤ ⟶ q:ℤ ⟶ E:({p..q-} ⟶ |g|) ⟶ (↓True) ⟶ |g|
Lemma: mon_itop_unroll_empty
∀[g:IMonoid]. ∀[i,j:ℤ]. ∀[E:{i..j-} ⟶ |g|]. ((Π i ≤ k < j. E[k]) = e ∈ |g|) supposing j ≤ i
Lemma: mon_itop_unroll_base
∀[g:IMonoid]. ∀[i,j:ℤ]. ∀[E:{i..j-} ⟶ |g|]. ((Π i ≤ k < j. E[k]) = e ∈ |g|) supposing i = j ∈ ℤ
Lemma: mon_itop_unroll_hi
∀[g:IMonoid]. ∀[i,j:ℤ].
∀[E:{i..j-} ⟶ |g|]. ((Π i ≤ k < j. E[k]) = ((Π i ≤ k < j - 1. E[k]) * E[j - 1]) ∈ |g|) supposing i < j
Lemma: mon_itop_unroll_unit
∀[g:IMonoid]. ∀[i,j:ℤ]. ∀[E:{i..j-} ⟶ |g|]. ((Π i ≤ k < j. E[k]) = E[i] ∈ |g|) supposing (i + 1) = j ∈ ℤ
Lemma: mon_itop_unroll_lo
∀[g:IMonoid]. ∀[i,j:ℤ].
∀[E:{i..j-} ⟶ |g|]. ((Π i ≤ k < j. E[k]) = (E[i] * (Π i + 1 ≤ k < j. E[k])) ∈ |g|) supposing i < j
Lemma: mon_itop_shift
∀[g:IMonoid]. ∀[a,b:ℤ].
∀[E:{a..b-} ⟶ |g|]. ∀[k:ℤ]. ((Π a ≤ j < b. E[j]) = (Π a + k ≤ j < b + k. E[j - k]) ∈ |g|) supposing a ≤ b
Lemma: mon_itop_split
∀[g:IMonoid]. ∀[a,b,c:ℤ].
(∀[E:{a..c-} ⟶ |g|]. ((Π a ≤ j < c. E[j]) = ((Π a ≤ j < b. E[j]) * (Π b ≤ j < c. E[j])) ∈ |g|)) supposing
((b ≤ c) and
(a ≤ b))
Lemma: mon_itop_split_el
∀[g:IMonoid]. ∀[a,b,c:ℤ].
(∀[E:{a..c-} ⟶ |g|]
((Π a ≤ j < c. E[j]) = ((Π a ≤ j < b. E[j]) * (E[b] * (Π b + 1 ≤ j < c. E[j]))) ∈ |g|)) supposing
(b < c and
(a ≤ b))
Lemma: mon_itop_op
∀[g:IAbMonoid]. ∀[a,b:ℤ].
∀[E,F:{a..b-} ⟶ |g|]. ((Π a ≤ i < b. E[i] * F[i]) = ((Π a ≤ i < b. E[i]) * (Π a ≤ i < b. F[i])) ∈ |g|)
supposing a ≤ b
Definition: mon_nat_op
n ⋅ e == n x(*;e) e
Lemma: mon_nat_op_wf
∀[g:IMonoid]. ∀[n:ℕ]. ∀[e:|g|]. (n ⋅ e ∈ |g|)
Lemma: comb_for_mon_nat_op_wf
λg,n,e,z. (n ⋅ e) ∈ g:IMonoid ⟶ n:ℕ ⟶ e:|g| ⟶ (↓True) ⟶ |g|
Lemma: mon_nat_op_zero
∀[g:IMonoid]. ∀[e:|g|]. ((0 ⋅ e) = e ∈ |g|)
Lemma: mon_nat_op_unroll
∀[g:IMonoid]. ∀[n:ℕ+]. ∀[e:|g|]. ((n ⋅ e) = (((n - 1) ⋅ e) * e) ∈ |g|)
Lemma: mon_nat_op_one
∀[g:IMonoid]. ∀[e:|g|]. ((1 ⋅ e) = e ∈ |g|)
Lemma: mon_nat_op_id
∀[g:IMonoid]. ∀[n:ℕ]. ((n ⋅ e) = e ∈ |g|)
Lemma: mon_nat_op_op
∀[g:IAbMonoid]. ∀[n:ℕ]. ∀[a,b:|g|]. ((n ⋅ (a * b)) = ((n ⋅ a) * (n ⋅ b)) ∈ |g|)
Lemma: mon_nat_op_add
∀[g:IMonoid]. ∀[e:|g|]. ∀[a,b:ℕ]. (((a + b) ⋅ e) = ((a ⋅ e) * (b ⋅ e)) ∈ |g|)
Lemma: mon_nat_op_hom_swap
∀[g,h:IMonoid]. ∀[f:MonHom(g,h)]. ∀[n:ℕ]. ∀[u:|g|]. ((n ⋅ (f u)) = (f (n ⋅ u)) ∈ |h|)
Lemma: mon_nat_op_mul
∀[g:IMonoid]. ∀[m,n:ℕ]. ∀[e:|g|]. ((n ⋅ (m ⋅ e)) = ((n * m) ⋅ e) ∈ |g|)
Definition: comp_id_mon
(<o,Id> monoid on T) == <T ⟶ T, λx,y. tt, λx,y. tt, λf,g. (f o g), Id, λx.x>
Lemma: comp_id_mon_wf
∀[T:Type]. ((<o,Id> monoid on T) ∈ IMonoid)
Definition: bor_mon
<𝔹,∨b> == <𝔹, λx,y. x =b y, λx,y. tt, λx,y. (x ∨by), ff, λx.x>
Lemma: bor_mon_wf
<𝔹,∨b> ∈ AbMon
Definition: band_mon
<𝔹,∧b> == <𝔹, λx,y. x =b y, λx,y. tt, λx,y. (x ∧b y), tt, λx.x>
Lemma: band_mon_wf
<𝔹,∧b> ∈ AbMon
Definition: int_add_grp
<ℤ+> == <ℤ, λx,y. (x =z y), λx,y. x ≤z y, λx,y. (x + y), 0, λx.(-x)>
Lemma: int_add_grp_wf
<ℤ+> ∈ AbGrp
Lemma: int_add_grp_wf2
<ℤ+> ∈ OGrp
Definition: nat_add_mon
<ℕ,+> == <ℕ, λx,y. (x =z y), λx,y. x ≤z y, λx,y. (x + y), 0, λx.x>
Lemma: nat_add_mon_wf
<ℕ,+> ∈ GrpSig
Lemma: nat_int_grp_sig_hom
IsMonHomInj(<ℕ,+>;<ℤ+>;λx.x)
Lemma: nat_add_mon_wf2
<ℕ,+> ∈ OCMon
Lemma: nat_op_mon_hom_1
∀[g:IMonoid]. ∀[a:|g|]. IsMonHom{<ℕ,+>,g}(λn.(n ⋅ a))
Lemma: nat_op_mon_hom_2
∀[g:IAbMonoid]. ∀[n:ℕ]. IsMonHom{g,g}(λa.(n ⋅ a))
Lemma: nat_op_on_nat_add_mon
∀[m,n:ℕ]. ((m ⋅ n) = (m * n) ∈ ℕ)
Definition: int_mul_mon
<ℤ,*> == <ℤ, λx,y. (x =z y), λx,y. x ≤z y, λx,y. (x * y), 1, λx.x>
Lemma: int_mul_mon_wf
<ℤ,*> ∈ AbMon
Definition: mon_when
when b. p == if b then p else e fi
Lemma: mon_when_wf
∀[g:IMonoid]. ∀[b:𝔹]. ∀[p:|g|]. (when b. p ∈ |g|)
Lemma: comb_for_mon_when_wf
λg,b,p,z. (when b. p) ∈ g:IMonoid ⟶ b:𝔹 ⟶ p:|g| ⟶ (↓True) ⟶ |g|
Lemma: mon_when_false
∀[g:GrpSig]. ∀[b:𝔹]. ∀[x:|g|]. (when b. x) = e ∈ |g| supposing ¬↑b
Lemma: mon_when_true
∀[g:GrpSig]. ∀[b:𝔹]. ∀[x:|g|]. (when b. x) = x ∈ |g| supposing ↑b
Lemma: mon_when_of_id
∀[g:IMonoid]. ∀[b:𝔹]. ((when b. e) = e ∈ |g|)
Lemma: mon_when_thru_op
∀[g:IMonoid]. ∀[b:𝔹]. ∀[p,q:|g|]. ((when b. (p * q)) = ((when b. p) * (when b. q)) ∈ |g|)
Lemma: mon_when_when
∀[g:Mon]. ∀[b,b':𝔹]. ∀[p:|g|]. ((when b. when b'. p) = (when b ∧b b'. p) ∈ |g|)
Lemma: mon_when_swap
∀[g:Mon]. ∀[b,b':𝔹]. ∀[p:|g|]. ((when b. when b'. p) = (when b'. when b. p) ∈ |g|)
Lemma: mon_when_is_hom
∀[g:IMonoid]. ∀[b:𝔹]. IsMonHom{g,g}(λp:|g|. when b. p)
Lemma: mon_when_hom_swap
∀[g,h:GrpSig]. ∀[f:MonHom(g,h)]. ∀[b:𝔹]. ∀[p:|g|]. ((when b. (f p)) = (f (when b. p)) ∈ |h|)
Lemma: nat_inc
ℕ ⊆r |(<ℤ+>↓hgrp)|
Lemma: nat_subtype
ℕ ⊆r |(<ℤ+>↓hgrp)|
Lemma: grp_car_inc
|(<ℤ+>↓hgrp)| ⊆r ℕ
Lemma: grp_car_subtype
|(<ℤ+>↓hgrp)| ⊆r ℕ
Definition: int_hgrp_el
zhgrp(n) == n
Lemma: int_hgrp_el_wf
∀[n:ℕ]. (zhgrp(n) ∈ |(<ℤ+>↓hgrp)|)
Definition: int_hgrp_to_nat
nat(n) == n
Lemma: int_hgrp_to_nat_wf
∀[n:|(<ℤ+>↓hgrp)|]. (nat(n) ∈ ℕ)
Lemma: zhgrp_to_nat_is_hom
IsMonHom{<ℤ+>↓hgrp,<ℕ,+>}(λn.nat(n))
Lemma: zhgrp_op_mon_hom_1
∀[g:IMonoid]. ∀[a:|g|]. IsMonHom{<ℤ+>↓hgrp,g}(λn.(nat(n) ⋅ a))
Lemma: mon_nat_op_wf2
∀[g:IMonoid]. ∀[n:|(<ℤ+>↓hgrp)|]. ∀[e:|g|]. (n ⋅ e ∈ |g|)
Lemma: comb_for_mon_nat_op_wf2
λg,n,e,z. (n ⋅ e) ∈ g:IMonoid ⟶ n:|(<ℤ+>↓hgrp)| ⟶ e:|g| ⟶ (↓True) ⟶ |g|
Home
Index