blob: 068d4903a452e98ee80a1c24de61c40fe3f07901 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
(* $Id$ *)
(****************************************************************************)
(* Bruno Barras *)
(****************************************************************************)
Section Inverse_Image.
Variables A,B:Set.
Variable R : B->B->Prop.
Variable f:A->B.
Local Rof : A->A->Prop := [x,y:A](R (f x) (f y)).
Remark Acc_lemma : (y:B)(Acc B R y)->(x:A)(y=(f x))->(Acc A Rof x).
Induction 1; Intros.
Apply Acc_intro; Intros.
Apply (H1 (f y0)); Try Trivial.
Rewrite H2; Trivial.
Save.
Lemma Acc_inverse_image : (x:A)(Acc B R (f x)) -> (Acc A Rof x).
Intros; Apply (Acc_lemma (f x)); Trivial.
Save.
Theorem wf_inverse_image: (well_founded B R)->(well_founded A Rof).
Red; Intros; Apply Acc_inverse_image; Auto.
Save.
End Inverse_Image.
(* $Id$ *)
|
