Library Coq.Sets.Image
Require Export Finite_sets.
Require Export Constructive_sets.
Require Export Classical_Type.
Require Export Classical_sets.
Require Export Powerset.
Require Export Powerset_facts.
Require Export Powerset_Classical_facts.
Require Export Gt.
Require Export Lt.
Require Export Le.
Require Export Finite_sets_facts.
Section Image.
Variables U V :
Type.
Inductive Im (
X:
Ensemble U) (
f:
U ->
V) :
Ensemble V :=
Im_intro :
forall x:
U,
In _ X x ->
forall y:
V,
y = f x ->
In _ (
Im X f)
y.
Lemma Im_def :
forall (
X:
Ensemble U) (
f:
U ->
V) (
x:
U),
In _ X x ->
In _ (
Im X f) (
f x).
Lemma Im_add :
forall (
X:
Ensemble U) (
x:
U) (
f:
U ->
V),
Im (
Add _ X x)
f = Add _ (
Im X f) (
f x).
Lemma image_empty :
forall f:
U ->
V,
Im (
Empty_set U)
f = Empty_set V.
Lemma finite_image :
forall (
X:
Ensemble U) (
f:
U ->
V),
Finite _ X ->
Finite _ (
Im X f).
Lemma Im_inv :
forall (
X:
Ensemble U) (
f:
U ->
V) (
y:
V),
In _ (
Im X f)
y ->
exists x :
U, In _ X x /\ f x = y.
Definition injective (
f:
U ->
V) :=
forall x y:
U,
f x = f y ->
x = y.
Lemma not_injective_elim :
forall f:
U ->
V,
~ injective f ->
exists x :
_, (exists y :
_, f x = f y /\ x <> y).
Lemma cardinal_Im_intro :
forall (
A:
Ensemble U) (
f:
U ->
V) (
n:
nat),
cardinal _ A n ->
exists p :
nat, cardinal _ (
Im A f)
p.
Lemma In_Image_elim :
forall (
A:
Ensemble U) (
f:
U ->
V),
injective f ->
forall x:
U,
In _ (
Im A f) (
f x) ->
In _ A x.
Lemma injective_preserves_cardinal :
forall (
A:
Ensemble U) (
f:
U ->
V) (
n:
nat),
injective f ->
cardinal _ A n ->
forall n':
nat,
cardinal _ (
Im A f)
n' ->
n' = n.
Lemma cardinal_decreases :
forall (
A:
Ensemble U) (
f:
U ->
V) (
n:
nat),
cardinal U A n ->
forall n':
nat,
cardinal V (
Im A f)
n' ->
n' <= n.
Theorem Pigeonhole :
forall (
A:
Ensemble U) (
f:
U ->
V) (
n:
nat),
cardinal U A n ->
forall n':
nat,
cardinal V (
Im A f)
n' ->
n' < n ->
~ injective f.
Lemma Pigeonhole_principle :
forall (
A:
Ensemble U) (
f:
U ->
V) (
n:
nat),
cardinal _ A n ->
forall n':
nat,
cardinal _ (
Im A f)
n' ->
n' < n ->
exists x :
_, (exists y :
_, f x = f y /\ x <> y).
End Image.
Hint Resolve Im_def image_empty finite_image:
sets v62.