関数

Require Import power.

Definition id_function {A : Type}
  : A -> A :=
  fun a => a.

Definition compose_functions {A B C : Type}
  (g : B -> C)
  (f : A -> B)
  : A -> C :=
  fun a => g (f a).

Section Functions.
  Context {A B : Type}.
  Variable f : A -> B.

  Definition injective : Prop :=
    forall a a',
    f a = f a' ->
    a = a'.

  Definition surjective : Prop :=
    forall b,
    exists a,
    f a = b.

  Definition bijective : Prop :=
    injective /\ surjective.

  Definition isomorphic : Prop :=
    exists g : B -> A,
    compose_functions g f = id_function /\
    compose_functions f g = id_function.

  Definition preimage
    (S : power B)
    : power A :=
    fun a => S (f a).

  Definition image
    (S : power A)
    : power B :=
    fun b => exists a, f a = b.
End Functions.

Definition isomorphism (A B : Type) : Type :=
  { f : A -> B | isomorphic f }.

Notation "A ≅ B" := (isomorphism A B) (at level 60, no associativity).

Section Functions.
  Context {A B C : Type}.
  Variable f : A -> B.
  Variable g : B -> C.

  Lemma preimage_of_composition
    (S : power C)
    : preimage (compose_functions g f) S = preimage f (preimage g S).
A, B, C: Type
f: A -> B
g: B -> C
S: power C
preimage (compose_functions g f) S = preimage f (preimage g S)
  Proof.
A, B, C: Type
f: A -> B
g: B -> C
S: power C
preimage (compose_functions g f) S = preimage f (preimage g S)
    unfold preimage, compose_functions.
A, B, C: Type
f: A -> B
g: B -> C
S: power C
(fun a : A => S (g (f a))) = (fun a : A => S (g (f a)))
    reflexivity.
  Qed.
End Functions.