From 8c057e95fd8d88bcc74a2335482b16eedd0ee60c Mon Sep 17 00:00:00 2001 From: matitaweb Date: Thu, 30 May 2013 13:59:41 +0000 Subject: [PATCH] commit by user andrea --- weblib/basics/relations.ma | 42 +++++++++++++++++++------------------- 1 file changed, 21 insertions(+), 21 deletions(-) diff --git a/weblib/basics/relations.ma b/weblib/basics/relations.ma index 995198aac..753ed3233 100644 --- a/weblib/basics/relations.ma +++ b/weblib/basics/relations.ma @@ -12,78 +12,78 @@ include "basics/logic.ma". (********** relations **********) -img class="anchor" src="icons/tick.png" id="relation"definition relation : Type[0] → Type[0] +definition relation : Type[0] → Type[0] ≝ λA.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 +definition reflexive: ∀A.∀R :a href="cic:/matita/basics/relations/relation.def(1)"relation/a A.Prop ≝ λA.λR.∀x:A.R x x. -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 +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. -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 +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. -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 +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). -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 +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. -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 +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)). -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 +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 **********) -img class="anchor" src="icons/tick.png" id="compose"definition 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). -img class="anchor" src="icons/tick.png" id="injective"definition injective: ∀A,B:Type[0].∀ f:A→B.Prop +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. -img class="anchor" src="icons/tick.png" id="surjective"definition surjective: ∀A,B:Type[0].∀f:A→B.Prop +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. -img class="anchor" src="icons/tick.png" id="commutative"definition commutative: ∀A:Type[0].∀f:A→A→A.Prop +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. -img class="anchor" src="icons/tick.png" id="commutative2"definition commutative2: ∀A,B:Type[0].∀f:A→A→B.Prop +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. -img class="anchor" src="icons/tick.png" id="associative"definition associative: ∀A:Type[0].∀f:A→A→A.Prop +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 *) -img class="anchor" src="icons/tick.png" id="monotonic"definition monotonic : ∀A:Type[0].∀R:A→A→Prop. +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 *) -img class="anchor" src="icons/tick.png" id="distributive"definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop +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). -img class="anchor" src="icons/tick.png" id="distributive2"definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop +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). -img class="anchor" src="icons/tick.png" id="injective_compose"lemma injective_compose : ∀A,B,C,f,g. +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)). /span class="autotactic"3span class="autotrace" trace /span/span/; qed. (* extensional equality *) -img class="anchor" src="icons/tick.png" id="exteqP"definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ +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). -img class="anchor" src="icons/tick.png" id="exteqR"definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝ +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). -img class="anchor" src="icons/tick.png" id="exteqF"definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝ +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 -- 2.39.2