1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 (* $Id: CSetoidFun.v,v 1.12 2004/09/22 11:06:10 loeb Exp $ *)
17 set "baseuri" "cic:/matita/algebra/CoRN/SetoidFun".
18 include "algebra/CoRN/Setoids.ma".
21 definition ap_fun : \forall A,B : CSetoid. \forall f,g : CSetoid_fun A B. Prop \def
22 \lambda A,B : CSetoid. \lambda f,g : CSetoid_fun A B.
23 \exists a:A. (csf_fun A B f) a \neq (csf_fun A B g) a.
24 (* Definition ap_fun (A B : CSetoid) (f g : CSetoid_fun A B) :=
25 {a : A | f a[#]g a}. *)
27 definition eq_fun : \forall A,B : CSetoid. \forall f,g : CSetoid_fun A B. Prop \def
28 \lambda A,B : CSetoid. \lambda f,g : CSetoid_fun A B.
29 \forall a:A. (csf_fun A B f) a = (csf_fun A B g) a.
30 (* Definition eq_fun (A B : CSetoid) (f g : CSetoid_fun A B) :=
31 forall a : A, f a[=]g a. *)
33 lemma irrefl_apfun : \forall A,B : CSetoid.
34 irreflexive (CSetoid_fun A B) (ap_fun A B).
36 unfold irreflexive. intro f.
41 cut (csf_fun A B f a = csf_fun A B f a)
50 apply eq_reflexive_unfolded
55 Lemma irrefl_apfun : forall A B : CSetoid, irreflexive (ap_fun A B).
57 unfold irreflexive in |- *.
59 unfold ap_fun in |- *.
64 set (H1 := ap_irreflexive_unfolded B (f a)) in *.
71 lemma cotrans_apfun : \forall A,B : CSetoid. cotransitive (CSetoid_fun A B) (ap_fun A B).
77 apply ap_cotransitive.
78 apply (ap_imp_neq B (csf_fun A B x a) (csf_fun A B y a) H1).
79 (* letin foo \def (\exist a:A.csf_fun A B x a\neq csf_fun A B z a). *)
82 apply (ap_cotransitive B ? ? H1 ?).
89 set (H1 := ap_cotransitive B (f a) (g a) H (h a)) in *.
106 Lemma cotrans_apfun : forall A B : CSetoid, cotransitive (ap_fun A B).
108 unfold cotransitive in |- *.
109 unfold ap_fun in |- *.
114 set (H1 := ap_cotransitive B (f a) (g a) H (h a)) in *.
130 lemma ta_apfun : \forall A, B : CSetoid. tight_apart (CSetoid_fun A B) (eq_fun A B) (ap_fun A B).
137 apply not_ap_imp_eq.unfold.intro.auto.
138 |intros. unfold.intro.elim H1.
139 apply (ap_imp_neq B ? ? H2). auto.