2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "basics/logic.ma".
14 (********** predicates *********)
16 definition predicate: Type[0] → Type[0]
19 (********** relations **********)
20 definition relation : Type[0] → Type[0]
23 definition relation2 : Type[0] → Type[0] → Type[0]
26 definition reflexive: ∀A.∀R :relation A.Prop
29 definition symmetric: ∀A.∀R: relation A.Prop
30 ≝ λA.λR.∀x,y:A.R x y → R y x.
32 definition transitive: ∀A.∀R:relation A.Prop
33 ≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z.
35 definition irreflexive: ∀A.∀R:relation A.Prop
36 ≝ λA.λR.∀x:A.¬(R x x).
38 definition cotransitive: ∀A.∀R:relation A.Prop
39 ≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
41 definition tight_apart: ∀A.∀eq,ap:relation A.Prop
42 ≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧
45 definition antisymmetric: ∀A.∀R:relation A.Prop
46 ≝ λA.λR.∀x,y:A. R x y → ¬(R y x).
48 (********** functions **********)
51 λA,B,C:Type[0].λf:B→C.λg:A→B.λx:A.f (g x).
53 interpretation "function composition" 'compose f g = (compose ? ? ? f g).
55 definition injective: ∀A,B:Type[0].∀ f:A→B.Prop
56 ≝ λA,B.λf.∀x,y:A.f x = f y → x=y.
58 definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
59 ≝λA,B.λf.∀z:B.∃x:A.z = f x.
61 definition commutative: ∀A:Type[0].∀f:A→A→A.Prop
62 ≝ λA.λf.∀x,y.f x y = f y x.
64 definition commutative2: ∀A,B:Type[0].∀f:A→A→B.Prop
65 ≝ λA,B.λf.∀x,y.f x y = f y x.
67 definition associative: ∀A:Type[0].∀f:A→A→A.Prop
68 ≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z).
70 (* functions and relations *)
71 definition monotonic : ∀A:Type[0].∀R:A→A→Prop.
73 λA.λR.λf.∀x,y:A.R x y → R (f x) (f y).
75 (* functions and functions *)
76 definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop
77 ≝ λA.λf,g.∀x,y,z:A. f x (g y z) = g (f x y) (f x z).
79 definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop
80 ≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) = g (f x y) (f x z).
82 lemma injective_compose : ∀A,B,C,f,g.
83 injective A B f → injective B C g → injective A C (λx.g (f x)).
86 (* extensional equality *)
88 (* moved inside sets.ma
89 definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝
90 λA.λP,Q.∀a.iff (P a) (Q a). *)
92 definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
93 λA,B.λR,S.∀a.∀b.iff (R a b) (S a b).
95 definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
96 λA,B.λf,g.∀a.f a = g a.
99 notation " x \eqP y " non associative with precedence 45
102 interpretation "functional extentional equality"
103 'eqP A x y = (exteqP A x y). *)
105 notation "x \eqR y" non associative with precedence 45
108 interpretation "functional extentional equality"
109 'eqR A B R S = (exteqR A B R S).
111 notation " f \eqF g " non associative with precedence 45
114 interpretation "functional extentional equality"
115 'eqF A B f g = (exteqF A B f g).