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.