include "basics/logic.ma".
(********** relations **********)
-definition relation : Type[0] → Type[0]
+\ 5img class="anchor" src="icons/tick.png" id="relation"\ 6definition relation : Type[0] → Type[0]
≝ λA.A→A→Prop.
-definition reflexive: ∀A.∀R :relation A.Prop
+\ 5img class="anchor" src="icons/tick.png" id="reflexive"\ 6definition reflexive: ∀A.∀R :\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
≝ λA.λR.∀x:A.R x x.
-definition symmetric: ∀A.∀R: relation A.Prop
+\ 5img class="anchor" src="icons/tick.png" id="symmetric"\ 6definition symmetric: ∀A.∀R: \ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
≝ λA.λR.∀x,y:A.R x y → R y x.
-definition transitive: ∀A.∀R:relation A.Prop
+\ 5img class="anchor" src="icons/tick.png" id="transitive"\ 6definition transitive: ∀A.∀R:\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 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).
+\ 5img class="anchor" src="icons/tick.png" id="irreflexive"\ 6definition irreflexive: ∀A.∀R:\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
+≝ λA.λR.∀x:A.\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(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.
+\ 5img class="anchor" src="icons/tick.png" id="cotransitive"\ 6definition cotransitive: ∀A.∀R:\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
+≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 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)).
+\ 5img class="anchor" src="icons/tick.png" id="tight_apart"\ 6definition tight_apart: ∀A.∀eq,ap:\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
+≝ λA.λeq,ap.∀x,y:A. (\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(ap x y) → eq x y) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6
+(eq x y → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(ap x y)).
-definition antisymmetric: ∀A.∀R:relation A.Prop
-≝ λA.λR.∀x,y:A. R x y → ¬(R y x).
+\ 5img class="anchor" src="icons/tick.png" id="antisymmetric"\ 6definition antisymmetric: ∀A.∀R:\ 5a href="cic:/matita/basics/relations/relation.def(1)"\ 6relation\ 5/a\ 6 A.Prop
+≝ λA.λR.∀x,y:A. R x y → \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(R y x).
(********** functions **********)
-definition compose ≝
+\ 5img class="anchor" src="icons/tick.png" id="compose"\ 6definition 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
-≝ λA,B.λf.∀x,y:A.f x = f y → x=y.
+\ 5img class="anchor" src="icons/tick.png" id="injective"\ 6definition injective: ∀A,B:Type[0].∀ f:A→B.Prop
+≝ λA,B.λf.∀x,y:A.f x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f y → x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6y.
-definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
-≝λA,B.λf.∀z:B.∃x:A.z = f x.
+\ 5img class="anchor" src="icons/tick.png" id="surjective"\ 6definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
+≝λA,B.λf.∀z:B.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6x:A\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6.\ 5/a\ 6z \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x.
-definition commutative: ∀A:Type[0].∀f:A→A→A.Prop
-≝ λA.λf.∀x,y.f x y = f y x.
+\ 5img class="anchor" src="icons/tick.png" id="commutative"\ 6definition commutative: ∀A:Type[0].∀f:A→A→A.Prop
+≝ λA.λf.∀x,y.f x y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 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.
+\ 5img class="anchor" src="icons/tick.png" id="commutative2"\ 6definition commutative2: ∀A,B:Type[0].∀f:A→A→B.Prop
+≝ λA,B.λf.∀x,y.f x y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 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).
+\ 5img class="anchor" src="icons/tick.png" id="associative"\ 6definition associative: ∀A:Type[0].∀f:A→A→A.Prop
+≝ λA.λf.∀x,y,z.f (f x y) z \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 f x (f y z).
(* functions and relations *)
-definition monotonic : ∀A:Type[0].∀R:A→A→Prop.
+\ 5img class="anchor" src="icons/tick.png" id="monotonic"\ 6definition 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
-≝ λA.λf,g.∀x,y,z:A. f x (g y z) = g (f x y) (f x z).
+\ 5img class="anchor" src="icons/tick.png" id="distributive"\ 6definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop
+≝ λA.λf,g.∀x,y,z:A. f x (g y z) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 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).
+\ 5img class="anchor" src="icons/tick.png" id="distributive2"\ 6definition 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) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 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)).
-/3/; qed.
+\ 5img class="anchor" src="icons/tick.png" id="injective_compose"\ 6lemma injective_compose : ∀A,B,C,f,g.
+\ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 A B f → \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 B C g → \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 A C (λx.g (f x)).
+/\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/; qed.
(* extensional equality *)
-definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝
-λA.λP,Q.∀a.iff (P a) (Q a).
+\ 5img class="anchor" src="icons/tick.png" id="exteqP"\ 6definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝
+λA.λP,Q.∀a.\ 5a href="cic:/matita/basics/logic/iff.def(1)"\ 6iff\ 5/a\ 6 (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).
+\ 5img class="anchor" src="icons/tick.png" id="exteqR"\ 6definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
+λA,B.λR,S.∀a.∀b.\ 5a href="cic:/matita/basics/logic/iff.def(1)"\ 6iff\ 5/a\ 6 (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.
+\ 5img class="anchor" src="icons/tick.png" id="exteqF"\ 6definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
+λA,B.λf,g.∀a.f a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 g a.
notation " x \eqP y " non associative with precedence 45
for @{'eqP A $x $y}.
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
projects / helm.git / blobdiff