X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Frelations.ma;h=995198aac2483ee8a56cb720ea609f8a1739ed0f;hb=05090b74e381e19a7867b12bb685cdb898c910c8;hp=3081fa96b05d8d5a3c966372a9b609b243afcf34;hpb=8baa4aabe6cc848c6a3ecd7a08e1bab9edc8bee1;p=helm.git

diff --git a/weblib/basics/relations.ma b/weblib/basics/relations.ma
index 3081fa96b..995198aac 100644
--- a/weblib/basics/relations.ma
+++ b/weblib/basics/relations.ma
@@ -12,78 +12,78 @@
 include "basics/logic.ma".
 
 (********** relations **********)
-definition relation : Type[0] → Type[0]
+img class="anchor" src="icons/tick.png" id="relation"definition relation : Type[0] → Type[0]
 ≝ λA.A→A→Prop. 
 
-definition reflexive: ∀A.∀R :a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop
+img class="anchor" src="icons/tick.png" id="reflexive"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: a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop
+img class="anchor" src="icons/tick.png" id="symmetric"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:a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop
+img class="anchor" src="icons/tick.png" id="transitive"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:a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop
+img class="anchor" src="icons/tick.png" id="irreflexive"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:a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop
+img class="anchor" src="icons/tick.png" id="cotransitive"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:a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop
+img class="anchor" src="icons/tick.png" id="tight_apart"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:a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop
+img class="anchor" src="icons/tick.png" id="antisymmetric"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 **********)
 
-definition compose ≝
+img class="anchor" src="icons/tick.png" id="compose"definition compose ≝
   λA,B,C:Type[0].λf:B→C.λg:A→B.λx:A.f (g x).
 
 interpretation "function composition" 'compose f g = (compose ? ? ? f g).
 
-definition injective: ∀A,B:Type[0].∀ f:A→B.Prop
+img class="anchor" src="icons/tick.png" id="injective"definition injective: ∀A,B:Type[0].∀ f:A→B.Prop
 ≝ λ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.a title="exists" href="cic:/fakeuri.def(1)"∃/ax:A.z a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f x.
+img class="anchor" src="icons/tick.png" id="surjective"definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
+≝λA,B.λf.∀z:B.a title="exists" href="cic:/fakeuri.def(1)"∃/ax:Aa title="exists" href="cic:/fakeuri.def(1)"./az a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f x.
 
-definition commutative: ∀A:Type[0].∀f:A→A→A.Prop 
+img class="anchor" src="icons/tick.png" id="commutative"definition commutative: ∀A:Type[0].∀f:A→A→A.Prop 
 ≝ λ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
+img class="anchor" src="icons/tick.png" id="commutative2"definition commutative2: ∀A,B:Type[0].∀f:A→A→B.Prop
 ≝ λ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
+img class="anchor" src="icons/tick.png" id="associative"definition associative: ∀A:Type[0].∀f:A→A→A.Prop
 ≝ λ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.
+img class="anchor" src="icons/tick.png" id="monotonic"definition monotonic : ∀A:Type[0].∀R:A→A→Prop.
 ∀f:A→A.Prop ≝
 λA.λR.λf.∀x,y:A.R x y → R (f x) (f y).
 
 (* functions and functions *)
-definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop
+img class="anchor" src="icons/tick.png" id="distributive"definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop
 ≝ λ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
+img class="anchor" src="icons/tick.png" id="distributive2"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) 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.
+img class="anchor" src="icons/tick.png" id="injective_compose"lemma injective_compose : ∀A,B,C,f,g.
 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.
+/span class="autotactic"3span class="autotrace" trace /span/span/; qed.
 
 (* extensional equality *)
 
-definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝
+img class="anchor" src="icons/tick.png" id="exteqP"definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝
 λ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 ≝
+img class="anchor" src="icons/tick.png" id="exteqR"definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
 λ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 ≝
+img class="anchor" src="icons/tick.png" id="exteqF"definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
 λ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