This repository has been archived by the owner on Jan 4, 2021. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 6
/
Families.v
80 lines (65 loc) · 1.49 KB
/
Families.v
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
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
Require Export Ensembles.
Require Import EnsemblesImplicit.
Set Implicit Arguments.
Section Families.
Variable T:Type.
Definition Family := Ensemble (Ensemble T).
Variable F:Family.
Inductive FamilyUnion: Ensemble T :=
| family_union_intro: forall (S:Ensemble T) (x:T),
In F S -> In S x -> In FamilyUnion x.
Inductive FamilyIntersection: Ensemble T :=
| family_intersection_intro: forall x:T,
(forall S:Ensemble T, In F S -> In S x) ->
In FamilyIntersection x.
End Families.
Section FamilyFacts.
Variable T:Type.
Lemma empty_family_union: FamilyUnion (@Empty_set (Ensemble T)) =
Empty_set.
Proof.
apply Extensionality_Ensembles.
unfold Same_set.
unfold Included.
intuition.
destruct H.
contradiction H.
contradiction H.
Qed.
Lemma empty_family_intersection:
FamilyIntersection (@Empty_set (Ensemble T)) = Full_set.
Proof.
apply Extensionality_Ensembles.
unfold Same_set.
unfold Included.
intuition.
constructor.
constructor.
intros.
contradiction H0.
Qed.
(* unions and intersections of subfamilies *)
Lemma subfamily_union: forall F G:Family T, Included F G ->
Included (FamilyUnion F) (FamilyUnion G).
Proof.
unfold Included.
intros.
destruct H0.
apply family_union_intro with S.
apply H.
assumption.
assumption.
Qed.
Lemma subfamily_intersection: forall F G:Family T, Included F G ->
Included (FamilyIntersection G) (FamilyIntersection F).
Proof.
unfold Included.
intros.
constructor.
destruct H0.
intros.
apply H0.
apply H.
assumption.
Qed.
End FamilyFacts.