From 8baa4aabe6cc848c6a3ecd7a08e1bab9edc8bee1 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 11 Oct 2011 11:09:25 +0000 Subject: [PATCH] commit by user utente1 --- weblib/arithmetics/nat.ma | 35 ++++++++++++++------------- weblib/basics/relations.ma | 49 +++++++++++++++++++------------------- 2 files changed, 42 insertions(+), 42 deletions(-) diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma index f14392e93..ef8da2f19 100644 --- a/weblib/arithmetics/nat.ma +++ b/weblib/arithmetics/nat.ma @@ -389,7 +389,7 @@ apply (not_le_Sn_n ? H3). qed. *) theorem not_eq_to_le_to_lt: ∀n,m. na title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/am → na title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/am → na title="natural 'less than'" href="cic:/fakeuri.def(1)"</am. -#n #m #Hneq #Hle cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a ?? Hle) // +#n #m #Hneq #Hle cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(6)"le_to_or_lt_eq/a ?? Hle) // #Heq /3/ qed. (* nelim (Hneq Heq) qed. *) @@ -478,7 +478,7 @@ theorem increasing_to_le2: ∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0 ∀m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. f a title="natural number" href="cic:/fakeuri.def(1)"0/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m → a title="exists" href="cic:/fakeuri.def(1)"∃/ai. f i a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m a title="logical and" href="cic:/fakeuri.def(1)"∧/a m a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a f (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a i). #f #incr #m #lem (elim lem) [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a ? ? a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a) /2/ - |#n #len * #a * #len #ltnr (cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … ltnr)) #H + |#n #len * #a * #len #ltnr (cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(6)"le_to_or_lt_eq/a … ltnr)) #H [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a ? ? a) % /2/ |@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a ? ? (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a a)) % // ] @@ -488,7 +488,7 @@ qed. theorem increasing_to_injective: ∀f:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/increasing.def(2)"increasing/a f → a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a f. #f #incr #n #m cases(a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"decidable_le/a n m) - [#lenm cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … lenm) // + [#lenm cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(6)"le_to_or_lt_eq/a … lenm) // #lenm #eqf @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … eqf) @a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"lt_to_not_eq/a @a href="cic:/matita/arithmetics/nat/increasing_to_monotonic.def(4)"increasing_to_monotonic/a // |#nlenm #eqf @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a … eqf) @a href="cic:/matita/basics/logic/sym_not_eq.def(4)"sym_not_eq/a @@ -700,14 +700,14 @@ qed. theorem lt_to_le_to_lt_times: ∀n,m,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → p a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a q → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a q → na title="natural times" href="cic:/fakeuri.def(1)"*/ap a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a ma title="natural times" href="cic:/fakeuri.def(1)"*/aq. #n #m #p #q #ltnm #lepq #posq -@(a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"le_to_lt_to_lt/a ? (na title="natural times" href="cic:/fakeuri.def(1)"*/aq)) +@(a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(5)"le_to_lt_to_lt/a ? (na title="natural times" href="cic:/fakeuri.def(1)"*/aq)) [@a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a // - |@a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(9)"monotonic_lt_times_l/a // + |@a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(10)"monotonic_lt_times_l/a // ] qed. theorem lt_times:∀n,m,p,q:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. na title="natural 'less than'" href="cic:/fakeuri.def(1)"</am → pa title="natural 'less than'" href="cic:/fakeuri.def(1)"</aq → na title="natural times" href="cic:/fakeuri.def(1)"*/ap a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a ma title="natural times" href="cic:/fakeuri.def(1)"*/aq. -#n #m #p #q #ltnm #ltpq @a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(10)"lt_to_le_to_lt_times/a/2/ +#n #m #p #q #ltnm #ltpq @a href="cic:/matita/arithmetics/nat/lt_to_le_to_lt_times.def(11)"lt_to_le_to_lt_times/aspan style="text-decoration: underline;" /span/2/ qed. theorem lt_times_n_to_lt_l: @@ -811,7 +811,8 @@ napplyS (not_eq_to_le_to_lt n (S m) H H1) qed. *) theorem eq_minus_S_pred: ∀n,m. n a title="natural minus" href="cic:/fakeuri.def(1)"-/a (a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a m) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a(n a title="natural minus" href="cic:/fakeuri.def(1)"-/am). -@a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a normalize // qed. +@a href="cic:/matita/arithmetics/nat/nat_elim2.def(2)"nat_elim2/a normalize // +qed. theorem plus_minus: ∀m,n,p:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → (na title="natural minus" href="cic:/fakeuri.def(1)"-/am)a title="natural plus" href="cic:/fakeuri.def(1)"+/ap a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a (na title="natural plus" href="cic:/fakeuri.def(1)"+/ap)a title="natural minus" href="cic:/fakeuri.def(1)"-/am. @@ -844,7 +845,7 @@ qed. theorem minus_pred_pred : ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a m → a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a n a title="natural minus" href="cic:/fakeuri.def(1)"-/a a href="cic:/matita/arithmetics/nat/pred.def(1)"pred/a m a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a n a title="natural minus" href="cic:/fakeuri.def(1)"-/a m. -#n #m #posn #posm @(a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(4)"lt_O_n_elim/a n posn) @(a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(4)"lt_O_n_elim/a m posm) //. +#n #m #posn #posm @(a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(7)"lt_O_n_elim/a n posn) @(a href="cic:/matita/arithmetics/nat/lt_O_n_elim.def(7)"lt_O_n_elim/a m posm) //. qed. @@ -910,7 +911,7 @@ qed. theorem le_minus_to_plus: ∀n,m,p. na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → na title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a pa title="natural plus" href="cic:/fakeuri.def(1)"+/am. #n #m #p #lep @a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a - [|@a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(6)"le_plus_minus_m_m/a | @a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a // ] + [|@a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(8)"le_plus_minus_m_m/a | @a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a // ] qed. theorem le_minus_to_plus_r: ∀a,b,c. c a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b → a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b a title="natural minus" href="cic:/fakeuri.def(1)"-/a c → a a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b. @@ -930,22 +931,22 @@ theorem lt_minus_to_plus: ∀a,b,c. a a title="natural minus" href="cic:/fakeur qed. theorem lt_minus_to_plus_r: ∀a,b,c. a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b a title="natural minus" href="cic:/fakeuri.def(1)"-/a c → a a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b. -#a #b #c #H @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(7)"le_plus_to_minus/a …)) +#a #b #c #H @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(9)"le_plus_to_minus/a …)) @a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a // qed. theorem lt_plus_to_minus: ∀n,m,p. m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n → n a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a pa title="natural plus" href="cic:/fakeuri.def(1)"+/am → na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a p. -#n #m #p #lenm #H normalize <a href="cic:/matita/arithmetics/nat/minus_Sn_m.def(5)"minus_Sn_m/a // @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(7)"le_plus_to_minus/a // +#n #m #p #lenm #H normalize <a href="cic:/matita/arithmetics/nat/minus_Sn_m.def(5)"minus_Sn_m/a // @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(9)"le_plus_to_minus/a // qed. theorem lt_plus_to_minus_r: ∀a,b,c. a a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c a title="natural minus" href="cic:/fakeuri.def(1)"-/a b. -#a #b #c #H @a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(7)"le_plus_to_minus_r/a // +#a #b #c #H @a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(9)"le_plus_to_minus_r/a // qed. theorem monotonic_le_minus_r: ∀p,q,n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. q a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → na title="natural minus" href="cic:/fakeuri.def(1)"-/ap a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a na title="natural minus" href="cic:/fakeuri.def(1)"-/aq. -#p #q #n #lepq @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(7)"le_plus_to_minus/a -@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(6)"le_plus_minus_m_m/a ? q)) /2/ +#p #q #n #lepq @a href="cic:/matita/arithmetics/nat/le_plus_to_minus.def(9)"le_plus_to_minus/a +@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(8)"le_plus_minus_m_m/a ? q)) /2/ qed. theorem eq_minus_O: ∀n,m:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. @@ -956,7 +957,7 @@ qed. theorem distributive_times_minus: a href="cic:/matita/basics/relations/distributive.def(1)"distributive/a ? a href="cic:/matita/arithmetics/nat/times.fix(0,0,2)"times/a a href="cic:/matita/arithmetics/nat/minus.fix(0,0,1)"minus/a. #a #b #c (cases (a href="cic:/matita/arithmetics/nat/decidable_lt.def(7)"decidable_lt/a b c)) #Hbc - [> a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a /2/ >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a // + [> a href="cic:/matita/arithmetics/nat/eq_minus_O.def(11)"eq_minus_O/a /2/ >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(11)"eq_minus_O/a // @a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a /2/ |@a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a (applyS a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"plus_to_minus/a) <a href="cic:/matita/arithmetics/nat/distributive_times_plus.def(7)"distributive_times_plus/a @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a (applyS a href="cic:/matita/arithmetics/nat/plus_minus_m_m.def(7)"plus_minus_m_m/a) /2/ @@ -968,7 +969,7 @@ cases (a href="cic:/matita/arithmetics/nat/decidable_le.def(6)"decidable_le/a [@a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"plus_to_minus/a @a href="cic:/matita/arithmetics/nat/plus_to_minus.def(7)"plus_to_minus/a <a href="cic:/matita/arithmetics/nat/associative_plus.def(4)"associative_plus/a @a href="cic:/matita/arithmetics/nat/minus_to_plus.def(8)"minus_to_plus/a // |cut (n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a ma title="natural plus" href="cic:/fakeuri.def(1)"+/ap) [@(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … (a href="cic:/matita/arithmetics/nat/le_n_Sn.def(1)"le_n_Sn/a …)) @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a //] - #H >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a /2/ >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(9)"eq_minus_O/a // + #H >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(11)"eq_minus_O/a /2/ >a href="cic:/matita/arithmetics/nat/eq_minus_O.def(11)"eq_minus_O/a // ] qed. @@ -1115,4 +1116,4 @@ lemma le_maxr: ∀i,n,m. a href="cic:/matita/arithmetics/nat/max.def(2)"max/a lemma to_max: ∀i,n,m. n a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i → a href="cic:/matita/arithmetics/nat/max.def(2)"max/a n m a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a i. #i #n #m #leni #lemi normalize (cases (a href="cic:/matita/arithmetics/nat/leb.fix(0,0,1)"leb/a n m)) -normalize // qed. +normalize // qed. \ No newline at end of file diff --git a/weblib/basics/relations.ma b/weblib/basics/relations.ma index b31db23d7..3081fa96b 100644 --- a/weblib/basics/relations.ma +++ b/weblib/basics/relations.ma @@ -15,27 +15,27 @@ include "basics/logic.ma". definition relation : Type[0] → Type[0] ≝ λA.A→A→Prop. -definition reflexive: ∀A.∀R :relation A.Prop +definition reflexive: ∀A.∀R :a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop ≝ λA.λR.∀x:A.R x x. -definition symmetric: ∀A.∀R: relation A.Prop +definition symmetric: ∀A.∀R: a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop ≝ λA.λR.∀x,y:A.R x y → R y x. -definition transitive: ∀A.∀R:relation A.Prop +definition transitive: ∀A.∀R:a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop ≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z. -definition irreflexive: ∀A.∀R:relation A.Prop -≝ λA.λR.∀x:A.¬(R x x). +definition irreflexive: ∀A.∀R:a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop +≝ λA.λR.∀x:A.a title="logical not" href="cic:/fakeuri.def(1)"¬/a(R x x). -definition cotransitive: ∀A.∀R:relation A.Prop -≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y. +definition cotransitive: ∀A.∀R:a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop +≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z a title="logical or" href="cic:/fakeuri.def(1)"∨/a R z y. -definition tight_apart: ∀A.∀eq,ap:relation A.Prop -≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧ -(eq x y → ¬(ap x y)). +definition tight_apart: ∀A.∀eq,ap:a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop +≝ λA.λeq,ap.∀x,y:A. (a title="logical not" href="cic:/fakeuri.def(1)"¬/a(ap x y) → eq x y) a title="logical and" href="cic:/fakeuri.def(1)"∧/a +(eq x y → a title="logical not" href="cic:/fakeuri.def(1)"¬/a(ap x y)). -definition antisymmetric: ∀A.∀R:relation A.Prop -≝ λA.λR.∀x,y:A. R x y → ¬(R y x). +definition antisymmetric: ∀A.∀R:a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop +≝ λA.λR.∀x,y:A. R x y → a title="logical not" href="cic:/fakeuri.def(1)"¬/a(R y x). (********** functions **********) @@ -45,19 +45,19 @@ definition compose ≝ interpretation "function composition" 'compose f g = (compose ? ? ? f g). definition injective: ∀A,B:Type[0].∀ f:A→B.Prop -≝ λA,B.λf.∀x,y:A.f x = f y → x=y. +≝ λA,B.λf.∀x,y:A.f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f y → xa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ay. definition surjective: ∀A,B:Type[0].∀f:A→B.Prop -≝λA,B.λf.∀z:B.∃x:A.z = f x. +≝λA,B.λf.∀z:B.a title="exists" href="cic:/fakeuri.def(1)"∃/ax:A.z a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f x. definition commutative: ∀A:Type[0].∀f:A→A→A.Prop -≝ λA.λf.∀x,y.f x y = f y x. +≝ λA.λf.∀x,y.f x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f y x. definition commutative2: ∀A,B:Type[0].∀f:A→A→B.Prop -≝ λA,B.λf.∀x,y.f x y = f y x. +≝ λA,B.λf.∀x,y.f x y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f y x. definition associative: ∀A:Type[0].∀f:A→A→A.Prop -≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z). +≝ λA.λf.∀x,y,z.f (f x y) z a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f x (f y z). (* functions and relations *) definition monotonic : ∀A:Type[0].∀R:A→A→Prop. @@ -66,25 +66,25 @@ definition monotonic : ∀A:Type[0].∀R:A→A→Prop. (* functions and functions *) definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop -≝ λA.λf,g.∀x,y,z:A. f x (g y z) = g (f x y) (f x z). +≝ λA.λf,g.∀x,y,z:A. f x (g y z) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g (f x y) (f x z). definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop -≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) = g (f x y) (f x z). +≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g (f x y) (f x z). lemma injective_compose : ∀A,B,C,f,g. -injective A B f → injective B C g → injective A C (λx.g (f x)). +a href="cic:/matita/basics/relations/injective.def(1)"injective/a A B f → a href="cic:/matita/basics/relations/injective.def(1)"injective/a B C g → a href="cic:/matita/basics/relations/injective.def(1)"injective/a A C (λx.g (f x)). /3/; qed. (* extensional equality *) definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ -λA.λP,Q.∀a.iff (P a) (Q a). +λA.λP,Q.∀a.a href="cic:/matita/basics/logic/iff.def(1)"iff/a (P a) (Q a). definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝ -λA,B.λR,S.∀a.∀b.iff (R a b) (S a b). +λA,B.λR,S.∀a.∀b.a href="cic:/matita/basics/logic/iff.def(1)"iff/a (R a b) (S a b). definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝ -λA,B.λf,g.∀a.f a = g a. +λA,B.λf,g.∀a.f a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a g a. notation " x \eqP y " non associative with precedence 45 for @{'eqP A $x $y}. @@ -102,5 +102,4 @@ notation " f \eqF g " non associative with precedence 45 for @{'eqF ? ? f g}. interpretation "functional extentional equality" -'eqF A B f g = (exteqF A B f g). - +'eqF A B f g = (exteqF A B f g). \ No newline at end of file -- 2.39.2