# Library set

#### Links: Index_v Table of contents Main page

Definition Inter {A} (R S : @set A) : set := fun a ⇒ R a ∧ S a.

Hint Unfold Inter.

Definition Cmp {A} (R : @set A) : set := fun a ⇒ ¬ R a.

Hint Unfold Cmp.

Definition Union {A} (R S : @set A) : set := fun a ⇒ R a ∨ S a.

Hint Unfold Union.

Definition Inc {A} (R S : @set A) := ∀ a, R a → S a.

Hint Unfold Inc.

Definition Eq {A} (R S : @set A) := Inc R S ∧ Inc S R.

Hint Unfold Eq.

Hint Unfold Inter.

Definition Cmp {A} (R : @set A) : set := fun a ⇒ ¬ R a.

Hint Unfold Cmp.

Definition Union {A} (R S : @set A) : set := fun a ⇒ R a ∨ S a.

Hint Unfold Union.

Definition Inc {A} (R S : @set A) := ∀ a, R a → S a.

Hint Unfold Inc.

Definition Eq {A} (R S : @set A) := Inc R S ∧ Inc S R.

Hint Unfold Eq.

Lemma extEq : ∀ {A} (R S : @set A), Eq R S → R = S.

Proof.

intros A R S [RS SR].

apply functional_extensionality; intros x.

apply propositional_extensionality; split; auto.

Qed.

Proof.

intros A R S [RS SR].

apply functional_extensionality; intros x.

apply propositional_extensionality; split; auto.

Qed.