Library Coq.Sets.Image
Require Export Finite_sets.
Require Export Constructive_sets.
Require Export Classical.
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.