Library Coqtail.Topology.TFunctions

Require Import Ensembles.
Require Import Topology.

Section Functions.

  Variable U V : Type.

  Inductive Image (X:Ensemble U) (f:U → V) : Ensemble V :=
    Image_intro : ∀ x:U, In _ X x → ∀ y:V, y = f x → In _ (Image X f) y.

  Inductive Preimage (Y:Ensemble V) (f:U → V) : Ensemble U :=
    Inverse_Image_intro : ∀ y, In _ Y y → ∀ x, y = f x → In _ (Preimage Y f) x.

  Definition function (A:Ensemble U) (B:Ensemble V) : (U→V)->Prop :=
    fun f:U→V ⇒ ∀ a:U, In U A a → In V B (f a).

  Lemma Image_in_arrival_space : ∀ (A:Ensemble U) (B:Ensemble V) (f:U→V),
      function A B f → Included _ (Image A f) B.
  Proof.
  intros A B f funf y.
  intros yIm. induction yIm.
  rewrite H0.
  apply (funf x H).
  Qed.

End Functions.